yosys: formal mismatch (div)
Steps to reproduce the issue
The following 2 programs (A/B) reported as mismatched.
A
module top_mod(
input [3:0] inp_e,
output [24:0] tmp25
);
wire [24:0] tmp17;
assign tmp17 = 25'h0;
assign tmp25 = 25'h5 / tmp17;
endmodule
B
module top_mod(
input [3:0] inp_e,
output [24:0] tmp25
);
assign tmp25 = 25'h5 / 25'h0;
endmodule
Expected behavior
Expected to be equivalent.
Actual behavior
Yosys (Yosys 0.9+3755 (git sha1 442d19f6, clang 11.0.0 -fPIC -Os)) reports mismatch between current and expected result:
ERROR: Found 25 unproven $equiv cells in 'equiv_status -assert'.
Can be reproduced with the following command:
#!/bin/bash
VFILE1=a_top_mod_old.v
VFILE2=a_top_mod_new.v
DUT=top_mod
../../YosysHQ/yosys/yosys -q -p "
read_verilog $VFILE1
rename $DUT top1
proc
memory
flatten top1
hierarchy -top top1
read_verilog $VFILE2
rename $DUT top2
proc
memory
flatten top2
equiv_make top1 top2 equiv
hierarchy -top equiv
clean -purge
equiv_simple -short
equiv_induct
equiv_status -assert
"
About this issue
- Original URL
- State: closed
- Created 4 years ago
- Comments: 19 (1 by maintainers)
I read this to mean even a single
xbit is enough to make the result of your comparisonx.I think the answer is actually to use
satnotequiv_inducthere.Division by constant zero results in
tmp25being25'bx. By default, neitherequiv_simplenorequiv_inductmodel undefined states, so these are not considered equivalent.Passing
-undeftoequiv_{simple,induct}solves the issue: