Very close verilogs do not SAT solve equivalent

[renau]

Steps to reproduce the issue

I have two files option1.v and option2.v. I use the check2.ys for SAT solver checking. I think that the verilog should be the same (the parenthesis should not change semantics), but it does not SAT solve. Why???

:::::::::::::: option1.v :::::::::::::: module option1(a, y); input [1:0] a; output [1:0] y;

assign y = ~^a; endmodule :::::::::::::: option2.v :::::::::::::: module option1(a, y); input [1:0] a; output [1:0] y;

assign y = ~(^a); endmodule :::::::::::::: check2.ys ::::::::::::::

read_verilog -sv ./option1.v ; prep; memory -nomap; rename -top gold; design -stash gold; read_verilog -sv ./option2.v ; prep; memory -nomap; rename -top gate; design -stash gate; design -copy-from gold -as gold gold design -copy-from gate -as gate gate

miter -equiv -make_assert -flatten gold gate equiv hierarchy -top equiv sat -prove-asserts -show-inputs -max 2 -verify -set-init-undef -ignore_unknown_cells equiv

[udif]

Without digging further let me just hint at 2 points you want to consider:

1. Your 2 files are not the same because ~^ is the XNOR reduction operator, while ~(^) combines 2 separate operators, the reduction XOR operator ^, and the unary NOT operator, ~.
2. You assign a 1-bit expression to a 2-bit vector , and so y[1] is driven according to width extension rules.

In practice, I've ran your 2 modules with a commercial formal equivalence tool, and they don't match for y[1]. I didn't have much time to diagnose it further (some other guys needed the license :-( ), but a simple verilog test yields those results:

module option1(a, y);
input [1:0] a;
output [1:0] y;
assign y = ~^a;
endmodule

module option2(a, y);
input [1:0] a;
output [1:0] y;
assign y = ~(^a);
endmodule

module top;

reg [1:0]in;
wire [1:0]o1;
wire [1:0]o2;

initial
begin
  $display("in o1 o2");
  #1 in = 2'b00; #1 $display("%02b %02b %02b", in, o1, o2);
  #1 in = 2'b01; #1 $display("%02b %02b %02b", in, o1, o2);
  #1 in = 2'b10; #1 $display("%02b %02b %02b", in, o1, o2);
  #1 in = 2'b11; #1 $display("%02b %02b %02b", in, o1, o2);
end
option1 op1 (.a(in), .y(o1));
option2 op2 (.a(in), .y(o2));

endmodule

in o1 o2
00 01 11
01 00 10
10 00 10
11 01 11

I went through section 11.6 to 11.8 of the IEEE1800-2017 standard, but can't really find the smoking gun for explaining this. It does say reduction operators produce unsigned result, so for ~^ y[1] is probably always 0. I can't however explain the behavior for ~(^). Even if it was due to sign extension, I would expect y[1] to be 0 when y[0] is 0.

[renau]

Ok, it makes sense. I forgot about the xnor operator. I thought that it was a not xor.

On Tue, Mar 5, 2019, 1:14 AM udif notifications@github.com wrote:

Without digging further let me just hint at 2 points you want to consider:

1. Your 2 files are not the same because ~^ is the XNOR reduction operator, while ~(^) combines 2 separate operators, the reduction XOR operator ^, and the unary NOT operator, ~.
2. You assign a 1-bit expression to a 2-bit vector , and so y[1] is driven according to width extension rules.

In practice, I've ran your 2 modules with a commercial formal equivalence tool, and they don't match for y[1]. I didn't have much time to diagnose it further (some other guys needed the license :-( ), but a simple verilog test yields those results:

module option1(a, y); input [1:0] a; output [1:0] y; assign y = ~^a; endmodule

module option2(a, y); input [1:0] a; output [1:0] y; assign y = ~(^a); endmodule

module top;

reg [1:0]in; wire [1:0]o1; wire [1:0]o2;

initial begin $display("in o1 o2");

1 in = 2'b00; #1 $display("%02b %02b %02b", in, o1, o2);

1 in = 2'b01; #1 $display("%02b %02b %02b", in, o1, o2);

1 in = 2'b10; #1 $display("%02b %02b %02b", in, o1, o2);

1 in = 2'b11; #1 $display("%02b %02b %02b", in, o1, o2);

end option1 op1 (.a(in), .y(o1)); option2 op2 (.a(in), .y(o2));

endmodule

in o1 o2 00 01 11 01 00 10 10 00 10 11 01 11

I went through section 11.6 to 11.8 of the IEEE1800-2017 standard, but can't really find the smoking gun for explaining this. It does say reduction operators produce unsigned result, so for ~^ y[1] is probably always 0. I can't however explain the behavior for ~(^). Even if it was due to sign extension, I would expect y[1] to be 0 when y[0] is 0.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/YosysHQ/yosys/issues/854#issuecomment-469601469, or mute the thread https://github.com/notifications/unsubscribe-auth/AFqFNuoYLm90Zlq3zTyEYj8qLV6f9_nvks5vTjVrgaJpZM4bd_8X .

[daveshah1]

My understanding is the difference for ~(^) is that this is autosized to the result type, so the XOR result is resized to 00 or 01, which is then inverted to 11 or 10