darbaria / axiomise-warpv-formal-6-stage

1 stars 0 forks source link

JAL for misaligned addresses doesn't raise trap #12

Open darbaria opened 3 years ago

darbaria commented 3 years ago

Page 21 of the RISCV-ISA 2019 version states that "The JAL and JALR instructions will generate an instruction-address-misaligned exception if the target address is not aligned to a four-byte boundary."

This is not implemented correctly in the design. The design generates a trap when it finds the instruction[21] bit is high. This is incorrect. The trap should be raised if the lower two bits are non-zero for the target address that is obtained by summing up the PC and the sign-extended offset (which anyways is also broken in the design, see Git issue #9 ).


//-- This is what the design is doing
as_ISA_JAL_design_raises_TRAP_but_incorrectly:
`ap (`CORE.FETCH_Instr_jump_a3 && `CORE.FETCH_Instr_raw_j_imm_a3[1] |-> ##2 `CORE.FETCH_Instr_non_aborting_isa_trap_a5);

JAL_TRAP.vcd.gz

darbaria commented 3 years ago

Bug classification is done.