3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-07-17 12:45:44 +00:00

Merge remote-tracking branch 'upstream/main' into silimate

This commit is contained in:
Mohamed Gaber 2026-06-09 16:22:51 +03:00
commit e58125b605
No known key found for this signature in database
834 changed files with 25281 additions and 8780 deletions

View file

@ -0,0 +1,19 @@
read_verilog -icells -specify <<EOT
(* abc9_box, blackbox *)
module box1(input i, output o);
specify
(i => o) = 1;
endspecify
endmodule
module top(input i, output o);
wire a, b, c, z;
$_AND_ a0(.A(b), .B(i), .Y(a));
$_AND_ b0(.A(a), .B(c), .Y(b));
$_AND_ c0(.A(b), .B(i), .Y(c));
box1 u_box(.i(i), .o(z));
assign o = c ^ z;
endmodule
EOT
abc9 -lut 4

View file

@ -17,7 +17,8 @@ design -save gold
abc9 -lut 4
design -load gold
abc9 -lut 4 -fast
scratchpad -copy abc9.script.default.fast abc9.script
abc9 -lut 4
design -load gold
scratchpad -copy abc9.script.default.area abc9.script

View file

@ -1,28 +0,0 @@
&st
&dch -r
&nf
&st
&syn2
&if -g -K 6
&synch2 -r
&nf
&st
&syn2
&if -g -K 6
&synch2 -r
&nf
&st
&syn2
&if -g -K 6
&synch2 -r
&nf
&st
&syn2
&if -g -K 6
&synch2 -r
&nf
&st
&syn2
&if -g -K 6
&synch2 -r
&nf

View file

@ -5,7 +5,7 @@ if ! which timeout ; then
exit 0
fi
if ! timeout 10 ../../yosys bug5495.v -p 'hierarchy; techmap; abc -script bug5495.abc' ; then
if ! timeout 10 ${YOSYS} bug5495.v -p 'hierarchy; techmap; abc -script bug5495.abc' ; then
echo "Yosys failed to complete"
exit 1
fi

View file

@ -6,6 +6,7 @@ library(test) {
pin (GCLK) {
clock_gate_out_pin : true;
direction : output;
function : "CLK&CE";
}
pin (CLK) {
clock_gate_clock_pin : true;
@ -26,6 +27,7 @@ library(test) {
pin (GCLK) {
clock_gate_out_pin : true;
direction : output;
function : "CLK&CE";
}
pin (CLK) {
clock_gate_clock_pin : true;
@ -42,6 +44,7 @@ library(test) {
pin (GCLK) {
clock_gate_out_pin : true;
direction : output;
function : "CLK&CE";
}
pin (CLK) {
clock_gate_clock_pin : true;
@ -58,6 +61,7 @@ library(test) {
pin (GCLK) {
clock_gate_out_pin : true;
direction : output;
function : "CLK|!CE";
}
pin (CLK) {
clock_gate_clock_pin : true;
@ -74,6 +78,7 @@ library(test) {
pin (GCLK) {
clock_gate_out_pin : true;
direction : output;
function : "CLK|!CE";
}
pin (CLK) {
clock_gate_clock_pin : true;
@ -94,6 +99,7 @@ library(test) {
pin (GCLK) {
clock_gate_out_pin : true;
direction : output;
function : "CLK|!CE";
}
pin (CLK) {
clock_gate_clock_pin : true;

View file

@ -1,53 +1,7 @@
read_verilog << EOT
module dffe_00( input clk, en,
input d1, output reg q1,
);
always @( negedge clk ) begin
if ( ~en )
q1 <= d1;
end
endmodule
module dffe_01( input clk, en,
input d1, output reg q1,
);
always @( negedge clk ) begin
if ( en )
q1 <= d1;
end
endmodule
module dffe_10( input clk, en,
input d1, output reg q1,
);
always @( posedge clk ) begin
if ( ~en )
q1 <= d1;
end
endmodule
module dffe_11( input clk, en,
input d1, output reg q1,
);
always @( posedge clk ) begin
if ( en )
q1 <= d1;
end
endmodule
module dffe_wide_11( input clk, en,
input [3:0] d1, output reg [3:0] q1,
);
always @( posedge clk ) begin
if ( en )
q1 <= d1;
end
endmodule
EOT
proc
yosys -import
read_verilog clockgate.v
read_verilog ../sim/sdffe.v
yosys proc
opt
design -save before
@ -128,41 +82,7 @@ select -module dffe_11 -assert-count 0 t:\\pdk_icg
#------------------------------------------------------------------------------
design -reset
read_rtlil << EOT
module \bad1
wire input 1 \clk
wire input 3 \d1
wire input 2 \en
wire output 4 \q1
cell $dffe $auto$ff.cc:266:slice$27
parameter \CLK_POLARITY 1
parameter \EN_POLARITY 1
parameter \WIDTH 1
connect \CLK \clk
connect \D \d1
connect \EN 1'1
connect \Q \q1
end
end
module \bad2
wire input 1 \clk
wire input 3 \d1
wire input 2 \en
wire output 4 \q1
cell $dffe $auto$ff.cc:266:slice$27
parameter \CLK_POLARITY 1
parameter \EN_POLARITY 1
parameter \WIDTH 1
connect \CLK 1'1
connect \D \d1
connect \EN \en
connect \Q \q1
end
end
EOT
read_rtlil clockgate_bad.il
# Check we don't choke on constants
clockgate -pos pdk_icg ce:clkin:clkout -tie_lo scanen
@ -173,19 +93,8 @@ select -module bad2 -assert-count 0 t:\\pdk_icg
# Regression test: EN is a bit from a multi-bit wire
design -reset
read_verilog << EOT
module dffe_wide_11( input clk, input [1:0] en,
input [3:0] d1, output reg [3:0] q1,
);
always @( posedge clk ) begin
if ( en[0] )
q1 <= d1;
end
endmodule
EOT
proc
read_verilog clockgate_wide.v
yosys proc
opt
clockgate -pos pdk_icg ce:clkin:clkout -tie_lo scanen
@ -193,8 +102,18 @@ select -assert-count 1 t:\\pdk_icg
#------------------------------------------------------------------------------
design -load before
clockgate -liberty c*ckgate.lib
design -reset
read_liberty c*ckgate.lib
design -save map
foreach mod {dffe_00 dffe_01 dffe_10 dffe_11} {
design -load before
hierarchy -top $mod
read_liberty -lib c*ckgate.lib
equiv_opt -map %map -multiclock clockgate -liberty c*ckgate.lib
design -load postopt
design -copy-to final $mod
}
design -load final
# rising edge ICGs
select -module dffe_00 -assert-count 0 t:\\pos_small
@ -276,6 +195,9 @@ select -module dffe_11 -assert-count 0 t:\\neg_small_tielo
select -module dffe_10 -assert-count 1 t:\$_NOT_
select -module dffe_11 -assert-count 0 t:\$_NOT_
# $sdffe is not gated
select -module sdffe -assert-count 0 sdffe t:* t:\$sdffe %d
#------------------------------------------------------------------------------
design -load before

44
tests/techmap/clockgate.v Normal file
View file

@ -0,0 +1,44 @@
module dffe_00( input clk, en,
input d1, output reg q1,
);
always @( negedge clk ) begin
if ( ~en )
q1 <= d1;
end
endmodule
module dffe_01( input clk, en,
input d1, output reg q1,
);
always @( negedge clk ) begin
if ( en )
q1 <= d1;
end
endmodule
module dffe_10( input clk, en,
input d1, output reg q1,
);
always @( posedge clk ) begin
if ( ~en )
q1 <= d1;
end
endmodule
module dffe_11( input clk, en,
input d1, output reg q1,
);
always @( posedge clk ) begin
if ( en )
q1 <= d1;
end
endmodule
module dffe_wide_11( input clk, en,
input [3:0] d1, output reg [3:0] q1,
);
always @( posedge clk ) begin
if ( en )
q1 <= d1;
end
endmodule

View file

@ -0,0 +1,31 @@
module \bad1
wire input 1 \clk
wire input 3 \d1
wire input 2 \en
wire output 4 \q1
cell $dffe $auto$ff.cc:266:slice$27
parameter \CLK_POLARITY 1
parameter \EN_POLARITY 1
parameter \WIDTH 1
connect \CLK \clk
connect \D \d1
connect \EN 1'1
connect \Q \q1
end
end
module \bad2
wire input 1 \clk
wire input 3 \d1
wire input 2 \en
wire output 4 \q1
cell $dffe $auto$ff.cc:266:slice$27
parameter \CLK_POLARITY 1
parameter \EN_POLARITY 1
parameter \WIDTH 1
connect \CLK 1'1
connect \D \d1
connect \EN \en
connect \Q \q1
end
end

View file

@ -0,0 +1,8 @@
module dffe_wide_11( input clk, input [1:0] en,
input [3:0] d1, output reg [3:0] q1,
);
always @( posedge clk ) begin
if ( en[0] )
q1 <= d1;
end
endmodule

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_

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

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

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

View file

@ -8,13 +8,132 @@ $_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
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]));
// // Workaround for DFFSR bug #5194
// 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_s.lib
copy top top_unmapped
dfflibmap -liberty dfflibmap_dffsr_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 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_r.lib
copy top top_unmapped
dfflibmap -liberty dfflibmap_dffsr_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 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]));
$_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_x.lib
opt
copy top top_unmapped
dfflibmap -liberty dfflibmap_dffsr_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 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 -set-assumes assume bug #5196
// no assume when mapping to unset clear_preset_var
$_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]));
@ -32,12 +151,14 @@ read_liberty dfflibmap_dffsr_not_next.lib
copy top top_unmapped
dfflibmap -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_not_next.lib top
async2sync
clk2fflogic
flatten
opt_clean -purge
equiv_make top top_unmapped equiv
equiv_induct equiv
equiv_status -assert equiv
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
##################################################################
@ -50,13 +171,9 @@ $_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
// // Workaround for DFFSR bug #5194
// 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]));
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]));
@ -68,17 +185,21 @@ EOT
proc
opt
read_liberty dfflibmap_dffr_not_next.lib
read_liberty dfflibmap_dffsr_not_next_l.lib
copy top top_unmapped
dfflibmap -liberty dfflibmap_dffr_not_next.lib top
dfflibmap -liberty dfflibmap_dffsr_not_next_l.lib top
async2sync
clk2fflogic
flatten
opt_clean -purge
equiv_make top top_unmapped equiv
equiv_induct equiv
equiv_status -assert equiv
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
##################################################################
@ -108,11 +229,11 @@ copy top top_unmapped
simplemap top
dfflibmap -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_not_next.lib top
async2sync
clk2fflogic
flatten
opt_clean -purge
equiv_make top top_unmapped equiv
equiv_induct equiv
equiv_induct -set-assumes equiv
equiv_status -assert equiv
##################################################################
@ -139,9 +260,9 @@ copy top top_unmapped
simplemap top
dfflibmap -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dff_not_next.lib top
async2sync
clk2fflogic
flatten
opt_clean -purge
equiv_make top top_unmapped equiv
equiv_induct equiv
equiv_induct -set-assumes equiv
equiv_status -assert equiv

View file

@ -0,0 +1,100 @@
##################################################################
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
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 dfflibmap_dffsr_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 dfflibmap_dffsr_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 dfflibmap_dffsr_not_next.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

View file

@ -0,0 +1,8 @@
#!/usr/bin/env python3
import sys
sys.path.append("..")
import gen_tests_makefile
gen_tests_makefile.generate(["--yosys-scripts", "--tcl-scripts", "--bash", "--yosys-args", "-e 'select out of bounds'"])

View file

@ -1,3 +1,3 @@
#!/usr/bin/env bash
exec ../tools/autotest.sh -G -j $@ -p 'proc; opt; memory -nomap; techmap -map ../mem_simple_4x1_map.v;; techmap; opt; abc;; stat' mem_simple_4x1_uut.v
exec ../tools/autotest.sh -G -Y ${YOSYS} -j $@ -p 'proc; opt; memory -nomap; techmap -map ../mem_simple_4x1_map.v;; techmap; opt; abc;; stat' mem_simple_4x1_uut.v

View file

@ -1,3 +1,3 @@
set -e
../../yosys -p 'read_verilog recursive.v; hierarchy -top top; techmap -map recursive_map.v -max_iter 1; select -assert-count 2 t:sub; select -assert-count 2 t:bar'
${YOSYS} -p 'read_verilog recursive.v; hierarchy -top top; techmap -map recursive_map.v -max_iter 1; select -assert-count 2 t:sub; select -assert-count 2 t:bar'

View file

@ -1,4 +0,0 @@
#!/usr/bin/env bash
set -eu
source ../gen-tests-makefile.sh
generate_mk --yosys-scripts --tcl-scripts --bash --yosys-args "-e 'select out of bounds'"

View file

@ -57,4 +57,4 @@ endmodule
EOF
logger -expect error "Malformed design" 1
abc_new -script abc_speed_gia_only.script -liberty ../../tests/liberty/normal.lib -liberty ../../tests/liberty/dff.lib
abc_new -liberty ../../tests/liberty/normal.lib -liberty ../../tests/liberty/dff.lib