mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-13 04:28:18 +00:00
Add tests/various/abc9.{v,ys} with SCC test
This commit is contained in:
parent
cec2292b0b
commit
9dca024a30
5
tests/various/abc9.v
Normal file
5
tests/various/abc9.v
Normal file
|
@ -0,0 +1,5 @@
|
||||||
|
module abc9_test027(output reg o);
|
||||||
|
initial o = 1'b0;
|
||||||
|
always @*
|
||||||
|
o <= ~o;
|
||||||
|
endmodule
|
14
tests/various/abc9.ys
Normal file
14
tests/various/abc9.ys
Normal file
|
@ -0,0 +1,14 @@
|
||||||
|
read_verilog abc9.v
|
||||||
|
proc
|
||||||
|
design -save gold
|
||||||
|
|
||||||
|
abc9 -lut 4
|
||||||
|
check
|
||||||
|
design -stash gate
|
||||||
|
|
||||||
|
design -import gold -as gold
|
||||||
|
design -import gate -as gate
|
||||||
|
|
||||||
|
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||||
|
sat -verify -prove-asserts -show-ports miter
|
||||||
|
|
Loading…
Reference in a new issue