lowRISC / lowRISC/dvsim

Annotate a vPlan from a formal run

Open
#252 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

enhancement
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

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. 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

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.