Yosys optimization alters circuit functionality

[flaviens]

Version

Yosys 0.37+21 (git sha1 3d9e44d18, clang 10.0.0-4ubuntu1 -fPIC -Os)

On which OS did this happen?

Linux

Reproduction Steps

Hi there!

I stumbled into a circuit that, when optimized by Yosys, changes functionality. This simple circuit seems to be legitimate synthesizable Verilog code and does not imply x/z signals on any path that leads to the mismatch. I also see no Yosys warning of any kind. Here is a repository for you to reproduce the issue easily.

Please let me know if you require any more information or help, or please let me know if I did something wrong here.

Thank you! Flavien

Expected Behavior

The behavior before and after optimization should be the same.

Actual Behavior

The behavior before and after optimization differ.

[povik]

I have been able to minimize it to this, which is probably the issue: EDIT: not the issue, just opt_muxtree changing the semantics of public wires in-place

read_verilog -sv <<EOF
module top(a, b, y);
  input wire a, b;
  output wire y;
  wire z;
  assign z = a ? b : a;
  assign y = b ? z : 0;
endmodule
EOF
opt_clean
equiv_opt -undef opt_muxtree

[povik]

Concise reproduction steps:

read_verilog -sv <<EOF
module top(in_data, out_data);
  bit [1:0] _00_;
  bit [1:0] _01_;
  bit _02_;
  bit _03_;
  bit _04_;
  bit _05_;
  bit [1:0] _06_;
  bit [1:0] _07_;
  bit _08_;
  bit _09_;
  bit _10_;
  bit celloutsig_0z;
  bit [1:0] celloutsig_1z;
  bit [1:0] celloutsig_2z;
  bit celloutsig_3z;
  input [95:0] in_data;
  bit [95:0] in_data;
  output out_data;
  bit out_data;
  assign celloutsig_1z = _01_ * _00_;
  assign celloutsig_2z = _05_ ? _06_ : _07_;
  assign celloutsig_3z = _02_ ? _03_ : _04_;
  assign celloutsig_0z = _09_ | _08_;
  assign _09_ = in_data[21];
  assign _08_ = in_data[51];
  assign _01_[0] = celloutsig_0z;
  assign _01_[1] = celloutsig_0z;
  assign _00_[0] = celloutsig_0z;
  assign _00_[1] = celloutsig_0z;
  assign _07_[0] = celloutsig_0z;
  assign _07_[1] = celloutsig_1z[0];
  assign _06_ = in_data[43:42];
  assign _05_ = celloutsig_1z[0];
  assign _04_ = celloutsig_2z[1];
  assign _03_ = celloutsig_2z[0];
  assign _02_ = in_data[43];
  assign _10_ = in_data[92];
  assign out_data = celloutsig_3z;
endmodule
EOF
eval -set in_data 96'hf0000000fffff40000000000 w:out_data 
opt
eval -set in_data 96'hf0000000fffff40000000000 w:out_data 

[povik]

Minimized:

read_verilog -sv <<EOF
module top(in_data, out_data);
  input wire [95:0] in_data;
  output wire out_data;
  wire [1:0] f = in_data[51] ? {in_data[0], in_data[0]} : {in_data[1], in_data[1]};
  assign out_data = in_data[0] ? f[0] : f[1];
endmodule
EOF
eval -set in_data 96'hf0000000fffff40000000000 w:out_data 
opt_muxtree
eval -set in_data 96'hf0000000fffff40000000000 w:out_data 

Issue appears to be opt_muxtree being confused by the same mux appearing twice in the tree.