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

dfflibmap: extended tests with same testcases as dlatchmap

This commit is contained in:
Iztok Jeras 2026-07-15 06:08:54 +02:00
parent 92d4f60977
commit 64ef4babf3
9 changed files with 229 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
tests/techmap/dfflibmap.ys
View File

@ -26,6 +26,8 @@ equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -prepare -liberty d
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,13 @@ 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
stat
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

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

@ -0,0 +1,34 @@
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;
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/dfflibmap_dffsr_l.lib Normal file
View File

@ -0,0 +1,34 @@
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;
clock : true;
}
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

1
tests/techmap/dfflibmap_dffsr_r.lib
View File

@ -14,6 +14,7 @@ library(test) {
}
pin(CLK) {
direction : input;
clock : true;
}
pin(CLEAR) {
direction : input;

1
tests/techmap/dfflibmap_dffsr_s.lib
View File

@ -14,6 +14,7 @@ library(test) {
}
pin(CLK) {
direction : input;
clock : true;
}
pin(CLEAR) {
direction : input;

1
tests/techmap/dfflibmap_dffsr_x.lib
View File

@ -14,6 +14,7 @@ library(test) {
}
pin(CLK) {
direction : input;
clock : true;
}
pin(CLEAR) {
direction : input;

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]));

83
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];
@ -44,9 +32,10 @@ EOT
proc
opt
read_liberty dfflibmap_dffsr_s.lib
copy top top_unmapped
##################################################################
dfflibmap -liberty dfflibmap_dffsr_s.lib top
clk2fflogic
@ -75,6 +64,34 @@ sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
delete top miter
copy top_unmapped top
dfflibmap -liberty dfflibmap_dffsr_l.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 dfflibmap_dffsr_h.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 dfflibmap_dffsr_mixedpol.lib top
@ -98,3 +115,17 @@ 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 dfflibmap_dffsr_not_next_l.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