extract_fa: Add test case

This commit is contained in:
Jannis Harder 2024-10-30 17:30:44 +01:00 committed by Øystein Hovind
parent f445479374
commit 40c690b030
1 changed files with 29 additions and 0 deletions

29
tests/various/bug3879.ys Normal file
View File

@ -0,0 +1,29 @@
read_verilog <<EOF
module gcd(I, D);
output [2:0] I;
input [3:0] D;
assign I = D[0]+D[1]+D[2]+D[3];
endmodule
EOF
design -save input
prep
design -stash gold
design -load input
synth -top gcd -flatten
extract_fa -v
design -stash gate
design -copy-from gold -as gold gcd
design -copy-from gate -as gate gcd
miter -equiv -make_assert -flatten gold gate miter
sat -verify -prove-asserts -show-all miter