multiple drivers on a variable in a module change values of input ports when using `prep`

[toby-bro]

Version

Yosys 0.54 (git sha1 db72ec3, g++ 12.2.0-14+deb12u1 -fPIC -O3)

On which OS did this happen?

Linux

Reproduction Steps

read_verilog -sv <<EOT
module simple_sub (
    input logic [7:0] a,
    input logic [7:0] b,
    output logic [7:0] a_out,
    output logic [7:0] b_out,
    output logic [7:0] diff
);
    wire [7:0] conflict_wire;
    assign a_out = a;
    assign b_out = b;
    assign conflict_wire = b;
    assign conflict_wire = a;
    assign diff = a - b;
    always_comb assert(b != a);
endmodule

module top;
    logic [7:0] a, b, a_out, b_out, diff;
    
    assign a = 8'hAA;
    assign b = 8'h55;

    simple_sub dut (
        .a(a),
        .b(b),
        .a_out(a_out),
        .b_out(b_out),
        .diff(diff)
    );

endmodule
EOT

prep -top top
chformal -lower
select simple_sub
sat -prove-asserts -verify

Tried to write a yosys script to simplify reproduction of bug, (hopefully it is correct 😅)

Expected Behavior

I don't really know (I thought I would mention it as this behaviour surprised me), I would have thought that for conflict_wire the value could be either that of a or that of b but I would have thought that the inputs are not modified in the module.

Actual Behavior

module simple_sub(a, b, a_out, b_out, diff);
  input [7:0] a;
  wire [7:0] a;
  output [7:0] a_out;
  wire [7:0] a_out;
  input [7:0] b;
  wire [7:0] b;
  output [7:0] b_out;
  wire [7:0] b_out;
  wire [7:0] conflict_wire;
  output [7:0] diff;
  wire [7:0] diff;
  assign diff = a - a;
  assign a_out = a;
  assign b = a;
  assign b_out = a;
  assign conflict_wire = a;
endmodule

b is assigned the value of a

[KrystalDelusion]

This specific case is also related to #5058 because of the multiple drivers being accepted as valid (and then opt_clean comes along and merges the two nets together).

[KrystalDelusion]

Also I don't think the script is quite right, since it still fails even if you remove conflict_wire (probably because without the top module it can freely assign a and b to just being the same).

read -noverific
read -sv <<EOT
module simple_sub (
    input logic [7:0] a,
    input logic [7:0] b,
    output logic [7:0] a_out,
    output logic [7:0] b_out,
    output logic [7:0] diff
);
    wire [7:0] conflict_wire;
    assign a_out = a;
    assign b_out = b;
    assign conflict_wire = b;
    assign conflict_wire = a;
    assign diff = a - b;
endmodule

module top;
    logic [7:0] a, b, a_out, b_out, diff;
    
    assign a = 8'hAA;
    assign b = 8'h55;

    simple_sub dut (
        .a(a),
        .b(b),
        .a_out(a_out),
        .b_out(b_out),
        .diff(diff)
    );

endmodule
EOT

prep -top top
cd simple_sub
select -assert-count 1 i:b %ci

is a working alternative, skipping the assert entirely.

[toby-bro]

Sorry I hadn't realised it was the same issue.
🤦 you're right the prover can't assert that they are always different as it only analyses the module without anything else.
Thanks for the corrected yosys script.
Thanks for the work on yosys.