clockgate: formal liberty tests

This commit is contained in:
Emil J. Tywoniak
2026-05-07 16:08:55 +02:00
parent f4a10a4808
commit 687e5442f2
5 changed files with 107 additions and 100 deletions
+6
View File
@@ -6,6 +6,7 @@ library(test) {
pin (GCLK) { pin (GCLK) {
clock_gate_out_pin : true; clock_gate_out_pin : true;
direction : output; direction : output;
function : "CLK&CE";
} }
pin (CLK) { pin (CLK) {
clock_gate_clock_pin : true; clock_gate_clock_pin : true;
@@ -26,6 +27,7 @@ library(test) {
pin (GCLK) { pin (GCLK) {
clock_gate_out_pin : true; clock_gate_out_pin : true;
direction : output; direction : output;
function : "CLK&CE";
} }
pin (CLK) { pin (CLK) {
clock_gate_clock_pin : true; clock_gate_clock_pin : true;
@@ -42,6 +44,7 @@ library(test) {
pin (GCLK) { pin (GCLK) {
clock_gate_out_pin : true; clock_gate_out_pin : true;
direction : output; direction : output;
function : "CLK&CE";
} }
pin (CLK) { pin (CLK) {
clock_gate_clock_pin : true; clock_gate_clock_pin : true;
@@ -58,6 +61,7 @@ library(test) {
pin (GCLK) { pin (GCLK) {
clock_gate_out_pin : true; clock_gate_out_pin : true;
direction : output; direction : output;
function : "CLK|!CE";
} }
pin (CLK) { pin (CLK) {
clock_gate_clock_pin : true; clock_gate_clock_pin : true;
@@ -74,6 +78,7 @@ library(test) {
pin (GCLK) { pin (GCLK) {
clock_gate_out_pin : true; clock_gate_out_pin : true;
direction : output; direction : output;
function : "CLK|!CE";
} }
pin (CLK) { pin (CLK) {
clock_gate_clock_pin : true; clock_gate_clock_pin : true;
@@ -94,6 +99,7 @@ library(test) {
pin (GCLK) { pin (GCLK) {
clock_gate_out_pin : true; clock_gate_out_pin : true;
direction : output; direction : output;
function : "CLK|!CE";
} }
pin (CLK) { pin (CLK) {
clock_gate_clock_pin : true; clock_gate_clock_pin : true;
@@ -1,53 +1,6 @@
read_verilog << EOT yosys -import
read_verilog clockgate.v
module dffe_00( input clk, en, yosys proc
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
opt opt
design -save before design -save before
@@ -128,41 +81,7 @@ select -module dffe_11 -assert-count 0 t:\\pdk_icg
#------------------------------------------------------------------------------ #------------------------------------------------------------------------------
design -reset design -reset
read_rtlil << EOT read_rtlil clockgate_bad.il
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
# Check we don't choke on constants # Check we don't choke on constants
clockgate -pos pdk_icg ce:clkin:clkout -tie_lo scanen clockgate -pos pdk_icg ce:clkin:clkout -tie_lo scanen
@@ -173,19 +92,8 @@ select -module bad2 -assert-count 0 t:\\pdk_icg
# Regression test: EN is a bit from a multi-bit wire # Regression test: EN is a bit from a multi-bit wire
design -reset design -reset
read_verilog << EOT read_verilog clockgate_wide.v
module dffe_wide_11( input clk, input [1:0] en, yosys proc
input [3:0] d1, output reg [3:0] q1,
);
always @( posedge clk ) begin
if ( en[0] )
q1 <= d1;
end
endmodule
EOT
proc
opt opt
clockgate -pos pdk_icg ce:clkin:clkout -tie_lo scanen clockgate -pos pdk_icg ce:clkin:clkout -tie_lo scanen
@@ -193,8 +101,18 @@ select -assert-count 1 t:\\pdk_icg
#------------------------------------------------------------------------------ #------------------------------------------------------------------------------
design -load before design -reset
clockgate -liberty c*ckgate.lib 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 # rising edge ICGs
select -module dffe_00 -assert-count 0 t:\\pos_small select -module dffe_00 -assert-count 0 t:\\pos_small
+44
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
+31
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
+8
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