mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-02-14 21:01:50 +00:00
Code Activity

Merge cbf3407585 into e4b32d6aae

Browse source
This commit is contained in:
Emil J 2026-02-12 17:12:04 +01:00 • committed by GitHub
commit 2766f9331e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
8 changed files with 246 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

4
tests/techmap/dfflibmap.ys
View file

@ -64,8 +64,8 @@ select -assert-count 1 t:dffe
select -assert-none t:dffn t:dffsr t:dffe t:$_NOT_ %% %n t:* %i
design -load orig
dfflibmap -prepare -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr.lib
dfflibmap -map-only -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr.lib
dfflibmap -prepare -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_r.lib
dfflibmap -map-only -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_r.lib
clean
select -assert-count 5 t:$_NOT_

6
tests/techmap/dfflibmap_dffsr.lib → tests/techmap/dfflibmap_dffsr_r.lib
View file

@ -7,8 +7,8 @@ library(test) {
clear : "CLEAR";
preset : "PRESET";
clear_preset_var1 : L;
clear_preset_var2 : L;
}
clear_preset_var2 : H;
}
pin(D) {
direction : input;
}
@ -28,6 +28,6 @@ library(test) {
pin(QN) {
direction: output;
function : "IQN";
}
}
}
}

33
tests/techmap/dfflibmap_dffsr_s.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 : 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";
}
}
}

72
tests/techmap/dfflibmap_formal.ys
View file

@ -8,6 +8,78 @@ $_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]));
$_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_s.lib
copy top top_unmapped
dfflibmap -liberty dfflibmap_dffsr_s.lib top
async2sync
flatten
opt_clean -purge
equiv_make top top_unmapped equiv
equiv_induct equiv
equiv_status -assert equiv
##################################################################
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]));
$_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_r.lib
copy top top_unmapped
dfflibmap -liberty dfflibmap_dffsr_r.lib top
async2sync
flatten
opt_clean -purge
equiv_make top top_unmapped equiv
equiv_induct equiv
equiv_status -assert equiv
##################################################################
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]));
// Formal checking of directly instantiated DFFSR doesn't work at the moment
// likely due to an equiv_induct assume bug #5196

99
tests/techmap/dfflibmap_proc_formal.ys Normal file
View file

@ -0,0 +1,99 @@
##################################################################
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;
always @( posedge C, posedge S, posedge R)
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;
always @( posedge C, posedge S, posedge R)
if (S)
Q[3] <= 1;
else if (R)
Q[3] <= 0;
else if (E)
Q[3] <= D;
assign Q[7:4] = ~Q[3:0];
endmodule
EOT
proc
opt
read_liberty dfflibmap_dffsr_s.lib
copy top top_unmapped
dfflibmap -liberty dfflibmap_dffsr_s.lib top
async2sync
flatten
opt_clean -purge
equiv_make top top_unmapped equiv
equiv_induct equiv
equiv_status -assert equiv
##################################################################
delete top equiv
copy top_unmapped top
dfflibmap -liberty dfflibmap_dffsr_r.lib top
async2sync
flatten
opt_clean -purge
equiv_make top top_unmapped equiv
equiv_induct equiv
equiv_status -assert equiv
##################################################################
delete top equiv
copy top_unmapped top
dfflibmap -liberty dfflibmap_dffsr_mixedpol.lib top
async2sync
flatten
opt_clean -purge
equiv_make top top_unmapped equiv
equiv_induct equiv
equiv_status -assert equiv
##################################################################
delete top equiv
copy top_unmapped top
dfflibmap -liberty dfflibmap_dffsr_not_next.lib top
async2sync
flatten
opt_clean -purge
equiv_make top top_unmapped equiv
equiv_induct equiv
equiv_status -assert equiv