mirror of
https://github.com/YosysHQ/yosys
synced 2025-08-03 18:00:24 +00:00
tests: Add equiv_assume.ys
This commit is contained in:
parent
af0b263557
commit
a57c593c41
1 changed files with 26 additions and 0 deletions
26
tests/various/equiv_assume.ys
Normal file
26
tests/various/equiv_assume.ys
Normal file
|
@ -0,0 +1,26 @@
|
|||
read_verilog -sv <<EOT
|
||||
module gold (input D, output Q);
|
||||
assign Q = '0;
|
||||
endmodule
|
||||
|
||||
module gate (input D, output Q);
|
||||
assume property (D == '0);
|
||||
assign Q = D;
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
chformal -lower
|
||||
async2sync
|
||||
design -stash input
|
||||
|
||||
# using $assert cells in sat verifies
|
||||
design -load input
|
||||
equiv_make -make_assert gold gate equiv
|
||||
prep -top equiv
|
||||
sat -set-assumes -prove-asserts -verify
|
||||
|
||||
# so should $equiv
|
||||
design -load input
|
||||
equiv_make gold gate equiv
|
||||
equiv_simple equiv
|
||||
equiv_status -assert equiv
|
Loading…
Add table
Add a link
Reference in a new issue