Skip to content

Annotate a vPlan from a formal run #252

Description

@martin-velay

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 Define some statically typed class with the stuff from a FlowCfg that Deploy cares about #161 and Tidy up the name of Deploy.sim_cfg #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 OneShotCfg.gen_results never writes report files to disk (lint/syn/formal/cdc/rdc) #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.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions