mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-06-06 17:11:01 +00:00
Code Activity

tests/symfpu: Add cover checks

Browse source 
Include mask/map for abc inputs (and switch to `anyconst` instead of `anyseq`).
Add false divide check for mantissa.
Covers aren't currently being tested by anything (and have to be removed for `sat`), but I've been using it locally with SBY to confirm that the different edge cases are able to be verified (e.g. when verifying HardFloat against symfpu while using the masked inputs to reduce solver time).
This commit is contained in:
Krystine Sherwin 2026-06-06 09:34:43 +12:00
parent acf011b0f0
commit d628022459
No known key found for this signature in database
2 changed files with 174 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

1
tests/symfpu/run-test.sh
View file

@ -19,6 +19,7 @@ chformal -remove
opt
read_verilog -sv -formal $defs -D${rm} edges.sv
chformal -remove -cover
chformal -lower
prep -top edges -flatten
sat -set-assumes -prove-asserts -verify