Annotate a vPlan from a formal run
Nobody has claimed this yet.
- Dominant language
- Python
- Stars
- 13
- Forks
- 21
- Avg merge
- 1d 11h
- Merged PRs (30d)
- 8
Description
Part of lowRISC/dvplan#129, and follows the source-naming issue.
The vPlan annotation is a simulation feature today. `CovVPlan` is typed against `SimCfg`, and the job is created in `sim/flow.py`. A formal run produces results a vPlan wants just as much, and an FPV config should be able to score a plan on its own without waiting for the bundle work.
## Scope
- Move the vPlan job and its config keys onto `FlowCfg`, so any flow that names a `vplan` gets it. `CovVPlan` stops depending on `SimCfg`, which is the same tidy-up as #161 and #164 ask for in general.
- `FormalCfg` gains the keys and returns its own sources from `vplan_sources()`: the property report the run wrote, and the expected-failure file where the config names one, which DVPlan reads as an exclusion.
- The job depends on the formal run finishing, and is scored whether the run passed or failed, as it already is for simulation. A regression where nothing proved is the case a plan most needs to describe.
- Optionally write a `dv_evidence` file for a formal run too, holding one `testcase` record for the run itself, so a plan can hold a testpoint saying the FPV run passes. Cheap, and independent of the formal parsers.
- Note that `OneShotCfg.gen_results` never writes report files to disk, which is #247. The annotated plan and its HTML land in the job's own output directory, so this does not depend on that being fixed, but the flow report will not link to it until it is.
## Done when
- `dvsim hw/ip/hmac/fpv/hmac_fpv_cfg.hjson` with a `vplan` key writes an annotated plan and its report.
- Simulation behaviour is unchanged.
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start in sim/flow.py and trace how CovVPlan, SimCfg, FlowCfg, and FormalCfg create jobs and expose sources. Run dvsim hw/ip/hmac/fpv/hmac_fpv_cfg.hjson with a vplan key, then verify that formal completion produces the annotated plan and HTML report while existing simulation behavior remains unchanged.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- python
- Domain
- build-system, devtools
- Issue type
- Feature
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Active
- Clarity
- Mostly clear
- Newbie friendliness
- 48/100