luke
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Add latch tests, extend dff tests. 

Co-authored-by: Iztok Jeras <iztok.jeras@gmail.com>
This commit is contained in:
nella 2026-07-31 12:00:14 +02:00 committed by nella
parent e75e42c5d7
commit 9050446798
23 changed files with 1182 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
tests/techmap/dfflibmap.ys
View File

@ -23,9 +23,11 @@ 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
dfflibmap -liberty dfflibmap.lib
clean
@ -74,6 +76,8 @@ select -assert-count 1 t:dffe
select -assert-count 4 t:dffsr
select -assert-none t:dffn t:dffsr t:dffe t:$_NOT_ %% %n t:* %i
##################################################################
design -load orig
dfflibmap -liberty dfflibmap.lib -dont_use *ffn
clean
@ -82,6 +86,12 @@ select -assert-count 0 t:dffn
select -assert-count 5 t:dffsr
select -assert-count 1 t:dffe
##################################################################
design -load orig
read_liberty -lib dfflibmap.lib dfflibmap_dffsr_mixedpol.lib
equiv_opt -map dfflibmap-sim.v -map dfflibmap_dffsr_mixedpol-sim.v -assert -multiclock dfflibmap -liberty dfflibmap.lib -liberty dfflibmap_dffsr_mixedpol.lib -dont_use dffsr
design -load orig
dfflibmap -liberty dfflibmap.lib -liberty dfflibmap_dffsr_mixedpol.lib -dont_use dffsr
clean

33
tests/techmap/dfflibmap_dffsr_h.lib Normal file
View File

@ -0,0 +1,33 @@
library(test) {
cell (dffsr) {
area : 6;
ff("IQ", "IQN") {
next_state : "D";
clocked_on : "CLK";
clear : "CLEAR";
preset : "PRESET";
clear_preset_var1 : H;
clear_preset_var2 : H;
}
pin(D) {
direction : input;
}
pin(CLK) {
direction : input;
}
pin(CLEAR) {
direction : input;
}
pin(PRESET) {
direction : input;
}
pin(Q) {
direction: output;
function : "IQ";
}
pin(QN) {
direction: output;
function : "IQN";
}
}
}

33
tests/techmap/dfflibmap_dffsr_l.lib Normal file
View File

@ -0,0 +1,33 @@
library(test) {
cell (dffsr) {
area : 6;
ff("IQ", "IQN") {
next_state : "D";
clocked_on : "CLK";
clear : "CLEAR";
preset : "PRESET";
clear_preset_var1 : L;
clear_preset_var2 : L;
}
pin(D) {
direction : input;
}
pin(CLK) {
direction : input;
}
pin(CLEAR) {
direction : input;
}
pin(PRESET) {
direction : input;
}
pin(Q) {
direction: output;
function : "IQ";
}
pin(QN) {
direction: output;
function : "IQN";
}
}
}

10
tests/techmap/dfflibmap_dffsr_mixedpol-sim.v Normal file
View File

@ -0,0 +1,10 @@
module dffsr_mixedpol(input CLK, D, CLEAR, PRESET, output reg Q, output QN);
always @(posedge CLK, negedge CLEAR, posedge PRESET)
if (PRESET) Q <= 1'b1;
else if (~CLEAR) Q <= 1'b0;
else Q <= ~D;
assign QN = ~Q;
endmodule

80
tests/techmap/dfflibmap_formal.ys
View File

@ -88,6 +88,86 @@ $_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
assume property (~R || ~S);
$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
assign Q[11:6] = ~Q[5:0];
endmodule
EOT
proc
opt
read_liberty dfflibmap_dffsr_l.lib
copy top top_unmapped
dfflibmap -liberty dfflibmap_dffsr_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 <<EOT
module top(input C, D, E, S, R, output [11:0] Q);
$_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
assume property (~R || ~S);
$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
assign Q[11:6] = ~Q[5:0];
endmodule
EOT
proc
opt
read_liberty dfflibmap_dffsr_h.lib
copy top top_unmapped
dfflibmap -liberty dfflibmap_dffsr_h.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 C, D, E, S, R, output [11:0] Q);
$_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
// no assume when mapping to X
$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));

81
tests/techmap/dfflibmap_proc_formal.ys
View File

@ -5,36 +5,24 @@ read_verilog -sv -icells <<EOT
module top(input C, D, E, S, R, output [7:0] Q);
always @( posedge C, posedge S, posedge R)
if (R)
Q[0] <= 0;
else if (S)
Q[0] <= 1;
else
Q[0] <= D;
if (R) Q[0] <= 0;
else if (S) Q[0] <= 1;
else Q[0] <= D;
always @( posedge C, posedge S, posedge R)
if (S)
Q[1] <= 1;
else if (R)
Q[1] <= 0;
else
Q[1] <= D;
if (S) Q[1] <= 1;
else if (R) Q[1] <= 0;
else Q[1] <= D;
always @( posedge C, posedge S, posedge R)
if (R)
Q[2] <= 0;
else if (S)
Q[2] <= 1;
else if (E)
Q[2] <= D;
if (R) Q[2] <= 0;
else if (S) Q[2] <= 1;
else if (E) Q[2] <= D;
always @( posedge C, posedge S, posedge R)
if (S)
Q[3] <= 1;
else if (R)
Q[3] <= 0;
else if (E)
Q[3] <= D;
if (S) Q[3] <= 1;
else if (R) Q[3] <= 0;
else if (E) Q[3] <= D;
assign Q[7:4] = ~Q[3:0];
@ -81,6 +69,36 @@ sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
##################################################################
design -load start
logger -expect log " mapped 4" 1
dfflibmap -liberty dfflibmap_dffsr_l.lib top
logger -check-expected
read_liberty dfflibmap_dffsr_l.lib
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
##################################################################
design -load start
logger -expect log " mapped 4" 1
dfflibmap -liberty dfflibmap_dffsr_h.lib top
logger -check-expected
read_liberty dfflibmap_dffsr_h.lib
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
##################################################################
design -load start
logger -expect log " mapped 4" 1
dfflibmap -liberty dfflibmap_dffsr_mixedpol.lib top
@ -108,3 +126,18 @@ 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
##################################################################
design -load start
logger -expect log " mapped 4" 1
dfflibmap -liberty dfflibmap_dffsr_not_next_l.lib top
logger -check-expected
read_liberty dfflibmap_dffsr_not_next_l.lib
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

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

55
tests/techmap/dlatchlibmap.lib Normal file
View File

@ -0,0 +1,55 @@
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;
}
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;
}
pin(CLEAR) {
direction : input;
}
pin(PRESET) {
direction : input;
}
pin(Q) {
direction: output;
function : "IQ";
}
pin(QN) {
direction: output;
function : "IQN";
}
}
}

107
tests/techmap/dlatchlibmap.ys Normal file
View File

@ -0,0 +1,107 @@
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
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
# 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

23
tests/techmap/dlatchlibmap_dlatch_not_data.lib Normal file
View File

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

23
tests/techmap/dlatchlibmap_dlatchn.lib Normal file
View File

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

33
tests/techmap/dlatchlibmap_dlatchsr_h.lib Normal file
View File

@ -0,0 +1,33 @@
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;
}
pin(CLEAR) {
direction : input;
}
pin(PRESET) {
direction : input;
}
pin(Q) {
direction: output;
function : "IQ";
}
pin(QN) {
direction: output;
function : "IQN";
}
}
}

33
tests/techmap/dlatchlibmap_dlatchsr_l.lib Normal file
View File

@ -0,0 +1,33 @@
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;
}
pin(CLEAR) {
direction : input;
}
pin(PRESET) {
direction : input;
}
pin(Q) {
direction: output;
function : "IQ";
}
pin(QN) {
direction: output;
function : "IQN";
}
}
}

10
tests/techmap/dlatchlibmap_dlatchsr_mixedpol-sim.v Normal file
View File

@ -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

33
tests/techmap/dlatchlibmap_dlatchsr_mixedpol.lib Normal file
View File

@ -0,0 +1,33 @@
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;
}
pin(CLEAR) {
direction : input;
}
pin(PRESET) {
direction : input;
}
pin(Q) {
direction: output;
function : "IQ";
}
pin(QN) {
direction: output;
function : "IQN";
}
}
}

27
tests/techmap/dlatchlibmap_dlatchsr_not_data.lib Normal file
View File

@ -0,0 +1,27 @@
library (test_not_data) {
cell (dlatchsr_not_data) {
area : 1.0;
pin (Q) {
direction : output;
function : "STATE";
}
pin (ENA) {
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";
}
}
}

33
tests/techmap/dlatchlibmap_dlatchsr_not_data_l.lib Normal file
View File

@ -0,0 +1,33 @@
library(test) {
cell (dlatchsr_not_data_l) {
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;
}
pin(CLEAR) {
direction : input;
}
pin(PRESET) {
direction : input;
}
pin(Q) {
direction: output;
function : "IQ";
}
pin(QN) {
direction: output;
function : "IQN";
}
}
}

33
tests/techmap/dlatchlibmap_dlatchsr_r.lib Normal file
View File

@ -0,0 +1,33 @@
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;
}
pin(CLEAR) {
direction : input;
}
pin(PRESET) {
direction : input;
}
pin(Q) {
direction: output;
function : "IQ";
}
pin(QN) {
direction: output;
function : "IQN";
}
}
}

33
tests/techmap/dlatchlibmap_dlatchsr_s.lib Normal file
View File

@ -0,0 +1,33 @@
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;
}
pin(CLEAR) {
direction : input;
}
pin(PRESET) {
direction : input;
}
pin(Q) {
direction: output;
function : "IQ";
}
pin(QN) {
direction: output;
function : "IQN";
}
}
}

33
tests/techmap/dlatchlibmap_dlatchsr_x.lib Normal file
View File

@ -0,0 +1,33 @@
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;
}
pin(CLEAR) {
direction : input;
}
pin(PRESET) {
direction : input;
}
pin(Q) {
direction: output;
function : "IQ";
}
pin(QN) {
direction: output;
function : "IQN";
}
}
}

325
tests/techmap/dlatchlibmap_formal.ys Normal file
View File

@ -0,0 +1,325 @@
##################################################################
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]));
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 <<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_h.lib
copy top top_unmapped
dfflibmap -liberty dlatchlibmap_dlatchsr_h.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
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

133
tests/techmap/dlatchlibmap_proc_formal.ys Normal file
View File

@ -0,0 +1,133 @@
##################################################################
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
techmap
copy top top_unmapped
design -save start
##################################################################
design -load start
logger -expect log " mapped 2" 1
dfflibmap -liberty dlatchlibmap_dlatchsr_s.lib top
logger -check-expected
read_liberty dlatchlibmap_dlatchsr_s.lib
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
##################################################################
design -load start
logger -expect log " mapped 2" 1
dfflibmap -liberty dlatchlibmap_dlatchsr_r.lib top
logger -check-expected
read_liberty dlatchlibmap_dlatchsr_r.lib
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
##################################################################
design -load start
logger -expect log " mapped 2" 1
dfflibmap -liberty dlatchlibmap_dlatchsr_l.lib top
logger -check-expected
read_liberty dlatchlibmap_dlatchsr_l.lib
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
##################################################################
design -load start
logger -expect log " mapped 2" 1
dfflibmap -liberty dlatchlibmap_dlatchsr_h.lib top
logger -check-expected
read_liberty dlatchlibmap_dlatchsr_h.lib
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
##################################################################
design -load start
logger -expect log " mapped 2" 1
dfflibmap -liberty dlatchlibmap_dlatchsr_mixedpol.lib top
logger -check-expected
read_liberty dlatchlibmap_dlatchsr_mixedpol.lib
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
##################################################################
design -load start
logger -expect log " mapped 2" 1
dfflibmap -liberty dlatchlibmap_dlatchsr_not_data.lib top
logger -check-expected
read_liberty dlatchlibmap_dlatchsr_not_data.lib
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
##################################################################
design -load start
logger -expect log " mapped 2" 1
dfflibmap -liberty dlatchlibmap_dlatchsr_not_data_l.lib top
logger -check-expected
read_liberty dlatchlibmap_dlatchsr_not_data_l.lib
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

5
tests/techmap/dlatchlibmap_wide.ys Normal file
View File

@ -0,0 +1,5 @@
read_verilog ../sim/dlatch.v
proc
logger -expect error "not supported" 1
dfflibmap -liberty dlatchlibmap.lib
logger -check-expected