Merge pull request #5844 from YosysHQ/lofty/abc-refactor-5

abc_new: integration testing via synth_gatemate

tests/arch/gatemate/add_sub.ys

@@ -1,9 +1,29 @@
 read_verilog ../common/add_sub.v
 hierarchy -top top
 proc
+design -save orig
+
 equiv_opt -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd top # Constrain all select calls below inside the top module
 select -assert-count 8 t:CC_ADDF
 select -assert-max 4 t:CC_LUT1
 select -assert-none t:CC_ADDF t:CC_LUT1 %% t:* %D
+
+design -load orig
+
+equiv_opt -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd top # Constrain all select calls below inside the top module
+select -assert-count 8 t:CC_ADDF
+select -assert-max 4 t:CC_LUT1
+select -assert-none t:CC_ADDF t:CC_LUT1 %% t:* %D
+
+design -load orig
+
+equiv_opt -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -abc_new # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd top # Constrain all select calls below inside the top module
+select -assert-count 8 t:CC_ADDF
+select -assert-max 4 t:CC_LUT1
+select -assert-none t:CC_ADDF t:CC_LUT1 %% t:* %D

tests/arch/gatemate/adffs.ys

@@ -31,6 +31,28 @@ select -assert-count 1 t:CC_DFF
 select -assert-max 1 t:CC_LUT2
 select -assert-none t:CC_BUFG t:CC_DFF t:CC_LUT2 %% t:* %D
 
+design -load read
+hierarchy -top dffs
+proc
+equiv_opt -async2sync -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd dffs # Constrain all select calls below inside the top module
+select -assert-count 1 t:CC_BUFG
+select -assert-count 1 t:CC_DFF
+select -assert-max 1 t:CC_LUT2
+select -assert-none t:CC_BUFG t:CC_DFF t:CC_LUT2 %% t:* %D
+
+design -load read
+hierarchy -top dffs
+proc
+equiv_opt -async2sync -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -abc_new # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd dffs # Constrain all select calls below inside the top module
+select -assert-count 1 t:CC_BUFG
+select -assert-count 1 t:CC_DFF
+select -assert-max 1 t:CC_LUT2
+select -assert-none t:CC_BUFG t:CC_DFF t:CC_LUT2 %% t:* %D
+
 design -load read
 hierarchy -top ndffnr
 proc
@@ -41,3 +63,25 @@ select -assert-count 1 t:CC_BUFG
 select -assert-count 1 t:CC_DFF
 select -assert-max 1 t:CC_LUT2
 select -assert-none t:CC_BUFG t:CC_DFF t:CC_LUT2 %% t:* %D
+
+design -load read
+hierarchy -top ndffnr
+proc
+equiv_opt -async2sync -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd ndffnr # Constrain all select calls below inside the top module
+select -assert-count 1 t:CC_BUFG
+select -assert-count 1 t:CC_DFF
+select -assert-max 1 t:CC_LUT2
+select -assert-none t:CC_BUFG t:CC_DFF t:CC_LUT2 %% t:* %D
+
+design -load read
+hierarchy -top ndffnr
+proc
+equiv_opt -async2sync -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -abc_new # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd ndffnr # Constrain all select calls below inside the top module
+select -assert-count 1 t:CC_BUFG
+select -assert-count 1 t:CC_DFF
+select -assert-max 1 t:CC_LUT2
+select -assert-none t:CC_BUFG t:CC_DFF t:CC_LUT2 %% t:* %D

tests/arch/gatemate/counter.ys

@@ -2,6 +2,9 @@ read_verilog ../common/counter.v
 hierarchy -top top
 proc
 flatten
+
+design -save orig
+
 equiv_opt -assert -async2sync -map +/gatemate/cells_sim.v synth_gatemate -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd top # Constrain all select calls below inside the top module
@@ -10,3 +13,25 @@ select -assert-count 8 t:CC_ADDF
 select -assert-count 1 t:CC_BUFG
 select -assert-count 8 t:CC_DFF
 select -assert-none t:CC_ADDF t:CC_BUFG t:CC_DFF %% t:* %D
+
+design -load orig
+
+equiv_opt -assert -async2sync -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd top # Constrain all select calls below inside the top module
+
+select -assert-count 8 t:CC_ADDF
+select -assert-count 1 t:CC_BUFG
+select -assert-count 8 t:CC_DFF
+select -assert-none t:CC_ADDF t:CC_BUFG t:CC_DFF %% t:* %D
+
+design -load orig
+
+equiv_opt -assert -async2sync -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -abc_new # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd top # Constrain all select calls below inside the top module
+
+select -assert-count 8 t:CC_ADDF
+select -assert-count 1 t:CC_BUFG
+select -assert-count 8 t:CC_DFF
+select -assert-none t:CC_ADDF t:CC_BUFG t:CC_DFF %% t:* %D

tests/arch/gatemate/fsm.ys

@@ -3,6 +3,8 @@ hierarchy -top fsm
 proc
 flatten
 
+design -save orig
+
 equiv_opt -run :prove -map +/gatemate/cells_sim.v synth_gatemate -noiopad
 async2sync
 miter -equiv -make_assert -flatten gold gate miter
@@ -18,3 +20,42 @@ select -assert-max 5 t:CC_LUT2
 select -assert-max 6 t:CC_LUT3
 select -assert-max 9 t:CC_LUT4
 select -assert-none t:CC_BUFG t:CC_DFF t:CC_LUT2 t:CC_LUT3 t:CC_LUT4 %% t:* %D
+
+design -load orig
+
+equiv_opt -run :prove -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree
+async2sync
+miter -equiv -make_assert -flatten gold gate miter
+stat
+sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
+
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd fsm # Constrain all select calls below inside the top module
+
+select -assert-count 1 t:CC_BUFG
+select -assert-count 6 t:CC_DFF
+select -assert-max 2 t:CC_LUT1
+select -assert-count 1 t:CC_LUT2
+select -assert-max 14 t:CC_L2T4
+select -assert-max 5 t:CC_L2T5
+select -assert-max 1 t:CC_MX2
+select -assert-none t:CC_BUFG t:CC_DFF t:CC_LUT1 t:CC_LUT2 t:CC_L2T4 t:CC_L2T5 t:CC_MX2 %% t:* %D
+
+design -load orig
+
+equiv_opt -run :prove -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -abc_new
+async2sync
+miter -equiv -make_assert -flatten gold gate miter
+stat
+sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
+
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd fsm # Constrain all select calls below inside the top module
+
+select -assert-count 1 t:CC_BUFG
+select -assert-count 6 t:CC_DFF
+select -assert-count 2 t:CC_LUT2
+select -assert-count 9 t:CC_L2T4
+select -assert-count 6 t:CC_L2T5
+select -assert-count 1 t:CC_MX2
+select -assert-none t:CC_BUFG t:CC_DFF t:CC_LUT2 t:CC_L2T4 t:CC_L2T5 t:CC_MX2 %% t:* %D

tests/arch/gatemate/latches.ys

@@ -27,3 +27,23 @@ cd latchsr # Constrain all select calls below inside the top module
 select -assert-count 1 t:CC_DLT
 select -assert-max 2 t:CC_LUT3
 select -assert-none t:CC_DLT t:CC_LUT3 %% t:* %D
+
+design -load read
+hierarchy -top latchsr
+proc
+equiv_opt -async2sync -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd latchsr # Constrain all select calls below inside the top module
+select -assert-count 1 t:CC_DLT
+select -assert-max 2 t:CC_L2T4
+select -assert-none t:CC_DLT t:CC_L2T4 %% t:* %D
+
+design -load read
+hierarchy -top latchsr
+proc
+equiv_opt -async2sync -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -abc_new # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd latchsr # Constrain all select calls below inside the top module
+select -assert-count 1 t:CC_DLT
+select -assert-max 2 t:CC_L2T4
+select -assert-none t:CC_DLT t:CC_L2T4 %% t:* %D

tests/arch/gatemate/logic.ys

@@ -1,6 +1,9 @@
 read_verilog ../common/logic.v
 hierarchy -top top
 proc
+
+design -save orig
+
 equiv_opt -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd top # Constrain all select calls below inside the top module
@@ -8,3 +11,23 @@ select -assert-max 1 t:CC_LUT1
 select -assert-max 6 t:CC_LUT2
 select -assert-max 2 t:CC_LUT4
 select -assert-none t:CC_LUT1 t:CC_LUT2 t:CC_LUT4 %% t:* %D
+
+design -load orig
+
+equiv_opt -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd top # Constrain all select calls below inside the top module
+select -assert-count 1 t:CC_LUT1
+select -assert-count 6 t:CC_LUT2
+select -assert-count 2 t:CC_L2T4
+select -assert-none t:CC_LUT1 t:CC_LUT2 t:CC_L2T4 %% t:* %D
+
+design -load orig
+
+equiv_opt -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -abc_new # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd top # Constrain all select calls below inside the top module
+select -assert-count 1 t:CC_LUT1
+select -assert-count 6 t:CC_LUT2
+select -assert-count 2 t:CC_L2T4
+select -assert-none t:CC_LUT1 t:CC_LUT2 t:CC_L2T4 %% t:* %D

tests/arch/gatemate/luttrees.ys

@@ -11,3 +11,24 @@ cd luttrees # Constrain all select calls below inside the top module
 select -assert-count 750 t:CC_LUT2 t:CC_L2T4 t:CC_L2T5 %%
 select -assert-none t:CC_LUT2 t:CC_L2T4 t:CC_L2T5 %% t:* %D
 
+design -load read
+
+hierarchy -top luttrees
+proc
+equiv_opt -async2sync -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -nomx4 -nomx8 -luttree # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd luttrees # Constrain all select calls below inside the top module
+
+select -assert-count 750 t:CC_LUT2 t:CC_L2T4 t:CC_L2T5 %%
+select -assert-none t:CC_LUT2 t:CC_L2T4 t:CC_L2T5 %% t:* %D
+
+design -load read
+
+hierarchy -top luttrees
+proc
+equiv_opt -async2sync -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -nomx4 -nomx8 -luttree -abc_new # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd luttrees # Constrain all select calls below inside the top module
+
+select -assert-count 750 t:CC_LUT2 t:CC_L2T4 t:CC_L2T5 %%
+select -assert-none t:CC_LUT2 t:CC_L2T4 t:CC_L2T5 %% t:* %D

tests/arch/gatemate/mul.ys

@@ -31,3 +31,29 @@ select -assert-count 1 t:CC_BUFG
 select -assert-max 18 t:CC_LUT4
 select -assert-count 18 t:CC_DFF
 select -assert-none t:CC_MULT t:CC_BUFG t:CC_LUT4 t:CC_DFF %% t:* %D
+
+design -load read
+hierarchy -top mul_unsigned_sync
+proc
+equiv_opt -assert -async2sync -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd mul_unsigned_sync # Constrain all select calls below inside the top module
+select -assert-count 1 t:CC_MULT
+select -assert-count 1 t:CC_BUFG
+select -assert-count 18 t:CC_LUT2
+select -assert-count 18 t:CC_MX2
+select -assert-count 18 t:CC_DFF
+select -assert-none t:CC_MULT t:CC_BUFG t:CC_LUT2 t:CC_MX2 t:CC_DFF %% t:* %D
+
+design -load read
+hierarchy -top mul_unsigned_sync
+proc
+# equiv_opt -assert -async2sync -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -abc_new # equivalency check (fails)
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd mul_unsigned_sync # Constrain all select calls below inside the top module
+select -assert-count 1 t:CC_MULT
+select -assert-count 1 t:CC_BUFG
+select -assert-count 18 t:CC_LUT2
+select -assert-count 18 t:CC_MX2
+select -assert-count 18 t:CC_DFF
+select -assert-none t:CC_MULT t:CC_BUFG t:CC_LUT2 t:CC_MX2 t:CC_DFF %% t:* %D

tests/arch/gatemate/mux.ys

@@ -12,6 +12,25 @@ select -assert-max 2 t:CC_LUT4
 select -assert-max 1 t:CC_MX2
 select -assert-none t:CC_LUT2 t:CC_LUT4 t:CC_MX2 %% t:* %D
 
+design -load read
+hierarchy -top mux4
+proc
+equiv_opt -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd mux4 # Constrain all select calls below inside the top module
+select -assert-count 3 t:CC_MX2
+select -assert-none t:CC_MX2 %% t:* %D
+
+design -load read
+hierarchy -top mux4
+proc
+equiv_opt -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -abc_new # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd mux4 # Constrain all select calls below inside the top module
+select -assert-count 1 t:CC_LUT1
+select -assert-count 3 t:CC_MX2
+select -assert-none t:CC_LUT1 t:CC_MX2 %% t:* %D
+
 design -load read
 hierarchy -top mux8
 proc
@@ -22,3 +41,21 @@ select -assert-max 1 t:CC_LUT3
 select -assert-max 5 t:CC_LUT4
 select -assert-max 1 t:CC_MX2
 select -assert-none t:CC_LUT3 t:CC_LUT4 t:CC_MX2 %% t:* %D
+
+design -load read
+hierarchy -top mux8
+proc
+equiv_opt -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd mux8 # Constrain all select calls below inside the top module
+select -assert-count 7 t:CC_MX2
+select -assert-none t:CC_MX2 %% t:* %D
+
+design -load read
+hierarchy -top mux8
+proc
+equiv_opt -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -abc_new # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd mux8 # Constrain all select calls below inside the top module
+select -assert-count 7 t:CC_MX2
+select -assert-none t:CC_MX2 %% t:* %D

tests/techmap/abc_speed_gia_only.script

@@ -1,28 +0,0 @@
-&st
-&dch -r
-&nf
-&st
-&syn2
-&if -g -K 6
-&synch2 -r
-&nf
-&st
-&syn2
-&if -g -K 6
-&synch2 -r
-&nf
-&st
-&syn2
-&if -g -K 6
-&synch2 -r
-&nf
-&st
-&syn2
-&if -g -K 6
-&synch2 -r
-&nf
-&st
-&syn2
-&if -g -K 6
-&synch2 -r
-&nf

tests/techmap/xaiger2-5169.ys

@@ -57,4 +57,4 @@ endmodule
 EOF
 
 logger -expect error "Malformed design" 1
-abc_new -script abc_speed_gia_only.script -liberty ../../tests/liberty/normal.lib -liberty ../../tests/liberty/dff.lib
+abc_new -liberty ../../tests/liberty/normal.lib -liberty ../../tests/liberty/dff.lib