diff options
| author | Jannis Harder <me@jix.one> | 2022-05-09 15:04:01 +0200 |
|---|---|---|
| committer | Jannis Harder <me@jix.one> | 2022-05-09 15:04:01 +0200 |
| commit | a855d62b420446756a8a36f5fd25a5c77ff07e16 (patch) | |
| tree | 83e61e98317217b5d0563eb6cdf638b2cac79ef4 /tests/sva/runtest.sh | |
| parent | 58b23954e89a75e726d98716d5029f148c804073 (diff) | |
| download | yosys-a855d62b420446756a8a36f5fd25a5c77ff07e16.tar.gz yosys-a855d62b420446756a8a36f5fd25a5c77ff07e16.tar.bz2 yosys-a855d62b420446756a8a36f5fd25a5c77ff07e16.zip | |
verific: Improve logic generated for SVA value change expressions
The previously generated logic assumed an unconstrained past value in
the initial state and did not handle 'x values. While the current formal
verification flow uses 2-valued logic, SVA value change expressions
require a past value of 'x during the initial state to behave in the
expected way (i.e. to consider both an initial 0 and an initial 1 as
$changed and an initial 1 as $rose and an initial 0 as $fell).
This patch now generates logic that at the same time
a) provides the expected behavior in a 2-valued logic setting, not
depending on any dont-care optimizations, and
b) properly handles 'x values in yosys simulation
Diffstat (limited to 'tests/sva/runtest.sh')
| -rw-r--r-- | tests/sva/runtest.sh | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tests/sva/runtest.sh b/tests/sva/runtest.sh index 8ed7f8cbc..2ecc9780c 100644 --- a/tests/sva/runtest.sh +++ b/tests/sva/runtest.sh @@ -57,7 +57,9 @@ generate_sby() { fi } -if [ -f $prefix.sv ]; then +if [ -f $prefix.ys ]; then + $PWD/../../yosys -q -e "Assert .* failed." -s $prefix.ys +elif [ -f $prefix.sv ]; then generate_sby pass > ${prefix}_pass.sby generate_sby fail > ${prefix}_fail.sby sby --yosys $PWD/../../yosys -f ${prefix}_pass.sby |