formal mismatch (div) #2508
Comments
|
Division by constant zero results in Passing |
|
@Ravenslofty when I add |
|
Without seeing your code there's no way for me to tell why that might be. |
|
Here is the case which was EQ without Amodule top_mod(
input [14:0] inp_2,
input [19:0] inp_6,
output tmp19,
output [14:0] tmp9
);
wire [19:0] _GEN_0 = {{5'd0}, inp_2};
assign tmp19 = 1'h0;
assign tmp9 = _GEN_0 / inp_6;
endmoduleBmodule top_mod(
input [14:0] inp_2,
input [19:0] inp_6,
output tmp19,
output [14:0] tmp9);
wire [14:0] _T; // a_top_mod.fir:3:3
wire [19:0] _T_0 = {{5'd0}, inp_2} / inp_6; // a_top_mod.fir:8:13
assign _T = _T_0[14:0]; // a_top_mod.fir:8:{10,13}
assign tmp19 = 17'h1FFFF < {{2'd0}, _T}; // a_top_mod.fir:3:3, :9:{14,24}
assign tmp9 = _T; // a_top_mod.fir:3:3, :9:{14,24}
endmodule |
|
How about? |
|
I think the answer is actually to use |
|
@Ravenslofty thank you, I will try. |
or ? The second one gives me: |
|
Actually, no. I got Helpfully though, Consider On A, the result of On B, the So the reason these are failing as not equivalent is because they are indeed not equivalent in the presence of undefined states. |
No |
|
You can go even further with |
Fails 20% of passing cases with error: Like this one: Amodule top_mod(
input [19:0] inp_0,
output tmp6
);
assign tmp6 = 1'h0;
endmoduleBmodule top_mod(
input [19:0] inp_0,
output tmp6);
assign tmp6 = {{3'd0}, inp_0} >= 23'h5054FE; // a_top_mod.fir:3:3, :6:{13,24}
endmodule |
|
Once again, when you include undefined states in |
|
@Ravenslofty could you explain how |
|
Because the result of an operation on something with |
|
In Verilog? |
I read this to mean even a single |
|
You are right about being X-pessimistic :( |
|
I was surprised by this, becoming sad and happy at the same time. I was always under the impression that a testcase like this: module test; Would produce: But instead is produces: I'm sad because this level of pessimism is not needed, but I'm happy because it makes 4-state simulation so much easier. |
Steps to reproduce the issue
The following 2 programs (A/B) reported as mismatched.
A
B
Expected behavior
Expected to be equivalent.
Actual behavior
Yosys (Yosys 0.9+3755 (git sha1 442d19f, clang 11.0.0 -fPIC -Os)) reports mismatch between current and expected result:
Can be reproduced with the following command:
The text was updated successfully, but these errors were encountered: