Unexpected result in insn_div when dividing by 0 when not using RISCV_FORMAL_ALTOPS

[Zeldax64]

When I run the insn_div test (without defining RISCV_FORMAL_ALTOPS) it always stops with an error after retiring any division by 0 instruction. After examining the counter trace I noticed that the signal rvfi_testbench.checker_inst.insn_spec.spec_rd_wdata is equal to 1 instead of -1.

I believe the problem is this line:

riscv-formal/insns/insn_div.v

Line 49 in 61d8b16

wire [`RISCV_FORMAL_XLEN-1:0] result = $signed(rvfi_rs1_rdata) / $signed(rvfi_rs2_rdata);

I have already read the description of RISCV_FORMAL_ALTOPS here but I think this define should also be listed in the Configuration Macros doc.

By the way, thanks for this great project. I have already caught some bugs in my implementation since I started using this framework.

[cliffordwolf]

After examining the counter trace I noticed that the signal rvfi_testbench.checker_inst.insn_spec.spec_rd_wdata is equal to 1 instead of -1.

That's interesting. What solver did you use? Because SMT-based solvers, like the ones used by default in SymbiYosys, should interpret x/0 as -1. But of course other engines might have different definitions. I've now added explicit handling of x/0 and INT_MIN/-1 to the instruction models.

[Zeldax64]

I'm using Boolector Version 3.0.1-pre master.