mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-07-23 15:42:32 +00:00
Code Activity

Merge 94d10012e7 into dddf137888

Browse source
This commit is contained in:
Iztok Jeras 2026-07-13 14:23:52 +02:00 • committed by GitHub
commit c3c7078112
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
19 changed files with 1130 additions and 236 deletions
Download patch file Download diff file Expand all files Collapse all files

66
tests/liberty/dff.log.ok
View file

@ -1,29 +1,47 @@
-- Running command `dfflibmap -info -liberty dff.lib' --
1. Executing DFFLIBMAP pass (mapping DFF cells to sequential cells from liberty file).
1. Executing DFFLIBMAP pass (mapping DFF/DLATCH cells to sequential cells from liberty file).
cell dff (noninv, pins=3, area=1.00) is a direct match for cell type $_DFF_P_.
final dff cell mappings:
unmapped dff cell: $_DFF_N_
final dff/dlatch cell mappings:
unmapped dff/dlatch cell: $_DFF_N_
\dff _DFF_P_ (.CLK( C), .D( D), .Q( Q));
unmapped dff cell: $_DFF_NN0_
unmapped dff cell: $_DFF_NN1_
unmapped dff cell: $_DFF_NP0_
unmapped dff cell: $_DFF_NP1_
unmapped dff cell: $_DFF_PN0_
unmapped dff cell: $_DFF_PN1_
unmapped dff cell: $_DFF_PP0_
unmapped dff cell: $_DFF_PP1_
unmapped dff cell: $_DFFE_NN_
unmapped dff cell: $_DFFE_NP_
unmapped dff cell: $_DFFE_PN_
unmapped dff cell: $_DFFE_PP_
unmapped dff cell: $_DFFSR_NNN_
unmapped dff cell: $_DFFSR_NNP_
unmapped dff cell: $_DFFSR_NPN_
unmapped dff cell: $_DFFSR_NPP_
unmapped dff cell: $_DFFSR_PNN_
unmapped dff cell: $_DFFSR_PNP_
unmapped dff cell: $_DFFSR_PPN_
unmapped dff cell: $_DFFSR_PPP_
dfflegalize command line: dfflegalize -cell $_DFF_P_ 01 t:$_DFF* t:$_SDFF*
unmapped dff/dlatch cell: $_DFF_NN0_
unmapped dff/dlatch cell: $_DFF_NN1_
unmapped dff/dlatch cell: $_DFF_NP0_
unmapped dff/dlatch cell: $_DFF_NP1_
unmapped dff/dlatch cell: $_DFF_PN0_
unmapped dff/dlatch cell: $_DFF_PN1_
unmapped dff/dlatch cell: $_DFF_PP0_
unmapped dff/dlatch cell: $_DFF_PP1_
unmapped dff/dlatch cell: $_DFFE_NN_
unmapped dff/dlatch cell: $_DFFE_NP_
unmapped dff/dlatch cell: $_DFFE_PN_
unmapped dff/dlatch cell: $_DFFE_PP_
unmapped dff/dlatch cell: $_DFFSR_NNN_
unmapped dff/dlatch cell: $_DFFSR_NNP_
unmapped dff/dlatch cell: $_DFFSR_NPN_
unmapped dff/dlatch cell: $_DFFSR_NPP_
unmapped dff/dlatch cell: $_DFFSR_PNN_
unmapped dff/dlatch cell: $_DFFSR_PNP_
unmapped dff/dlatch cell: $_DFFSR_PPN_
unmapped dff/dlatch cell: $_DFFSR_PPP_
unmapped dff/dlatch cell: $_DLATCH_N_
unmapped dff/dlatch cell: $_DLATCH_P_
unmapped dff/dlatch cell: $_DLATCH_NN0_
unmapped dff/dlatch cell: $_DLATCH_NN1_
unmapped dff/dlatch cell: $_DLATCH_NP0_
unmapped dff/dlatch cell: $_DLATCH_NP1_
unmapped dff/dlatch cell: $_DLATCH_PN0_
unmapped dff/dlatch cell: $_DLATCH_PN1_
unmapped dff/dlatch cell: $_DLATCH_PP0_
unmapped dff/dlatch cell: $_DLATCH_PP1_
unmapped dff/dlatch cell: $_DLATCHSR_NNN_
unmapped dff/dlatch cell: $_DLATCHSR_NNP_
unmapped dff/dlatch cell: $_DLATCHSR_NPN_
unmapped dff/dlatch cell: $_DLATCHSR_NPP_
unmapped dff/dlatch cell: $_DLATCHSR_PNN_
unmapped dff/dlatch cell: $_DLATCHSR_PNP_
unmapped dff/dlatch cell: $_DLATCHSR_PPN_
unmapped dff/dlatch cell: $_DLATCHSR_PPP_
dfflegalize command line: dfflegalize -cell $_DFF_P_ 01 t:$_DFF* t:$_SDFF* t:$_DLATCH*

2
tests/techmap/dfflibmap.ys
View file

@ -23,7 +23,7 @@ read_liberty -lib dfflibmap.lib
equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -liberty dfflibmap.lib
equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -prepare -liberty dfflibmap.lib
dfflibmap -prepare -liberty dffl*bmap.lib
dfflibmap -prepare -liberty dfflibmap.lib
equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -map-only -liberty dfflibmap.lib
design -load orig

19
tests/techmap/dlatchlibmap-sim.v Normal file
View file

@ -0,0 +1,19 @@
module dlatchn(input ENA, D, output reg Q, output QN);
always @*
if (~ENA) Q <= D;
assign QN = ~Q;
endmodule
module dlatchsr(input ENA, D, CLEAR, PRESET, output reg Q, output QN);
always @*
if (CLEAR) Q <= 1'b0;
else if (PRESET) Q <= 1'b1;
else if (ENA) Q <= D;
assign QN = ~Q;
endmodule

57
tests/techmap/dlatchlibmap.lib Normal file
View file

@ -0,0 +1,57 @@
library(test) {
/* D-type latch with reset and preset */
cell (dlatchn) {
area : 6;
latch("IQ", "IQN") {
data_in : "D";
enable : "!ENA";
}
pin(D) {
direction : input;
}
pin(ENA) {
direction : input;
clock : true;
}
pin(Q) {
direction: output;
function : "IQ";
}
pin(QN) {
direction: output;
function : "IQN";
}
}
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";
}
}
}

97
tests/techmap/dlatchlibmap.ys Normal file
View file

@ -0,0 +1,97 @@
read_verilog -icells <<EOT
module top(input E, D, S, R, output [9:0] Q);
$_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]));
$_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
simplemap
design -save orig
read_liberty -lib dlatchlibmap.lib
equiv_opt -map dlatchlibmap-sim.v -assert -multiclock dfflibmap -liberty dlatchlibmap.lib
equiv_opt -map dlatchlibmap-sim.v -assert -multiclock dfflibmap -prepare -liberty dlatchlibmap.lib
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
select -assert-count 4 t:$_NOT_
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 -prepare -liberty dlatchlibmap.lib
select -assert-count 9 t:$_NOT_
select -assert-count 1 t:$_DLATCH_N_
select -assert-count 4 t:$_DLATCHSR_PPP_
select -assert-none t:$_DLATCH_N_ t:$_DLATCHSR_PPP_ t:$_NOT_ %% %n t:* %i
design -load orig
dfflibmap -map-only -liberty dlatchlibmap.lib
select -assert-count 5 t:$_NOT_
select -assert-count 0 t:dlatchn
select -assert-count 1 t:dlatchsr
select -assert-count 1 t:$_DLATCH_P_
select -assert-count 1 t:$_DLATCH_PP0_
select -assert-count 1 t:$_DLATCH_PP1_
select -assert-count 1 t:$_DLATCHSR_NNN_
design -load orig
dfflibmap -prepare -liberty dlatchlibmap.lib
dfflibmap -map-only -liberty dlatchlibmap.lib
clean
select -assert-count 4 t:$_NOT_
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 -prepare -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatchsr_r.lib
dfflibmap -map-only -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatchsr_r.lib
clean
select -assert-count 4 t:$_NOT_
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
select -assert-count 0 t:dlatchn
select -assert-count 5 t:dlatchsr
design -load orig
dfflibmap -liberty dlatchlibmap.lib -liberty dlatchlibmap_dlatchsr_mixedpol.lib -dont_use dlatchsr
clean
# We have one more _NOT_ than with the regular dlatchsr
select -assert-count 5 t:$_NOT_
select -assert-count 1 t:dlatchn
select -assert-count 4 t:dlatchsr_mixedpol
# The additional NOT is on latch2.
# Originally, latch2.R is an active high "preset".
# dlatchsr_mixedpol has functionally swapped labels due to the data_in inversion,
# so we use its CLEAR port for the "preset",
# but we have to invert it because the CLEAR pin is active low.
# latch2.CLEAR = !R
select -assert-count 1 c:latch2 %x:+[CLEAR] %ci t:$_NOT_ %i

24
tests/techmap/dlatchlibmap_dlatch_not_data.lib Normal file
View file

@ -0,0 +1,24 @@
library (test_not_data) {
cell (dff_not_data) {
area: 1.0;
pin (QN) {
direction : output;
function : "STATE";
}
pin (ENA) {
direction : input;
clock : true;
}
pin (D) {
direction : input;
}
pin (RN) {
direction : input;
}
latch (STATE, STATEN) {
enable: "ENA";
data_in: "!D";
preset : "!RN";
}
}
}

24
tests/techmap/dlatchlibmap_dlatchn.lib Normal file
View file

@ -0,0 +1,24 @@
library(test) {
cell (dlatchn) {
area : 6;
latch("IQ", "IQN") {
data_in : "D";
enable : "!ENA";
}
pin(D) {
direction : input;
}
pin(ENA) {
direction : input;
clock : true;
}
pin(Q) {
direction: output;
function : "IQ";
}
pin(QN) {
direction: output;
function : "IQN";
}
}
}

34
tests/techmap/dlatchlibmap_dlatchsr_mixedpol.lib Normal file
View file

@ -0,0 +1,34 @@
library(test) {
cell (dlatchsr_mixedpol) {
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";
}
}
}

28
tests/techmap/dlatchlibmap_dlatchsr_not_data.lib Normal file
View file

@ -0,0 +1,28 @@
library (test_not_data) {
cell (dlatchsr_not_data) {
area : 1.0;
pin (Q) {
direction : output;
function : "STATE";
}
pin (ENA) {
clock : true;
direction : input;
}
pin (D) {
direction : input;
}
pin (RN) {
direction : input;
}
pin (SN) {
direction : input;
}
latch (STATE,STATEN) {
clear : "!SN";
enable : "ENA";
data_in : "!D";
preset : "!RN";
}
}
}

34
tests/techmap/dlatchlibmap_dlatchsr_not_data_l.lib Normal file
View file

@ -0,0 +1,34 @@
library(test) {
cell (dlatchr_not_data) {
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";
}
}
}

34
tests/techmap/dlatchlibmap_dlatchsr_r.lib Normal file
View file

@ -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 : 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";
}
}
}

34
tests/techmap/dlatchlibmap_dlatchsr_s.lib Normal file
View file

@ -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 : 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";
}
}
}

34
tests/techmap/dlatchlibmap_dlatchsr_x.lib Normal file
View file

@ -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 : X;
clear_preset_var2 : X;
}
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";
}
}
}

250
tests/techmap/dlatchlibmap_formal.ys Normal file
View file

@ -0,0 +1,250 @@
##################################################################
read_verilog -sv -icells <<EOT
module top(input E, D, S, R, output [9:0] Q);
$_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_s.lib
copy top top_unmapped
dfflibmap -liberty dlatchlibmap_dlatchsr_s.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 <<EOT
module top(input E, D, S, R, output [9:0] Q);
$_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_r.lib
copy top top_unmapped
dfflibmap -liberty dlatchlibmap_dlatchsr_r.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 <<EOT
module top(input E, D, S, R, output [9:0] Q);
$_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]));
// no assume when mapping to X
$_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_x.lib
opt
copy top top_unmapped
dfflibmap -liberty dlatchlibmap_dlatchsr_x.lib top
clk2fflogic
flatten
opt_clean -purge
miter -equiv -make_assert -flatten top_unmapped top miter
hierarchy -top miter
# Prove that this is equivalent
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
##################################################################
design -reset
read_verilog -sv -icells <<EOT
module top(input E, D, S, R, output [9:0] Q);
$_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]));
// no assume when mapping to unset clear_preset_var
$_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_dlatchn.lib
read_liberty dlatchlibmap_dlatchsr_not_data.lib
copy top top_unmapped
dfflibmap -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatchsr_not_data.lib top
clk2fflogic
flatten
opt_clean -purge
miter -equiv -make_assert -flatten top_unmapped top miter
hierarchy -top miter
# Prove that this is equivalent
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
##################################################################
design -reset
read_verilog -sv -icells <<EOT
module top(input E, D, S, R, output [9:0] Q);
$_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_not_data_l.lib
copy top top_unmapped
dfflibmap -liberty dlatchlibmap_dlatchsr_not_data_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 <<EOT
module top(input E, D, S, R, output Q);
// DLATCHSR with priority R over S
always @*
if (R) Q <= 1'b0;
else if (S) Q <= 1'b1;
else if (E) Q <= D;
endmodule
EOT
proc
opt
read_liberty dlatchlibmap_dlatchn.lib
read_liberty dlatchlibmap_dlatchsr_not_data.lib
copy top top_unmapped
simplemap top
dfflibmap -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatchsr_not_data.lib top
clk2fflogic
flatten
opt_clean -purge
equiv_make top top_unmapped equiv
equiv_induct -set-assumes equiv
equiv_status -assert equiv
##################################################################
design -reset
read_verilog <<EOT
module top(input E, D, R, output Q);
// DLATCH with preset
always @*
if (~R) Q <= 1'b1;
else if (E) Q <= D;
endmodule
EOT
proc
opt
read_liberty dlatchlibmap_dlatchn.lib
read_liberty dlatchlibmap_dlatch_not_data.lib
copy top top_unmapped
simplemap top
dfflibmap -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatch_not_data.lib top
clk2fflogic
flatten
opt_clean -purge
equiv_make top top_unmapped equiv
equiv_induct -set-assumes equiv
equiv_status -assert equiv

78
tests/techmap/dlatchlibmap_proc_formal.ys Normal file
View file

@ -0,0 +1,78 @@
##################################################################
read_verilog -sv -icells <<EOT
module top(input E, D, S, R, output [3:0] Q);
always_latch
if (R) Q[0] <= 1'b0;
else if (S) Q[0] <= 1'b1;
else if (E) Q[0] <= D;
always_latch
if (S) Q[1] <= 1'b1;
else if (R) Q[1] <= 1'b0;
else if (E) Q[1] <= D;
assign Q[3:2] = ~Q[1:0];
endmodule
EOT
proc
opt
read_liberty dlatchlibmap_dlatchsr_s.lib
copy top top_unmapped
dfflibmap -liberty dlatchlibmap_dlatchsr_s.lib top
clk2fflogic
flatten
opt_clean -purge
miter -equiv -make_assert -flatten top_unmapped top miter
# Prove that this is equivalent
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
##################################################################
delete top miter
copy top_unmapped top
dfflibmap -liberty dlatchlibmap_dlatchsr_r.lib top
clk2fflogic
flatten
miter -equiv -make_assert -flatten top_unmapped top miter
# Prove that this is equivalent
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
##################################################################
delete top miter
copy top_unmapped top
dfflibmap -liberty dlatchlibmap_dlatchsr_mixedpol.lib top
clk2fflogic
flatten
miter -equiv -make_assert -flatten top_unmapped top miter
# Prove that this is equivalent
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
##################################################################
delete top miter
copy top_unmapped top
dfflibmap -liberty dlatchlibmap_dlatchsr_not_data.lib top
clk2fflogic
flatten
miter -equiv -make_assert -flatten top_unmapped top miter
# Prove that this is equivalent
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter