LEC failed after yosys synthesis

[Telpukhov]

Version

up to 0.32

On which OS did this happen?

Linux

Reproduction Steps

Yosys makes wrong full adder extraction in the case of adding multiple bits. Minimal example of such behaviour is the sum of 4 bits. Initial RTL:

module gcd(I, D);

  output [2:0] I;
  input [3:0] D;

  assign I = D[0]+D[1]+D[2]+D[3];
endmodule

Simple script for Yosys, with extract_fa command:

read_verilog gcd.v
synth  -top gcd -flatten
extract_fa

opt -purge
show -stretch -prefix gcd -format dot
write_verilog res.v

I've analysed output file and graphical representation. It have obvious inequivalence to the initial RTL. But to be consistent, I've made a script for equivalence check:

read_verilog gcd.v

hierarchy -top gcd
proc
opt 
opt
async2sync
opt
splitnets -ports
opt
flatten
opt
select gcd
rename -hide
    
                   
design -stash gold


read_verilog res.v

hierarchy -top gcd
proc
opt
opt
async2sync
opt
splitnets -ports
opt
flatten
opt
select gcd
rename -hide

design -stash gate


design -copy-from gold -as gold gcd
design -copy-from gate -as gate gcd

miter -equiv -flatten -ignore_gold_x gold gate miter
hierarchy -top miter
opt
select miter
hierarchy -top miter
rename -hide

sat -verify -tempinduct -prove trigger 0 -set-init-undef -set-def-inputs -seq 5

Interesting part is that on LINUX builds I get this problem and wrong netlist. But then I tried to run this testcase on Windows pre-built binaries, and everything was fine - output netlist was correct, and equivalence was prooved. So in next sections I will submit Windows results like "Expected Behaviour", and Linux results like "Actual Behaviour".

Analysing wrong results you can verify that I[0] should be XOR of D[0], D[1], D[2], D[3]. But in resulted netlist we get I[0] as XOR of ~D[0], ~D[1], D[2], ~D[3]. It gets mismatch already on test vector (0, 0, 0, 0). Equivalence script expectedly indicates a mismatch.

In correct (windows) netlist we still have some unnecessary inversions, but logic functions are equivalent to RTL. For example I[0] = ~((~D[0])^(~D[1])^(~D[3]))^D[2] and it is equivalent to XOR of D[0], D[1], D[2], D[3]. Equivalence script indicates Induction step proven: SUCCESS!

Expected Behavior

module gcd(I, D);
  wire _00_;
  wire _01_;
  wire _02_;
  wire _03_;
  wire _04_;
  wire _05_;
  wire _06_;
  wire _07_;
  (* src = "gcd.v:4.15-4.16" *)
  input [3:0] D;
  wire [3:0] D;
  (* src = "gcd.v:3.16-3.17" *)
  output [2:0] I;
  wire [2:0] I;
  assign _02_ = ~D[3];
  \$fa  #(
    .WIDTH(32'd1)
  ) _09_ (
    .A(_04_),
    .B(_05_),
    .C(_02_),
    .X(_00_),
    .Y(_01_)
  );
  assign _04_ = ~D[0];
  assign _05_ = ~D[1];
  \$fa  #(
    .WIDTH(32'd1)
  ) _12_ (
    .A(_06_),
    .B(_03_),
    .C(1'h0),
    .X(I[2]),
    .Y(I[1])
  );
  \$fa  #(
    .WIDTH(32'd1)
  ) _13_ (
    .A(D[2]),
    .B(_07_),
    .C(1'h0),
    .X(_03_),
    .Y(I[0])
  );
  assign _06_ = ~_00_;
  assign _07_ = ~_01_;
endmodule

Actual Behavior

module gcd(I, D);
  wire _00_;
  wire _01_;
  wire _02_;
  wire _03_;
  wire _04_;
  wire _05_;
  wire _06_;
  (* src = "gcd.v:4.15-4.16" *)
  input [3:0] D;
  wire [3:0] D;
  (* src = "gcd.v:3.16-3.17" *)
  output [2:0] I;
  wire [2:0] I;
  \$fa  #(
    .WIDTH(32'd1)
  ) _07_ (
    .A(_04_),
    .B(_05_),
    .C(_06_),
    .X(_01_),
    .Y(_02_)
  );
  assign _04_ = ~D[0];
  assign _05_ = ~D[1];
  assign _06_ = ~D[3];
  assign _00_ = ~_01_;
  \$fa  #(
    .WIDTH(32'd1)
  ) _12_ (
    .A(_00_),
    .B(_03_),
    .C(1'h0),
    .X(I[2]),
    .Y(I[1])
  );
  \$fa  #(
    .WIDTH(32'd1)
  ) _13_ (
    .A(D[2]),
    .B(_02_),
    .C(1'h0),
    .X(_03_),
    .Y(I[0])
  );
endmodule

[jix]

I could reproduce this and found what I think is a missing inversion in extract_fa (see #3882) that seems to be the reason, but I'm not super confident that adding it there doesn't break another case. I suspect the windows version wasn't affected because the synth output was slightly different, thus using slightly different code paths in extract_fa.

[Telpukhov]

I could reproduce this and found what I think is a missing inversion in extract_fa (see #3882) that seems to be the reason, but I'm not super confident that adding it there doesn't break another case. I suspect the windows version wasn't affected because the synth output was slightly different, thus using slightly different code paths in extract_fa.

Thank you for the answer!
I’ve tried building Yosys with your changes. It indeed works correctly with initial testcase I’ve provided. However, there’s another simple case it still fails. I used the same script to synthesize and extract FA from a sum of two N-bit integers and it seems to generate non-equivalent Verilog netlist for N>=3.
Example Verilog:

module gcd(I, A, B);
  input [2:0] A, B;
  output [3:0] I;
  assign I = A+B;
endmodule

Graph representation of the synthesized netlist:

LEC result: