write_btor: Part selects of undriven signals are lowered as separate inputs

[georgerennie]

Version

Yosys 0.45+153 (git sha1 ab378f8, g++ 14.2.1 -fPIC -O3)

On which OS did this happen?

Linux

Reproduction Steps

read_verilog -formal <<EOT
module top;
(* anyseq *) wire [1:0] a;
wire [1:0] mask = 2'b01;
always @* assert({1'b0, a[0]} == (a & mask));
endmodule
EOT

proc -noopt
chformal -lower
write_btor design.btor2

sat -prove-asserts -verify                          # Returns UNSAT
exec -not-expect-stdout ^sat -- btormc design.btor2 # Returns UNSAT

design -reset

read_verilog -formal <<EOT
module top;
wire [1:0] a;
wire [1:0] mask = 2'b01;
always @* assert({1'b0, a[0]} == (a & mask));
endmodule
EOT

proc -noopt
chformal -lower
write_btor design.btor2

sat -prove-asserts -verify                          # Returns UNSAT
exec -not-expect-stdout ^sat -- btormc design.btor2 # Returns SAT - bad

Expected Behavior

I expect an undriven wire to have the same semantics as one driven by anyseq, to be left free to take any value at any time, but that all references to that wire should see the same value.

Actual Behavior

With the BTOR backend, part selects of an undriven wire get lowered as inputs multiple times, meaning that different uses of the wire can see different values. Looking at the generated btor

; BTOR description generated by Yosys 0.45+153 (git sha1 ab378f840, g++ 14.2.1 -fPIC -O3) for module top.
1 sort bitvec 1
2 input 1
3 const 1 0
4 sort bitvec 2
5 concat 4 3 2
6 input 4
7 const 4 01
8 and 4 6 7
9 eq 1 5 8
10 const 1 1
11 not 1 9
12 and 1 10 11
13 bad 12 <<EOT:4.11-4.45
14 uext 4 7 0 mask ; <<EOT:3.12-3.16
15 uext 4 6 0 a ; <<EOT:2.12-2.13
; end of yosys output

we see that node 2 defines a 1 bit input (a[0]), and node 6 separately defines a 2 bit input (a), so these are not consistent.

Instead, when emitting for an undriven wire it should be emitted as an input once and then part selects referenced from that input with slice. Partially driven wires can be modelled with bit masks to select between the driver and an input variable.