insn_div.v and insn_rem.v do not actually perform signed division in all cases

[kimmeljo]

Specifically referring to this line (in insn_div.v but same idea applies to insn_rem.v):

wire [`RISCV_FORMAL_XLEN-1:0] result = rvfi_rs2_rdata == `RISCV_FORMAL_XLEN'b0 ? {`RISCV_FORMAL_XLEN{1'b1}} :
                                         rvfi_rs1_rdata == {1'b1, {`RISCV_FORMAL_XLEN-1{1'b0}}} && rvfi_rs2_rdata == {`RISCV_FORMAL_XLEN{1'b1}} ? {1'b1, {`RISCV_FORMAL_XLEN-1{1'b0}}} :
                                         **$signed(rvfi_rs1_rdata) / $signed(rvfi_rs2_rdata)**;

If rvfi_rs1_rdata is a negative number and rvfi_rs2_rdata is a positive number with a larger absolute value, an assertion on rd_wdata fails if the HW correctly returns 0.

Fix (confirmed by shimming locally):

  wire [`RISCV_FORMAL_XLEN-1:0] result = rvfi_rs2_rdata == `RISCV_FORMAL_XLEN'b0 ? {`RISCV_FORMAL_XLEN{1'b1}} :
                                         rvfi_rs1_rdata == {1'b1, {`RISCV_FORMAL_XLEN-1{1'b0}}} && rvfi_rs2_rdata == {`RISCV_FORMAL_XLEN{1'b1}} ? {1'b1, {`RISCV_FORMAL_XLEN-1{1'b0}}} :
                                         **{$signed(rvfi_rs1_rdata) / $signed(rvfi_rs2_rdata)}**;

(surrounding the division expression in {...})

Note that local testing was only performed for RV32*

[jix]

I reproduced this by instantiating this check for the nerv core, which doesn't actually implement this instruction, and inspecting the resulting netlist which indeed has an unsigned $div cell. It's also expected by my reading of the SV standard since the ternary operator's operands are part of the same expression as the division and share the same signedness. Both read_verilog and verific agree here (although I wouldn't rule out that this was previously working due to some read_verilog bug wrt expression signedness).

This prompted me to look into re-running the cbmc based formal equivalence check to the spike instruction set simulator (in tests/spike), which should have caught this when the verilog instruction model was initially written, but I'm not sure for which instruction set variant this was performed. Either div wasn't part of what was tested or this worked due to a now fixedread_verilog bug. Unfortunately those test have seen some bitrot. The write_simplec backend produces code that didn't work with the cbmc version I tried, but that was easy enough work around and I could successfully rerun the tests for simple instructions like and and add. For div the write_simplec backend seems to be stuck in a loop. I haven't debugged this further yet.

[georgerennie]

I suspect part of why this was never caught is that only picorv32 of the cores in the repo is using a configuration that supports the m extension, and it defines RISCV_FORMAL_ALTOPS so isn't actually being tested on div/mul/rem value calculation

[KrystalDelusion]

@jix do you remember what changes were needed for the write_simplec backend to work with cbmc?

[jix]

@KrystalDelusion hat's what I had stashed locally https://github.com/jix/yosys/tree/simplec_workaround, but I didn't verify it's still working or that this is complete