yosys/tests/various/setundef_selection.ys

# Test that setundef -zero respects wire selection: only selected wire is changed
read_verilog <<EOT
module test;
    wire a = 1'bx;
    wire b = 1'bx;
endmodule
EOT
setundef -zero w:a
sat -prove a 0
design -reset

# Test that setundef -undriven -zero respects wire selection
read_verilog <<EOT
module test(output wire a, output wire b);
    assign a = 1'b0;
endmodule
EOT
setundef -undriven -zero w:b
sat -prove b 0
design -reset

# Test that setundef -init respects cell selection: only selected FF gets init set
read_rtlil setundef_selection_ff.il
setundef -init -zero c:myff_a
# only wire a should have init attribute, not b
select -assert-count 1 w:* a:init %i
design -reset