Repro tie box, portarcs, read_liberty.

This commit is contained in:
nella
2026-09-21 16:33:47 +02:00
parent fb74fe275d
commit b60492b203
3 changed files with 77 additions and 0 deletions
@@ -0,0 +1,12 @@
# https://github.com/librelane/librelane/blob/f24e0ea5db2260719e9a0c7d51d07db74a87fa23/librelane/scripts/pyosys/synthesize.py
# plain read_liberty -lib (librelane order) makes cells abc9_box without timing; abc_new refuses, abc accepts
read_liberty -lib ../openroad/cm_test_cells.lib
read_liberty -lib ../openroad/sm_test_cells.lib
read_verilog spm.v
hierarchy -top spm -chparam bits 8
synth -run :fine
techmap
dfflibmap -liberty ../openroad/sm_test_cells.lib
abc_new -liberty ../openroad/cm_test_cells.lib -liberty ../openroad/sm_test_cells.lib
select -assert-none t:$_*_
+30
View File
@@ -0,0 +1,30 @@
# https://github.com/The-OpenROAD-Project/OpenROAD/blob/80443953721b0134bed51bbab17a633a575098a6/src/cut/test/sky130_const_cell.v
# input-less box (tie cell): abc asserts in Gia_ManLevelWithBoxes, same with abc9 -lut
read_verilog <<EOT
module top(clk, c);
input clk;
output c;
wire flop_net;
TIEHI _403_ (
.Y(flop_net)
);
DFF output_flop (
.D(flop_net),
.Q(c),
.CLK(clk)
);
endmodule
EOT
read_liberty -lib -unit_delay cm_test_cells.lib
read_liberty -lib -unit_delay sm_test_cells.lib
hierarchy -top top
abc_new -liberty cm_test_cells.lib -liberty sm_test_cells.lib
select -assert-count 1 t:TIEHI
select -assert-count 1 t:DFF
check -assert
+35
View File
@@ -0,0 +1,35 @@
# mapped cells without timing: portarcs -draw divides by zero (portarcs.cc:285), SIGFPE
read_verilog -specify <<EOT
(* abc9_box, lib_whitebox *)
module MX4(input D0, D1, D2, D3, S0, S1, output Y);
specify
(D0 => Y) = 100; (D1 => Y) = 100; (D2 => Y) = 100; (D3 => Y) = 100;
(S0 => Y) = 50; (S1 => Y) = 50;
endspecify
assign Y = S1 ? (S0 ? D3 : D2) : (S0 ? D1 : D0);
endmodule
module top(input [3:0] d, input [1:0] s, input a, output y, z);
wire m;
MX4 mux (.D0(d[0]), .D1(d[1]), .D2(d[2]), .D3(d[3]), .S0(s[0]), .S1(s[1]), .Y(m));
assign y = m ^ a;
assign z = m & d[0];
endmodule
EOT
hierarchy -top top
proc
opt
design -save gold
techmap
abc_new -liberty openroad/cm_test_cells.lib
select -assert-count 1 top/t:MX4
select -assert-none top/t:$_*_
check -assert
read_verilog openroad/cells_sim.v
flatten
opt_clean
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
miter -equiv -flatten -make_assert -ignore_gold_x gold gate miter
sat -verify -prove-asserts -show-ports miter