Accesses to the debug module in debug mode should never be denied by the PMP
unit. This commit implements fcov to confirm we have stimulated this particular
behaviour in relevant related states.
Illegal bins are used for incorrect behaviour (e.g. denied access in debug mode)
Other behaviours such as debug module accesses outside of debug mode are left as
ignore_bins for now. This is not explicitly disallowed by the specification, and
our implementation does not have any opinion about its validity, but external
debug modules opine that it should not be allowed. We could possibly expand the
stimulus in the future to test this condition, but it is low priority.
This improves portability across different unix-like operating systems
by using bash from the PATH, instead of bash from a hardcoded location.
Signed-off-by: Harry Callahan <hcallahan@lowrisc.org>
Some FI countermeasures in Ibex use redundancy to detect fault attacks
(e.g., the onehot encoding & checker in the RF). As synthesis tools
are great in detecting redundant logic and reducing it, this commit
puts a keep_hierarchy synthesis constraint on prim_generic* modules.
This is exactely the purpose of the prim_generic_buf, prim_generic_flop,
and prim_generic_and2 modules - having synthesis barriers to avoid
optimizations.
Signed-off-by: Pascal Nasahl <nasahlpa@lowrisc.org>
This commit adds the new `ibex_secure_ibex` variable that allows
the user to configure whether the SecureIbex configuration is
synthesized. By default, the non-SecureIbex version is
synthesized.
Signed-off-by: Pascal Nasahl <nasahlpa@lowrisc.org>
Otherwise an alert is raised if a core has a different
configuration than zero. There, the primary core would
return the non-zero value but the lockstep core zero.
This difference causes an alert.
This PR fixes this bug and passes the mvendirid and mimpid
parameters also to the lockstep core so that they are in sync
Signed-off-by: Robert Schilling <rschilling@rivosinc.com>
This commit has no functional changes, but it just rewrites the
mem_assume_t interface to improve clarity.
It also puts the error assumption inside the interface instead of
outside.
Correct the base address and size of the RAM memory model
within the simulator environment. Previously the error in
the RAM size was masking the incorrect base address (zero)
and it simulated as intended but could fail if the base
address and/or RAM size were modified.
To make the proof of DivInstrStable, this commit adds two helper
properties in the previous step. One that when an instruction is not a
multiply that the multiplier state must never leave ALBL and one that
the writeback stage must have a valid instruction in it if it is
blocking an instruction from proceeding from EX to WB. This allow
DivInstrStable to be proven with Hp 2.
The MType_{Div,DivU,Rem,RemU}_PC properties were proving very slow
before this. They were proving with Hp 45, which was very slow. This
change groups them together so that the engines can help each other out,
the N engine helps with proving these properties much faster than with
Hp alone. In the long-term it is better to capture a relavant assumption
in the proof files instead of putting this in the TCL script.
The old patchfile disabled clock gating and set ResetAll = 1.
We don't need either of these things any more with some minor
invariant tweaks. This also improves the proof script, which
should be faster now.
FetchErrRoot is very slow to prove, and via SST I discovered that it
was exploring the state space where ctrl FSM is in FIRST_FETCH, and
there was a memory load instruction latched by IF, and it causes the stall
logic to think there is a memory-induced stall.
This is unreachable state because in FIRST_FETCH there can't be instructions
latched, so add a helper property to aid the proof.
Signed-off-by: Gary Guo <gary.guo@lowrisc.org>
M extension is not currently proven. This should be disabled rather than
assumed as otherwise its property might be used to prove other
properties in the same step (and thus not performing actual work).
Signed-off-by: Gary Guo <gary.guo@lowrisc.org>
Adds a Nix environment which provides a development shell for the formal
verification flow. All dependencies are fetched and built upon entering the
shell (nix develop .#formal), except for the proprietary Cadence Jasper.
The dev shell (nix develop .#formal-dev) is identical to the normal
shell, but prints some information on how to swap out components. This
is also documented in the README.
Documentation on how to use this environment is added to the dv/formal/README.md
The provided Makefile/.tcl scripts make assumptions about the environment
they are run within which are provided by the Nix environment. Using Nix is
the recommended way to run this flow, but if you cannot do this, you will need
to duplicate the setup done by Nix in terms of environment variables and
provided dependencies.
Jasper Gold options:
- allow_unsupported_OS is required on both the machines I use.
- acquire_proj means that if JG is killed (which happens somewhat
often) the next it runs it will still be able to take ownership
of the project.
Co-authored-by: Louis-Emile Ploix <louis-emile.ploix@lowrisc.org>
Co-authored-by: Marno van der Maas <mvdmaas+git@lowrisc.org>
Co-authored-by: Gary Guo <gary.guo@lowrisc.org>
Signed-off-by: Harry Callahan <hcallahan@lowrisc.org>
This lets fusesoc do the heavy lifting in identify the correct files for us.
Fusesoc is already extensively used for this purpose for synthesis and simulation.
As part of this step, apply RTL patches that work around some current
restrictions in the formal flow to the /build fileset copied by fusesoc.
Co-authored-by: Gary Guo <gary.guo@lowrisc.org>
Signed-off-by: Harry Callahan <hcallahan@lowrisc.org>
Here's a high-level overview of what this commit does:
- Compiles Sail into SystemVerilog including patchin compiler bugs
- Create a TCL file that tells JasperGold what to prove and assume
- Check memory operations modelling the LSU
Most of these properties now prove without time-bound on the response
from memory due to alternative LSUs
- Check memory even with Smepmp errors:
Continues on top of https://github.com/riscv/sail-riscv/pull/196
- CSR verification
- Checks for instruction types such as B-Type, I-Type, R-Type
- Check illegal instructions and WFI instructions
- Using psgen language for proof generation
- Documentation on how to use the setup
- Wrap around proof that proves instructions executed in a row still
match the specification.
- Liveness proof to guarantee instructions will retire within a upper
bound of cycles.
All of these proofs make heavy use of the concept of k-induction. All
the different properties and steps are necessary to help the tool get
the useful properties it needs to prove the next step. The instruction
correctness, wrap-around and liveness all give us increased confidence
that Ibex is trace-equivalent to Sail.
Throughout this process an issue was found in Ibex where the pipeline
was not flushing properly on changing PMP registers using clear: #2193
Alternative LSUs:
This makes all top level memory properties prove quickly and at a low
proof effort (1 or 2-induction). Three 'alternative LSUs' representing
three stages of memory instructions:
1. Before the first response is received, in the EX stage
2. After the first response is received, but not the second grant,
also in the EX stage
3. Before the last response is received in the WB stage.
In each case we ask 'if the response came now, would the result
be correct?'. Similar is applied for CSRs/PC though less directly.
This is particularly interesting (read: ugly) in the case of a PMP error
wbexc_exists makes Wrap properties fast to prove. The bottleneck becomes
SpecPastNoWbexcPC, which fails only due to a bug. See the comment
in riscv.proof.
Co-authored-by: Marno van der Maas <mvdmaas+git@lowrisc.org>
Signed-off-by: Louis-Emile Ploix <louis-emile.ploix@lowrisc.org>
Instead of using default values from a package, create a top-level
parameter to define these and pass them down. This allows integrators
to specify them on a per-instance basis.
Signed-off-by: Robert Schilling <rschilling@rivosinc.com>
The "else" part of the if/else check here wasn't possible because the
surrounding else branch (starting at line 406) is already in the case
where instr[26] is zero.
When encountering certain illegal compressed instructions, incorrect instruction information was displayed. Now, illegal instructions can be printed correctly.
This removes several assertions from `ibex_controller`. They aimed to
ensure that controller behaviour was correct on exception behaviour
(e.g. ensuring that a pending interrupt will actually trigger an
interrupt). However they've proved to be flaky and hard to maintain with
multiple edge cases needing to be accounted for.
The co-simulation checking in functional verification will catch the
same issues these assertions catch. The assertions (when working
correctly) would cause a failure directly when the bug happens which
makes debugging easier. However they've added significant effort in
regression triage due to their many false failures so it's not worth the
maintenance burden.
Within formal they don't really add any value now we have the full
end-to-end formal flow.
This fixes#2193, an issue that meant bit clears in PMP related CSRs
didn't immediately apply to an instruction already in the fetch stage
due to a lack of a pipeline flush.
With this change the pipeline will flush in that scenario, fixing the
issue. It now flushes the pipeline on all CSR modifications as this
makes the pipeline more resliant against similar issues in the future
(where the list of CSRs to flush on should have been updated but
wasn't).
Previously the ibex_cs_registers module received the CSR address via the
operand muxes. This has been observed to cause timing issues in some
cases. The CSR address is always read from the same bits of the
instruction so there's no need to go via the operand muxes. With this
change the relevant instruction bits are fed straight out of the decoder
and into the ibex_cs_registers module.
This assertion wasn't quite correct if SecureIbex is false because it
was checking for the magic IbexMuBiOn value instead of just looking at
the bottom bit.
Fixes#2249.
These were noticed by someone responding to issue #2230. I think the
author's original logic was to point out that there's a path from e.g.
raddr_a_i to rdata_a_o which doesn't depend on any clock, so is
"asynchronous".
But that's the same in the other modes and also for the other register
file implementations, which don't have analogous comments.
Drop these ones.
The RISC-V Debug Specification (current release 1.0.0-rc4) in Section
A.2 states that the PMP must not disallow accesses to addresses of the
Debug Module when the hart is in debug mode, regardless of how the PMP
is configured. This commit changes the PMP accordingly.
Signed-off-by: Andreas Kurth <adk@lowrisc.org>
Although the current code isn't wrong as far as I can tell, it would be
better to initialize the lognest_name_length variable when it is
declared to avoid a build warning with older Verilator versions.
