diff options
Diffstat (limited to 'tests/various/chformal_coverprecond.ys')
| -rw-r--r-- | tests/various/chformal_coverprecond.ys | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/tests/various/chformal_coverprecond.ys b/tests/various/chformal_coverprecond.ys new file mode 100644 index 000000000..59e302a72 --- /dev/null +++ b/tests/various/chformal_coverprecond.ys @@ -0,0 +1,25 @@ +read_verilog -formal <<EOT +module top(input a, b, c, d); + + always @* begin + if (a) assert (b == c); + if (!a) assert (b != c); + if (b) assume (c); + if (c) cover (d); + end + +endmodule +EOT + +prep -top top + +select -assert-count 1 t:$cover + +chformal -cover -coverprecond +select -assert-count 2 t:$cover + +chformal -assert -coverprecond +select -assert-count 4 t:$cover + +chformal -assume -coverprecond +select -assert-count 5 t:$cover |