Generate signals for RISC-V Formal Verification.
Output of signals is partially delayed to get values before and after
the completion of an instruction.
The timing of the output is based on the detection of a retired
instruction. This change is detected on changes of the instruction
code itself, changes of the program counter and the valid signal.
The compressed instruction is forwarded because the decoder maps the
compressed instruction into the corresponding uncompressed instruction,
but the original instruction is needed to detect the correct format.
Register output based on the requirements from RVFI.
The specifications mandate that CSRRS/CSRRC instructions must not write to
CSRs from x0. Similarly, CSRRSI/CSRRCI instructions must not write a zero
immediate to CSRs. With this commit, these conditions are checked and
corresponding CSR operations are changed to read-only.
This commit adds checks to CSR accesses. If a CSR is accessed that is not
implemented, or if a read-only CSR is written to, an illegal instruction
exception is caused.
This commit adds the CSRs `mcycle(h)`, `minstret(h)`, `mcountinhibit` and
mhpmcounter3(h) - mhpmcounter31(h) as well as `mphmevent3 - mhpmevent31`.
The registers `mphmevent3 - mhpmevent31` are hardwired and cannot be
reconfigured.
The `nop` instruction ( `32'h00_00_00_13` ) cannot be distinguished from masked `addi` ( `17'b?, 3'b000, 5'b?, 7'h13` ) in `unique casex` statement. The other way around is not a problem, as `addi` cannot have both registers as 0x0.
This can be also fixed by replacing `unique casex` with `priority casex`. However, in my opinion, it is not a good solution as it may hide future bugs like this.
This commit simplifies the assignment of literals to enum types in
default cases by:
- defining or using existing enum values for all-zero values,
- feeding a single `1'bX` into the type cast instead of exact width
(the tools are fine with that).
- Decoding must give precedence to rs2 (i.e. instr_i[6:2]) to
switch between C.MV and C.JR.
"C.MV is only valid when rs2̸=x0; the code points with rs2=x0
correspond to the C.JR instruction. The code points with rs2̸=x0
and rd=x0 are HINTs."
- C.JR is only valid with rs1==x0. Throw an illegal instruction
exception if that's not the case.
"C.JR is only valid when rs1̸=x0; the code point with rs1=x0
is reserved." RV32 Spec, p103
All spec references based on RISC-V Unprivileged ISA
V20190305-Base-Ratification
The RV32C Specification, p106 (RISC-V Unprivileged ISA
V20190305-Base-Ratification) states:
C.ADD adds the values in registers rd and rs2 and writes the result to
register rd. C.ADD expands into add rd, rd, rs2. C.ADD is only valid
when rs2̸=x0; the code points with rs2=x0 correspond to the C.JALR and
C.EBREAK instructions. The code points with rs2̸=x0 and rd=x0 are HINTs.
This essentially says: rs2 == x0 takes precedence when decoding, that's
instr[6:2]. The current code was written with the assumption of
instr[11:7] taking precedence, thus incorrectly decoding a C.ADD HINT.
Fixeslowrisc/ibex#64
The instruction masks for the tracer are defined as parameters and contain
`?` literals, which can resolve to `1`, `0` or `X` in simulation. To cover
the `X`, the type of the masks must be changed from `int unsigned`
(standard for parameters according to guidelines) to `logic [31:0]`.
Our coding guidelines require the usage of `unique case` constructs with
proper `default` cases. This commit implements this change and also makes sure
that potential `'X` are propagated.
This commit adds a `default` to all `unique case` statements. Also, in case
FSMs reach an undefined state, the `'X` is propagated to ease detection
in simulation. Both these changes are required by our coding guidelines.
It is not obvious that the MSB in the MAC of the multiplier can safely
be ignored, and it is tedious to derive this from solely studying the
architecture of the multiplier. This comment makes clear that it is
indeed safe and also gives some reasoning.
The core ignores the lowest byte of the boot address and thus does not
support booting from addresses not aligned to 256 bytes. This commit
updates both the documentation accordingly and adds an assert to the
IF stage.
This commit replaces fully-specified, binary case statements with default
case by a simple one-line assignment to avoid linting errors. Removing the
default would also work but is more error prone if at a later point more
case are added and the statement is no longer fully-specified.
In case of interrupts, `exc_cause` carries the interrupt ID in the lower
bits and its MSB is 0 anyway. There is no need to forward only the lower
bits to the IF stage.
