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>
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.
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>
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.
The previous code here was a bit too hacky, so implement a solution that
directly follows the suggestion in the Cadence support article.
An example was also added to make it clear what this transformation is
achieving.
Add some more typehints, and cleanup names.
Signed-off-by: Harry Callahan <hcallahan@lowrisc.org>
It appears that VCS require expression after `iff` to be wrapped inside
parenthesis otherwise it will complain about syntax error.
This should fix the weekly VCS regression.
Signed-off-by: Gary Guo <gary.guo@lowrisc.org>
Previously the riscv_rf_intg_test skipped certain scenarios where an ECC
error from the register file should trigger an alert. This change stops
it from skipping those scenarios.
A spurious response is one that isn't associated with any on-going
request. With this new feature the memory agent can generate them
randomly when the interface is idle (i.e. there are no outstanding
requests).
This test injects a fault into different MuBi encoded signals within
the prim_ram_1p_scr and prim_ram_1p_adv and checks whether a fatal
alert is triggered.
I have excluded the addr_match signal from FI as its encoding
is not directly checked. If the signal was a MuBi True, a
fault into it is treated by the mubi4_and_hi as a False.
If the signal was a MuBi False, a fault into it is treated
by the mubi4_and_hi also as a False. Hence, no address
collision occurs and the holding register is not returned.
This PR is based on #2182 and closes#2173.
Signed-off-by: Pascal Nasahl <nasahlpa@lowrisc.org>
When an interrupt is raised the Ibex controller will move from the
DECODE state to the IRQ_TAKEN state when it chooses to handle the
interrupt. When in IRQ_TAKEN it's possible for the interrupt state to
change again which aborts the interrupt entry. This leads to mis-matches
against cosim.
This change adds a warning to flag up cases where this has occurred to
enable quick triage of failures related to this scenario.
The cosimulation environment does not know if a memory access from spike
is due to an instruction fetch or a data memory access. It uses a
heuristic to differentiate the two. Any access between the PC and the PC
+ 8 is considered an instruction fetch.
This heuristic did not correctly handle addresses at the top of the
range where the PC + 8 calculation overflows. This commit fixes the top
of range handling.
The 'pre_val' MIP addresses the scenario where MIP changes as an
instruction is excuting, this means a CSR instruction can observe a
different MIP from the one that decides whether or not that instruction
will be interrupted.
Where an access is unaligned Ibex splits it into two transactions, each
of which undergoes a PMP check. It is possible for the first half to
fail a PMP check and the second to succeed and hence produce a request
on the memory interface.
In Spike it accesses memory byte by byte and if it encounters a PMP
error for a particular byte it won't try any further bytes.
This results in a mis-match between Ibex and spike when an unaligned
transaction is split across two PMP regions, one of which allows the
access and the other doesn't. Ibex generates a transaction and spike
doesn't producing an error.
This adds a fixup into the co-simulation environment. It detects when we
have an access that fails PMP that is misaligned. Where this has
resulted in Ibex producing a memory request that spike would not we
remove it from the list of memory requests to check after checking that
the request passes PMP within spike.
Previous code working with clocking blocks synced to the raw clock
event. Instead they should sync to the clocking block event. This
ensures the values being read are the latest values rather than a cycle
old.
In particular for ibex_mem_intf_agent this meant it was unable to
produce a single cycle response to any memory transaction. With this fix
these are now observed.
This sets the C++ standard that's being used for a compiler that's
building a Verilator simulation. Recent versions of Verilator (since
5.020) require the compiler to be in C++14 mode, so passing -std=c++11
breaks the build with them.
Looking at history, -std=c++14 has been supported since GCC
6.1 (released in 2016), so I don't think this argument is going to
cause any tooling problems.
The DV flow is expecting log files to be produced with a particular file
name, without it the reporting mechanisms do not work correctly. This
adds VCS log output to a named rather rather than just capturing stdout.
Previously some $value$plusargs calls weren't explictly specifying a
format for a number to read from the plusarg. Under some simulators this
is acceptable under others it generates an error.
An instruction stall on a FENCE.I had been mistakenly placed in an
illegal bin. A FENCE.I acts much like a branch or jump so can produce
instruction stalls just as those instructions can.
