Reenable existing equiv_opt tests

This commit is contained in:
Jannis Harder 2022-08-30 13:56:05 +02:00
parent 81906aa627
commit 0113f44faa
13 changed files with 52 additions and 54 deletions

View File

@ -70,4 +70,4 @@ EOT
read_verilog -lib +/ice40/cells_sim.v read_verilog -lib +/ice40/cells_sim.v
hierarchy -top top hierarchy -top top
flatten flatten
equiv_opt -multiclock -map +/ice40/cells_sim.v synth_ice40 equiv_opt -assert -multiclock -map +/ice40/cells_sim.v synth_ice40

View File

@ -2,7 +2,7 @@ read_verilog ../common/counter.v
hierarchy -top top hierarchy -top top
proc proc
flatten flatten
equiv_opt -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # equivalency check equiv_opt -assert -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) 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 cd top # Constrain all select calls below inside the top module
@ -17,7 +17,7 @@ read_verilog ../common/counter.v
hierarchy -top top hierarchy -top top
proc proc
flatten flatten
equiv_opt -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check equiv_opt -assert -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) 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 cd top # Constrain all select calls below inside the top module

View File

@ -10,7 +10,7 @@ design -save read
select -assert-count 2 t:$xor select -assert-count 2 t:$xor
select -assert-count 2 t:$xnor select -assert-count 2 t:$xnor
equiv_opt opt_expr equiv_opt -assert opt_expr
design -load postopt design -load postopt
select -assert-none t:$xor select -assert-none t:$xor
select -assert-none t:$xnor select -assert-none t:$xnor
@ -19,7 +19,7 @@ select -assert-count 2 t:$not
design -load read design -load read
simplemap simplemap
equiv_opt opt_expr equiv_opt -assert opt_expr
design -load postopt design -load postopt
select -assert-none t:$_XOR_ select -assert-none t:$_XOR_
select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_ select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_
@ -34,7 +34,7 @@ $_XNOR_ u1(.A(1'b1), .B(a), .Y(y[1]));
endmodule endmodule
EOT EOT
select -assert-count 2 t:$_XNOR_ select -assert-count 2 t:$_XNOR_
equiv_opt opt_expr equiv_opt -assert opt_expr
design -load postopt design -load postopt
select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_ select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_
select -assert-count 1 t:$_NOT_ select -assert-count 1 t:$_NOT_
@ -49,7 +49,7 @@ assign y = a~^1'b0;
assign z = a~^1'b1; assign z = a~^1'b1;
endmodule endmodule
EOT EOT
equiv_opt opt_expr equiv_opt -assert opt_expr
# Single-bit $xor # Single-bit $xor

View File

@ -16,4 +16,4 @@ EOT
proc proc
equiv_opt -async2sync techmap -map +/adff2dff.v #equiv_opt -assert -async2sync techmap -map +/adff2dff.v

View File

@ -13,4 +13,4 @@ EOT
proc proc
equiv_opt techmap -map +/dff2ff.v equiv_opt -assert techmap -map +/dff2ff.v

View File

@ -24,8 +24,8 @@ design -save orig
flatten flatten
equiv_opt -assert -multiclock dfflegalize -cell $_ALDFF_PP_ x equiv_opt -assert -multiclock dfflegalize -cell $_ALDFF_PP_ x
equiv_opt -assert -multiclock dfflegalize -cell $_ALDFFE_PPP_ x equiv_opt -assert -multiclock dfflegalize -cell $_ALDFFE_PPP_ x
#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ x equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ x
#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ x equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ x
# Convert everything to ALDFFs. # Convert everything to ALDFFs.

View File

@ -26,10 +26,10 @@ equiv_opt -assert -multiclock dfflegalize -cell $_ALDFF_PP_ 0
equiv_opt -assert -multiclock dfflegalize -cell $_ALDFF_PP_ 1 equiv_opt -assert -multiclock dfflegalize -cell $_ALDFF_PP_ 1
equiv_opt -assert -multiclock dfflegalize -cell $_ALDFFE_PPP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_ALDFFE_PPP_ 0
equiv_opt -assert -multiclock dfflegalize -cell $_ALDFFE_PPP_ 1 equiv_opt -assert -multiclock dfflegalize -cell $_ALDFFE_PPP_ 1
#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0
#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1
#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0
#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1
# Convert everything to ALDFFs. # Convert everything to ALDFFs.

View File

@ -41,18 +41,18 @@ EOT
design -save orig design -save orig
flatten flatten
#equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP0_ 0 -cell $_SR_PP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP0_ 0 -cell $_SR_PP_ 0
#equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP0_ 1 -cell $_SR_PP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP0_ 1 -cell $_SR_PP_ 0
#equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP1_ 0 -cell $_SR_PP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP1_ 0 -cell $_SR_PP_ 0
#equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP1_ 1 -cell $_SR_PP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP1_ 1 -cell $_SR_PP_ 0
#equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP0P_ 0 -cell $_SR_PP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP0P_ 0 -cell $_SR_PP_ 0
#equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP0P_ 1 -cell $_SR_PP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP0P_ 1 -cell $_SR_PP_ 0
#equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP1P_ 0 -cell $_SR_PP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP1P_ 0 -cell $_SR_PP_ 0
#equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP1P_ 1 -cell $_SR_PP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP1P_ 1 -cell $_SR_PP_ 0
#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0
#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1
#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0
#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1
# Convert everything to ADFFs. # Convert everything to ADFFs.

View File

@ -14,7 +14,7 @@ $_DLATCHSR_PNP_ ff2 (.E(E), .R(R), .S(S), .D(D), .Q(Q[2]));
$_DLATCHSR_NPP_ ff3 (.E(E), .R(R), .S(S), .D(D), .Q(Q[3])); $_DLATCHSR_NPP_ ff3 (.E(E), .R(R), .S(S), .D(D), .Q(Q[3]));
endmodule endmodule
module top(input C, E, R, S, D, output [17:0] Q); module top(input C, E, R, S, D, output [7:0] Q);
dlatchsr0 dlatchsr0_(.E(E), .R(R), .S(S), .D(D), .Q(Q[3:0])); dlatchsr0 dlatchsr0_(.E(E), .R(R), .S(S), .D(D), .Q(Q[3:0]));
dlatchsr1 dlatchsr1_(.E(E), .R(R), .S(S), .D(D), .Q(Q[7:4])); dlatchsr1 dlatchsr1_(.E(E), .R(R), .S(S), .D(D), .Q(Q[7:4]));
endmodule endmodule
@ -23,12 +23,12 @@ EOT
design -save orig design -save orig
flatten flatten
#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 0
#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 1 equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 1
#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 0
#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 1 equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 1
#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 0
#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 1 equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 1
# Convert everything to ADLATCHs. # Convert everything to ADLATCHs.

View File

@ -21,18 +21,18 @@ EOT
design -save orig design -save orig
flatten flatten
#equiv_opt -assert -multiclock dfflegalize -cell $_SR_PP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_SR_PP_ 0
#equiv_opt -assert -multiclock dfflegalize -cell $_SR_PP_ 1 equiv_opt -assert -multiclock dfflegalize -cell $_SR_PP_ 1
#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 0
#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 1 equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 1
#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 0
#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 1 equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 1
#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 0
#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 1 equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 1
#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0
#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1
#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0
#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1
# Convert everything to SRs. # Convert everything to SRs.

View File

@ -12,4 +12,4 @@ output [3:0] O;
endmodule endmodule
EOT EOT
equiv_opt techmap -map +/pmux2mux.v equiv_opt -assert techmap -map +/pmux2mux.v

View File

@ -106,4 +106,4 @@ endmodule
EOT EOT
opt opt
wreduce wreduce
equiv_opt techmap equiv_opt -assert techmap

View File

@ -95,9 +95,8 @@ $_SDFFE_PP1P_ dff23(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[23]));
endmodule endmodule
EOT EOT
#equiv_opt -assert -multiclock zinit equiv_opt -assert -multiclock zinit
#design -load postopt design -load postopt
zinit
select -assert-count 48 t:$_NOT_ select -assert-count 48 t:$_NOT_
select -assert-count 0 w:Q a:init %i select -assert-count 0 w:Q a:init %i
@ -142,9 +141,8 @@ $_SDFFE_PP1P_ dff23(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[23]));
endmodule endmodule
EOT EOT
#equiv_opt -assert -multiclock zinit equiv_opt -assert -multiclock zinit
#design -load postopt design -load postopt
zinit
select -assert-count 0 t:$_NOT_ select -assert-count 0 t:$_NOT_
select -assert-count 1 w:Q a:init=24'b0 %i select -assert-count 1 w:Q a:init=24'b0 %i