fix: report the formal coverage columns the engine actually measured - #257
Open
martin-velay wants to merge 1 commit into
Open
fix: report the formal coverage columns the engine actually measured#257martin-velay wants to merge 1 commit into
martin-velay wants to merge 1 commit into
Conversation
get_coverage read formal_coverage["formal"], ["stimuli"] and ["checker"],
which are the columns a JasperGold run reports. A VC Formal run reports
stimuli, coi and proof, so reporting one raised KeyError: 'formal' and
took dvsim down with a traceback after the build job had already passed
and written its results.
The columns are now taken from the report the tool's own parser wrote,
and summary_header follows them, so the cross-cfg summary table names the
columns the cfg's engine filled in rather than another engine's. Only
stimuli is common to the two engines, so neither set can stand in for the
other and there is nothing to harmonise onto.
This was reachable only once an OpenTitan-side bug was fixed. The
vcformal parse-formal-report.py rejects the --exp-fail-path that
common_formal_cfg.hjson always passes, so make failed, no results.hjson
was written, result.get("coverage") returned None, and get_coverage took
its "No coverage information found" branch instead.
tests/flow/ is new; nothing covered this module before.
AI-assisted (Claude Code) — reviewed and approved by author
Signed-off-by: Martin Velay <mvelay@lowrisc.org>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description
get_coverage read formal_coverage["formal"], ["stimuli"] and ["checker"], which are the columns a JasperGold run reports. A VC Formal run reports stimuli, coi and proof, so reporting one raised KeyError: 'formal' and took dvsim down with a traceback after the build job had already passed and written its results.
The columns are now taken from the report the tool's own parser wrote, and summary_header follows them, so the cross-cfg summary table names the columns the cfg's engine filled in rather than another engine's. Only stimuli is common to the two engines, so neither set can stand in for the other and there is nothing to harmonise onto.
This was reachable only once an OpenTitan-side bug was fixed. The vcformal parse-formal-report.py rejects the --exp-fail-path that common_formal_cfg.hjson always passes, so make failed, no results.hjson was written, result.get("coverage") returned None, and get_coverage took its "No coverage information found" branch instead.
tests/flow/ is new; nothing covered this module before.
AI-assisted (Claude Code) — reviewed and approved by author