Cannot generate trap on bad jump address (c.j/c.jal)

[aignacio]

Hi Clifford, I was testing my core in the last few days and I've notice some problems when testing the compressed ISA, my IP is able to pass in all checks but not in the c.j and c.jal instructions, then when I saw the error log, it was displayed that fails in the assertion of trap. Looking deeper in the VCD I understood the problem, that's related to the LSB being set in the jump address, so then my IP raised a synchronous trap what it was not expected by the rvfi_insn_check.v. Commenting the code segment like the image below of a trap generation shows that the IP pass in all the tests. Could you clarify me that verify LSB it's wrong on these instructions?

[cliffordwolf]

Could you clarify me that verify LSB it's wrong on these instructions?

From the RISC-V ISA Spec:

And from https://github.com/SymbioticEDA/riscv-formal/blob/master/docs/examplebugs.md:

[aignacio]

Yes, I totally agree with you about this, so for example in jal, jalr and branches, I always verify the LSB and do not have any problems, but in the case of c.j and c.jal I'm facing these issues where the solver generates a non-zero LSB jump address like in the vcd below and it not expect the trap (spec_trap = 1), that I've got from the fail tests...I'm not sure if the solve should generate the trap condition cause looking to the checker, spec_trap will be always 0

[aignacio]

SOLVED: I'd found the bug for this, problem was a mistake due to the way I was handling priorities in terms of trap/branch taken at same time in the control unit.....