Logical Equivalence Check

[EmJunaid]

I'm comparing two netlists through equiv_make given as below: First netlist:

module inverter(in, out);
input in;
wire in;
output out;
wire out;
sky130_fd_sc_hd__inv_2 0 (
.A(in),
.Y(out)
);
endmodule

second_netlist

module inverter (in,
out);
input in;
output out;

wire net1;
wire net2;

sky130_fd_sc_hd__decap_3 PHY_0 ();
sky130_fd_sc_hd__decap_3 PHY_1 ();
sky130_fd_sc_hd__decap_3 PHY_10 ();
sky130_fd_sc_hd__decap_3 PHY_11 ();
sky130_fd_sc_hd__decap_3 PHY_12 ();
sky130_fd_sc_hd__decap_3 PHY_13 ();
sky130_fd_sc_hd__decap_3 PHY_14 ();
sky130_fd_sc_hd__decap_3 PHY_15 ();
sky130_fd_sc_hd__decap_3 PHY_16 ();
sky130_fd_sc_hd__decap_3 PHY_17 ();
sky130_fd_sc_hd__decap_3 PHY_18 ();
sky130_fd_sc_hd__decap_3 PHY_19 ();
sky130_fd_sc_hd__decap_3 PHY_2 ();
sky130_fd_sc_hd__decap_3 PHY_20 ();
sky130_fd_sc_hd__decap_3 PHY_21 ();
sky130_fd_sc_hd__decap_3 PHY_22 ();
sky130_fd_sc_hd__decap_3 PHY_23 ();
sky130_fd_sc_hd__decap_3 PHY_24 ();
sky130_fd_sc_hd__decap_3 PHY_25 ();
sky130_fd_sc_hd__decap_3 PHY_3 ();
sky130_fd_sc_hd__decap_3 PHY_4 ();
sky130_fd_sc_hd__decap_3 PHY_5 ();
sky130_fd_sc_hd__decap_3 PHY_6 ();
sky130_fd_sc_hd__decap_3 PHY_7 ();
sky130_fd_sc_hd__decap_3 PHY_8 ();
sky130_fd_sc_hd__decap_3 PHY_9 ();
sky130_fd_sc_hd__tapvpwrvgnd_1 TAP_26 ();
sky130_fd_sc_hd__tapvpwrvgnd_1 TAP_27 ();
sky130_fd_sc_hd__tapvpwrvgnd_1 TAP_28 ();
sky130_fd_sc_hd__tapvpwrvgnd_1 TAP_29 ();
sky130_fd_sc_hd__tapvpwrvgnd_1 TAP_30 ();
sky130_fd_sc_hd__tapvpwrvgnd_1 TAP_31 ();
sky130_fd_sc_hd__tapvpwrvgnd_1 TAP_32 ();
sky130_fd_sc_hd__inv_2 0 (.A(net1),
.Y(net2));
sky130_fd_sc_hd__buf_1 input1 (.A(in),
.X(net1));
sky130_fd_sc_hd__buf_4 output2 (.A(net2),
.X(out));
endmodule

Script for equivalence checking is given as:

read_liberty -nooverwrite -lib -ignore_miss_dir -setattr blackbox cell.lib
read_verilog inverter.resized.v.without_power_pins.v
hierarchy -auto-top
hierarchy -generate sky130_fd_sc_hd__buf*
hierarchy -generate sky130_fd_sc_hd__decap*
hierarchy -generate sky130_fd_sc_hd__tapvpwrvgnd*
prep -flatten
splitnets -ports;;
rename -top gold
design -stash gold

read_liberty -nooverwrite -lib -ignore_miss_dir -setattr blackbox cell.lib
read_verilog inverter.v
hierarchy -auto-top
prep -flatten
splitnets -ports;;
rename -top gate
design -stash gate

read_liberty -nooverwrite -lib -ignore_miss_dir -setattr blackbox cell.lib
design -copy-from gold -as gold gold
design -copy-from gate -as gate gate
equiv_make gold gate equiv
prep -flatten -top equiv

opt_clean -purge
show -prefix equiv-prep -colors 1 -stretch

opt -full
equiv_simple -seq 5
equiv_induct -seq 5
equiv_status -assert

Dot file is given as below:

And getting this ERROR:

ERROR: Found 2 unproven $equiv cells in 'equiv_status -assert'

Can anyone guide me why I'm getting this error?

[nakengelhardt]

Do you have a logic model of the sky130 cells? From a quick glance at the script it looks like everything is loaded as blackboxes, so for the buffers on each side of the inverter yosys wouldn't be able to know that the output is equivalent to the input...

[EmJunaid]

@nakengelhardt Do you mean other than the liberty file or do you mean what's inside the liberty file?

[zappos23]

hi, i am facing similar situation too. i thought there are cell’s function definition in the liberty file? Wouldn’t that be sufficient?

[zappos23]

Even with loading the sky130 stdcell primitive and still seeing the design not equivalent

[EmJunaid]

@zappos23 do you know how to put a check on output of equiv.dot module? or even can we do this or not?

[zappos23]

@EmJunaid, i’ve no idea. Not sure if we can create mapping for the cells. I noticed, the only way to get both netlists to be equivalent is they need to have the same logic structure. The extra buffers like your gate netlist can already cause them to be not equivalent.

[nakengelhardt]

@nakengelhardt Do you mean other than the liberty file or do you mean what's inside the liberty file?

I mean contents of the cells in the liberty file - you are loading blackboxes only (all the calls to read_liberty use -lib) so Yosys has no idea what these cells do. In that case the only kind of equivalence check you could do is structural (equiv_struct) but this only works if both circuits have identical structure, which is almost never the case for pre- vs post-synthesis (as you can see here where it fails due to presence of buffers even for a circuit that is only a single instantiated inverter).

[EmJunaid]

@nakengelhardt yes you are right. Yosys was not able to understand the logic of cells that's why it was falling the check. I need to somehow provide the information about logical behaviour of these cells.

[zappos23]

@EmJunaid would you mind to share the commands? Thanks

[EmJunaid]

@zappos23 You need to read the liberty file not as a blackbox so you need to remove -lib from read_liberty command and also you need to read liberty file having power and ground connections as well. read_liberty -ignore_miss_dir cell.lib