diff --git a/tests/techmap/dlatchlibmap.ys b/tests/techmap/dlatchlibmap.ys index dd1a943e1..f4ba8dc7d 100644 --- a/tests/techmap/dlatchlibmap.ys +++ b/tests/techmap/dlatchlibmap.ys @@ -25,6 +25,8 @@ equiv_opt -map dlatchlibmap-sim.v -assert -multiclock dfflibmap -prepare -libert dfflibmap -prepare -liberty dlatchlibmap.lib equiv_opt -map dlatchlibmap-sim.v -assert -multiclock dfflibmap -map-only -liberty dlatchlibmap.lib +################################################################## + design -load orig dfflibmap -liberty dlatchlibmap.lib clean @@ -73,6 +75,8 @@ select -assert-count 1 t:dlatchn select -assert-count 4 t:dlatchsr select -assert-none t:dlatchn t:dlatchsr t:$_NOT_ %% %n t:* %i +################################################################## + design -load orig dfflibmap -liberty dlatchlibmap.lib -dont_use *latchn clean @@ -80,6 +84,12 @@ clean select -assert-count 0 t:dlatchn select -assert-count 5 t:dlatchsr +################################################################## + +design -load orig +read_liberty -lib dlatchlibmap.lib dlatchlibmap_dlatchsr_mixedpol.lib +equiv_opt -map dlatchlibmap-sim.v -map dlatchlibmap_dlatchsr_mixedpol-sim.v -assert -multiclock dfflibmap -liberty dlatchlibmap.lib -liberty dlatchlibmap_dlatchsr_mixedpol.lib -dont_use dlatchsr + design -load orig dfflibmap -liberty dlatchlibmap.lib -liberty dlatchlibmap_dlatchsr_mixedpol.lib -dont_use dlatchsr clean diff --git a/tests/techmap/dlatchlibmap_dlatchsr_h.lib b/tests/techmap/dlatchlibmap_dlatchsr_h.lib new file mode 100644 index 000000000..c9582cc96 --- /dev/null +++ b/tests/techmap/dlatchlibmap_dlatchsr_h.lib @@ -0,0 +1,34 @@ +library(test) { + cell (dlatchsr) { + area : 6; + latch("IQ", "IQN") { + data_in : "D"; + enable : "ENA"; + clear : "CLEAR"; + preset : "PRESET"; + clear_preset_var1 : H; + clear_preset_var2 : H; + } + pin(D) { + direction : input; + } + pin(ENA) { + direction : input; + clock : true; + } + pin(CLEAR) { + direction : input; + } + pin(PRESET) { + direction : input; + } + pin(Q) { + direction: output; + function : "IQ"; + } + pin(QN) { + direction: output; + function : "IQN"; + } + } +} diff --git a/tests/techmap/dlatchlibmap_dlatchsr_l.lib b/tests/techmap/dlatchlibmap_dlatchsr_l.lib new file mode 100644 index 000000000..7d438f612 --- /dev/null +++ b/tests/techmap/dlatchlibmap_dlatchsr_l.lib @@ -0,0 +1,34 @@ +library(test) { + cell (dlatchsr) { + area : 6; + latch("IQ", "IQN") { + data_in : "D"; + enable : "ENA"; + clear : "CLEAR"; + preset : "PRESET"; + clear_preset_var1 : L; + clear_preset_var2 : L; + } + pin(D) { + direction : input; + } + pin(ENA) { + direction : input; + clock : true; + } + pin(CLEAR) { + direction : input; + } + pin(PRESET) { + direction : input; + } + pin(Q) { + direction: output; + function : "IQ"; + } + pin(QN) { + direction: output; + function : "IQN"; + } + } +} diff --git a/tests/techmap/dlatchlibmap_dlatchsr_mixedpol-sim.v b/tests/techmap/dlatchlibmap_dlatchsr_mixedpol-sim.v new file mode 100644 index 000000000..0be00d357 --- /dev/null +++ b/tests/techmap/dlatchlibmap_dlatchsr_mixedpol-sim.v @@ -0,0 +1,10 @@ +module dlatchsr_mixedpol(input ENA, D, CLEAR, PRESET, output reg Q, output QN); + + always @* + if (PRESET) Q <= 1'b1; + else if (~CLEAR) Q <= 1'b0; + else if (ENA) Q <= ~D; + + assign QN = ~Q; + +endmodule diff --git a/tests/techmap/dlatchlibmap_formal.ys b/tests/techmap/dlatchlibmap_formal.ys index 135bfdc1a..7a0ca60c3 100644 --- a/tests/techmap/dlatchlibmap_formal.ys +++ b/tests/techmap/dlatchlibmap_formal.ys @@ -84,6 +84,82 @@ $_DLATCH_P_ latch0 (.E(E), .D(D), .Q(Q[0])); $_DLATCH_PP0_ latch1 (.E(E), .D(D), .R(R), .Q(Q[1])); $_DLATCH_PP1_ latch2 (.E(E), .D(D), .R(R), .Q(Q[2])); +assume property (~R || ~S); +$_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R( R), .S( S), .Q(Q[3])); +$_DLATCHSR_NNN_ latch4 (.E(E), .D(D), .R(~R), .S(~S), .Q(Q[4])); + +assign Q[9:5] = ~Q[4:0]; + +endmodule + +EOT + +proc +opt +read_liberty dlatchlibmap_dlatchsr_l.lib + +copy top top_unmapped +dfflibmap -liberty dlatchlibmap_dlatchsr_l.lib top + +clk2fflogic +flatten +opt_clean -purge +miter -equiv -make_assert -flatten top_unmapped top miter +hierarchy -top miter +# Prove that this is equivalent with the assumption +sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter +# Prove that this is NOT equivalent WITHOUT the assumption +sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter + +################################################################## + +design -reset +read_verilog -sv -icells <