-
Notifications
You must be signed in to change notification settings - Fork 94
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Mismatch between documentation and checks #9
Comments
Yeah, that's because rocket doesn't really set it yet either and PicoRV32 is only verified in non-interrupt mode (because it's using a non-standard interrupt mechanism that pre-dates the priv spec). This should be added to
That also works.
That's a bug in |
Thanks for the quick reply. As I said, I have all the checks passing without any changes to riscv-formal, so it's not urgent. |
The |
I have also encountered this, with the The earlier instruction has already retired, so its I am trying to come up with a workaround for this, but all I can think of at the moment is "retiring" a dummy I am also playing with hacking my local copy of As an aside, moving to the latest version of riscv-formal (I was around 40 commits behind) has found a lot of nasty bugs in my processor, so thank you for all the hard work there :) |
Had posted a message here about rs2_addr error getting flagged for ADDI but was wrong. I thought it was complaining about ADDI rs2_addr but it was actually rs1_addr. Nothing to see here :) |
I have been playing with riscv-formal for checking one of our small processors, and I came across a few issues where the documentation does not appear to match what the checks are actually doing. Our small processor supports a bit less than the bare minimum of RV32I (It's actually a bare minimal RV32E processor that I temporarily increased the number of registers to 32 registers just for testing with riscv-formal - as a result, its basically just an RV32I processor without counters). It supports interrupts and exceptions, but for the purposes of these tests, I have hardwired the interrupt inputs to 0. I'm currently running the same checks as picorv except I changed the isa to rv32i and I'm skipping liveness for now.
rvfi_intr
- According to rvfi.md: "rvfi_intr must be set for the first instruction that is part of a trap handler, i.e. an instruction that has a rvfi_pc_rdata that does not match the rvfi_pc_wdata of the previous instruction.". Looking at the checks, it seems like rvfi_intr is ignored. My implementation sets rvfi_pc_wdata to the start of the trap handler for each instruction that causes a fault and it passes all the checks that are done for picorv (except liveness - I'm skipping it for now).rvfi_rs1_addr
andrvfi_rs2_addr
- According to rvfi.md: "For an instruction that reads no rs1/rs2 register, this output can have an arbitrary value." Our processor always assumes rs1 is insn[19:15] and rs2 is insn[24:20]. I tried keeping those values for rvfi_rs1_addr and rvfi_rs2_addr, but I failed checks for addi, lui, and other similar instructions that don't use rs1 and/or rs2. I ended up changing rvfi_rsX_addr and rvfi_rsX_rdata to 0 if the instruction doesn't use rsX, and with that change I passed all the tests. This is consistent with what I saw when looking at the instruction check system verilog.Anyways, I'm really enjoying using with riscv-formal. Thanks!
The text was updated successfully, but these errors were encountered: