mirror of
https://github.com/lowRISC/ibex.git
synced 2025-04-22 21:07:34 -04:00
Formal equivalence checking with Sail
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>
This commit is contained in:
Louis-Emile
Marno van der Maas
parent
78739562ce
commit
82a142b14c
27 changed files with 3546 additions and 0 deletions
|
|
@ -6,6 +6,10 @@ University of Bologna under the name Zero-riscy. In December 2018, Ibex has
|
|||
been contributed to lowRISC who is maintaining and advancing the design since
|
||||
then.
|
||||
|
||||
Similarly, the Ibex `dv/formal` work was originally developed by the University of
|
||||
Oxford in the summer of 2023. In the summer of 2024 this work was extended
|
||||
for and contributed to lowRISC who is now maintaining and advancing the design.
|
||||
|
||||
Throughout the years, Ibex has seen contributions from many people and we at
|
||||
lowRISC are very thankful for all of them. This file lists the many people who
|
||||
contributed to what is called Ibex today. If you made a contribution to Ibex
|
||||
|
|
@ -38,6 +42,7 @@ please feel free to open a pull request to get your name added to this file.
|
|||
- Ivan Ribeiro
|
||||
- Karol Gugala
|
||||
- Leon Woestenberg
|
||||
- Louis-Emile Ploix
|
||||
- Luís Marques
|
||||
- Marek Pikuła
|
||||
- Markus Wegmann
|
||||
|
|
|
|||
2
dv/formal/.gitignore
vendored
Normal file
2
dv/formal/.gitignore
vendored
Normal file
|
|
@ -0,0 +1,2 @@
|
|||
jgproject
|
||||
jgproofs
|
||||
38
dv/formal/Makefile
Normal file
38
dv/formal/Makefile
Normal file
|
|
@ -0,0 +1,38 @@
|
|||
SAIL=sail
|
||||
|
||||
SAIL_RISCV_MODEL_DIR=../sail-riscv/model
|
||||
|
||||
include Sources.mk
|
||||
|
||||
PSGEN_SRCS=thm/btype.proof thm/ibex.proof thm/mem.proof thm/riscv.proof
|
||||
PSGEN_FLAGS=-root riscv -task
|
||||
|
||||
SAIL_EXTRA_SRCS=../spec/main.sail
|
||||
|
||||
SAIL_SV_FLAGS=-sv -sv-comb -sv-inregs -sv-outregs -sv-nostrings -sv-nopacked -sv-nomem -Oconstant_fold -memo-z3 \
|
||||
-sv-unreachable translate -sv-unreachable lookup_TLB -sv-unreachable translate_tlb_miss -sv-unreachable translate_tlb_hit -sv-unreachable pt_walk \
|
||||
-sv-fun2wires 2:read_ram \
|
||||
-sv-fun2wires 2:write_ram \
|
||||
-sv-fun2wires wX \
|
||||
-sv-fun2wires 2:rX \
|
||||
|
||||
.PHONY: sv
|
||||
sv:
|
||||
mkdir -p build
|
||||
python3 buildspec.py header > build/ibexspec_instrs.sv
|
||||
cd build && $(SAIL) $(SAIL_SRCS) $(SAIL_EXTRA_SRCS) $(SAIL_SV_FLAGS) `cd .. && python3 buildspec.py unreachables` -o ibexspec
|
||||
python3 spec/fix_pmp_bug.py
|
||||
python3 buildspec.py unreachable_loc_hack
|
||||
|
||||
.PHONY: reset-sub
|
||||
reset-sub:
|
||||
cd sail-riscv && git reset --hard HEAD
|
||||
|
||||
.PHONY: update-sub
|
||||
update-sub: reset-sub
|
||||
cd sail-riscv && git pull
|
||||
|
||||
.PHONY: psgen
|
||||
psgen:
|
||||
mkdir -p build
|
||||
psgen $(addprefix -path ,$(PSGEN_SRCS)) $(PSGEN_FLAGS) -sv-out build/psgen.sv -tcl-out build/psgen.tcl
|
||||
142
dv/formal/README.md
Normal file
142
dv/formal/README.md
Normal file
|
|
@ -0,0 +1,142 @@
|
|||
# End to End Formal Verification against the Sail
|
||||
|
||||
Prerequisities (in your PATH):
|
||||
- [The lowRISC fork of the Sail compiler](https://github.com/lowRISC/sail/tree/lowrisc)
|
||||
- [psgen](https://github.com/mndstrmr/psgen)
|
||||
|
||||
Build instructions:
|
||||
- `git submodule init`
|
||||
- `make psgen` to build the SV for the proofs given in `thm/`
|
||||
- `make sv` to build the SV translation of the Sail compiler. Will invoke `buildspec.py`, which can be configured to adjust which instructions are defined. By default all of them are, this is correct but slow.
|
||||
- Make the changes to Ibex described in the RTL changes.
|
||||
- `SAIL_DIR=<path to sail compiler source> jg verify.tcl`
|
||||
|
||||
## Conclusivity
|
||||
All properties are currently known to be conclusive, with the exception of M-Types. The later stages (Memory, Top, RegMatch and Wrap and some Liveness) generally take longer.
|
||||
|
||||
This means that (up to base case) Ibex is trace equivalent to the Sail (i.e. where the Sail main function is run in a loop). This means:
|
||||
- If one takes a sequence of instructions and ran Ibex on them, the same memory operations in the same order would be produced by running the Sail main function in a loop.
|
||||
- We do not prove that the instruction executed with a given PC was loaded with that PC.
|
||||
- We haven't proved that Ibex resets correctly, if it doesn't there is no trace equivalence.
|
||||
|
||||
## RTL Changes
|
||||
- `ResetAll = 1` is required for now (instead of `ResetAll = Lockstep`)
|
||||
- Fix for [#2913](https://github.com/lowRISC/ibex/issues/2193): Include `|| csr_op_o == CSR_OP_CLEAR` in the cases for `csr_pipeline_flushes` in `ibex_id_stage.sv`.
|
||||
|
||||
## Code Tour
|
||||
### Top Level Goals
|
||||
The top level objective is to get proofs for `Wrap`, `Live`, `Load`, `Store` and `NoMem`. These properties are themselves enough to prove trace equivalence (see below).
|
||||
They are intended to be simple and human interpretable, you should be able to convince yourself that those properties together imply specification conformance of Ibex (igoring the holes listed below).
|
||||
- `Wrap` proves that on each invocation of the specification (each time `spec_en` is high) the new inputs to the spec are consistent with the previous outputs of the spec.
|
||||
- `Live` proves that you will always eventually get a `spec_en` event, (i.e. it's not possible to avoid comparing with the spec). This is done by finding a very conservative but finite bound on the amount of time between spec `spec_en`.
|
||||
- `Load` and `Store` prove that the requests made to memory are correct, given a common spec/Ibex starting state. `Wrap`+`Live` proves that that starting state is actually the same. They are written only in terms of top level signals, and `instr_will_progress`, which directly implies `spec_en`.
|
||||
- `NoMem` checks that non memory instructions don't make memory requests.
|
||||
|
||||
Everything else (about 1,000 properties) exist to help `Wrap` converge.
|
||||
|
||||
Immediately below `Wrap` we have `Top`, which asserts that when any instruction retires it does so correctly. This is proved with a big case split, where we check the same for each individual instruction. Most of the work goes into proving those properties with many many invariants.
|
||||
|
||||
### Helpers
|
||||
Most Ibex specific helpers can be found in `thm/ibex.proof`, it's a mess of invariants that help the model checker significantly.
|
||||
Each one was at some point obtained by analysing some kind of k-induction trace, or just by thinking about why a property can't be easily proved in its current state.
|
||||
|
||||
The standout part of that file is `Memory`. It is the central graph induction used to prove that memory operations are well behaved.
|
||||
The definitions of the nodes are fairly clear, though their invariants can be complex. They are however fairly intuitive with some thought.
|
||||
|
||||
Arguably the most important helpers are those in `thm/riscv.proof` that individually check each instruction or type of instruction.
|
||||
They pretty much all check the same thing: The RF addr/WE is correct, the RF data is correct, the CSRs are correct, and the PC is correct.
|
||||
Most also have `use structure_fast`, which is a great help.
|
||||
|
||||
That file also contains checks for non-instructions like IRQs, illegal instructions and fetch errors. They are checked in largely similar ways.
|
||||
|
||||
Towards the end of `riscv.proof` we have Top, RegMatch and Wrap. Wrap is the goal. Top is the statement: 'every instruction is correct', and RegMatch is to help Wrap
|
||||
with the otherwise difficult RegA and RegB properties.
|
||||
|
||||
The other helpers are in `btype.proof` and `mem.proof`, which mostly just contain more graph inductions for properties that can otherwise be difficult to prove.
|
||||
|
||||
### Liveness
|
||||
The final property of `Wrap` is `Live`, which essentially proves that there will be infinite points of comparison between Ibex and the spec. It is this signal which means you don't have to trust that `spec_en` means anything. `Live` is difficult to prove. Ideally it would say `always (s_eventually spec_en)`, but in practice it has to enforce a strict bound, since proving `s_eventually` properties is quite difficult: `always (##[0:N] spec_en)`. You can find this value for `N` in `Wrap`, at the time of writing it's 212, essentially, meaning that an instruction must move to writeback at least once in 212 cycles. This is obviously an extremely weak bound, but that's fine since any finite bound is sufficient to prove liveness.
|
||||
|
||||
The proof of `Live` is fairly neat, and can be found in `ibex.proof`. It composes many properties about smaller time bounds into one large property, which conservatively just adds them all up. The major difficulty in particular is proving that if an instruction is killed, then the next one will not be. There are also issues with long running instructions and events (divide, memory, WFI).
|
||||
|
||||
By default live (and the liveness lemmas) are commented out, since it currently only applies when `TIME_LIMIT = 1`.
|
||||
|
||||
## Guide to Bug Hunting
|
||||
When you are looking to check you haven't introduced a bug you should be careful not to accidentically assume the absence of any bugs.
|
||||
|
||||
**Either prove each task in order, or run a bounded check on the property you are interested in, but do so outside of the proof structure, i.e. in the `<embedded>` task.**
|
||||
|
||||
It is enough to check `Wrap`, `Load*` and `Store*`. That said it might be more convenient to check a lower level property.
|
||||
- If you've changed the behaviour of an instruction (either its GPRs, CSRs, PC or whatever else) you should probably be checking the properties for that instruction or class of instructions. Alternatively you could check the `Top` properties.
|
||||
- If you've changed the behaviour of interrupts check the `IRQ` properties.
|
||||
- If you've changed PMP, or other memory related things check `FetchErr` as well as the data memory properties.
|
||||
- Pipeline control issues are only directly checked by `Wrap`, though will likely be picked up by something else.
|
||||
|
||||
## Proof Holes
|
||||
1. Some CSRs are not checked. See `ex_is_checkable_csr` in `top.sv` for the full list. They are not checked either because they aren't specified, can't be specified or because I haven't got around to adding them yet. Some should be easy to check. When a CSR instruction touches one of those CSRs the next round of checks is essentially just disabled, anything can happen and verification will assume at the next `spec_en`.
|
||||
2. Bus errors are assumed not to occur. They are not specified, though the bigger issue is that they would be hard to prove correctness of.
|
||||
3. There are no NMIs or fast IRQs, since there are not specified.
|
||||
4. We forbid attempting to enter debug mode, as this is also not specified.
|
||||
5. We assume `ResetAll` and no clock gating. Both of these could be fixed with probably fairly little effort.
|
||||
6. I don't check that Ibex ever handles interrupts. If it does it handle an interrupt it does so correctly.
|
||||
7. I haven't proved security, I have proved correctness, or more specificially specification conformance. If there is a bug in the spec, or a side channel somewhere, I will not find it.
|
||||
8. There is currently no proof of correctness of instruction fetch, i.e. when IF returns an instruction with a given PC, it has not been proved that that instruction was actually loaded from memory with that PC. This was proved for CHERIoT-Ibex and could probably be easily proved here too.
|
||||
9. Ibex has not been proved to reset to the correct state, there's no reason it couldn't be.
|
||||
|
||||
The precise configuration of Ibex can be found in `top.sv`, but is mostly the default with the following exceptions:
|
||||
- 4 PMP Regions, enabled
|
||||
- `BranchTargetALU = 1`
|
||||
- `ResetAll = 1` (but `SecureIbex = 0`)
|
||||
In particular, this means we have
|
||||
- `RV32MFast`
|
||||
- `RV32BNone` (Hence we are missing some instructions. This might be a good place for future work, it should be not terribly difficult to extend this)
|
||||
- `RegFileFF`
|
||||
|
||||
The following are not holes per se, but are limitations, needed to obtain convergence of liveness or others:
|
||||
1. Memory grants/responses are bounded to take at most `TIME_LIMIT` cycles in `protocol/mem.sv`. Removing this restriction would be hard. That number is 10 at time of writing, but `Wrap` and `Live` have only been tested with 1. See below for more on that.
|
||||
2. WFI instructions may not currently be enterred if they couldn't ever be exitted in `protocol/irqs.sv`. This probably should be legal behaviour, but without it liveness is false. There could probably instead be a specific carveout for this case, since it's also legal behaviour.
|
||||
3. If a WFI is enterred it must be interrupted within `WFI_BOUND` cycles, in `protocol/irqs.sv`. An `s_eventually` equivalent would be nice but in practice is very difficult to prove properties with.
|
||||
4. When an interrupt is fired, that interrupt must remain fired until a memory request is granted (i.e. as if it was some MMIO operation), in `protocol/irqs.sv`. This might be removable.
|
||||
|
||||
## Wrap Around
|
||||
The formal work includes `Wrap` properties. They check that each time the specification is 'used' the inputs to the specification equal its outputs the last time it was read.
|
||||
|
||||
Wrap properties have currently only been tested with `TIME_LIMIT = 1`, which is way lower than is ideal. Higher numbers do probably work, but I have no idea how long they will take. If JG is doing its job properly it shouldn't matter at all. The liveness properties will fail for higher time limits (this should be easy but fiddly to fix! They would ideally have limits written in terms of `TIME_LIMIT` and `WFI_BOUND`), so they are commented out by default.
|
||||
|
||||
While the implications of such a property are intuitive, we can be satisfying formal too. Define five functions:
|
||||
1. The specification function $\text{Spec} : S \times I \to S$ maps an architectural state and input to the next architectural state. It does not matter what is meant by 'next' here, but in our case $\text{Spec}$ steps through either an illegal instruction, an interrupt or a regular instruction.
|
||||
2. $\text{SpecOut} : S \times I \to O$ maps an architectural state and input to an output (i.e. memory outputs).
|
||||
3. $\text{Ibex} : A \times I \to A$ maps one micro-architectural state and input to the next micro-architectural state, where 'next' is equivalent to 'next' for $\text{Spec}$ and might span multiple clock cycles.
|
||||
4. $\text{IbexOut} : S \times I \to O$ maps a micro-architectural state and input to an output.
|
||||
5. $\text{abs} : A \to S$ maps a micro-architectural state to an architectural state.
|
||||
|
||||
The memory assertions (`Load`, `Store`, `NoMem`) prove the following statement, for any micro-architectural state $a$ and input $i$:
|
||||
```math
|
||||
\text{SpecOut}(\text{abs}(a), i) = \text{IbexOut}(a, i)
|
||||
```
|
||||
|
||||
The assertions with prefix `Wrap_` (using essentially every other property we have as lemmas) prove the following statement:
|
||||
```math
|
||||
\text{Spec}(\text{abs}(a), i) = \text{abs}(\text{Ibex}(a, i))
|
||||
```
|
||||
If $a_0$ is the reset micro-architectural state we have, by a straightforward induction, that for a sequence of $n$ inputs $I$,
|
||||
```math
|
||||
\text{Spec}^n(\text{abs}(a_0), I) = \text{abs}(\text{Ibex}^n(a_0, I))
|
||||
```
|
||||
Where I here denote $f^{n + 1}(a, I)$ to be the the left fold of `f` over `I` using `a` initially, i.e. in Haskell syntax `foldl f a I`. Combined we derive that
|
||||
```math
|
||||
\text{SpecOut}(\text{abs}(\text{Ibex}^n (a_0, I)), i) = \text{SpecOut}(\text{Spec}^n (\text{abs}(a_0), I), i) = \text{IbexOut}(\text{Ibex}^n (a_0, I), i)
|
||||
```
|
||||
|
||||
Finally, we will (but have not yet attempted to) prove that $\text{abs}(a_0) = s_0$, where $s_0$ is the initial state of the specification:
|
||||
```math
|
||||
\text{SpecOut}(\text{Spec}^n (s_0, I), i) = \text{IbexOut}(\text{Ibex}^n (a_0, I), i)
|
||||
```
|
||||
|
||||
With that we can conclude that for any sequence of $n$ steps the outputs will remain the same between the specification and Ibex, proving their complete equivalence, so long as there are infinite such steps, which the `Live` property proves.
|
||||
|
||||
Note a few things:
|
||||
1. We do not implicitly rely on (or define) 'correctness' for $\text{abs}$. Satisfying the above propositions is sufficient. In practice it will need to be 'correct' in some sense for $\text{Spec}$ to make use of it.
|
||||
2. We do not need to prove that the internal signals of Ibex mean anything, e.g. we have no explicit interpretation of the register file, the pipeline or anything else. To be convinced that I am correct you need to trust only that `Wrap`, `Live`, `Load`, `Store`, `NoMem` say what I claim they do above. If I am wrong about my interpretation about internal signals, it does not matter.
|
||||
3. In practice there are steps we cannot prove equivalence across (i.e. accessing CSRs we don't have a specification for). In such cases we just disable the next check and resume after that.
|
||||
|
||||
27
dv/formal/Sources.mk
Normal file
27
dv/formal/Sources.mk
Normal file
|
|
@ -0,0 +1,27 @@
|
|||
SAIL_XLEN := riscv_xlen32.sail
|
||||
|
||||
SAIL_CHECK_SRCS = riscv_addr_checks_common.sail riscv_addr_checks.sail riscv_misa_ext.sail
|
||||
SAIL_DEFAULT_INST = riscv_insts_base.sail riscv_insts_cext.sail riscv_insts_mext.sail riscv_insts_zicsr.sail
|
||||
|
||||
SAIL_SEQ_INST = $(SAIL_DEFAULT_INST) riscv_jalr_seq.sail
|
||||
|
||||
SAIL_SEQ_INST_SRCS = riscv_insts_begin.sail $(SAIL_SEQ_INST) riscv_insts_end.sail
|
||||
|
||||
SAIL_SYS_SRCS = riscv_csr_map.sail
|
||||
SAIL_SYS_SRCS += riscv_sys_exceptions.sail
|
||||
SAIL_SYS_SRCS += riscv_sync_exception.sail
|
||||
SAIL_SYS_SRCS += riscv_csr_ext.sail
|
||||
SAIL_SYS_SRCS += riscv_sys_control.sail
|
||||
|
||||
PRELUDE = prelude.sail $(SAIL_XLEN) prelude_mem_metadata.sail prelude_mem.sail
|
||||
|
||||
SAIL_REGS_SRCS = riscv_reg_type.sail riscv_regs.sail riscv_pc_access.sail riscv_sys_regs.sail
|
||||
SAIL_REGS_SRCS += riscv_pmp_regs.sail riscv_pmp_control.sail
|
||||
SAIL_REGS_SRCS += riscv_ext_regs.sail $(SAIL_CHECK_SRCS)
|
||||
|
||||
SAIL_ARCH_SRCS = $(PRELUDE)
|
||||
SAIL_ARCH_SRCS += riscv_types_common.sail riscv_types_ext.sail riscv_types.sail
|
||||
SAIL_ARCH_SRCS += riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail
|
||||
SAIL_ARCH_SRCS += riscv_mem.sail
|
||||
|
||||
SAIL_SRCS = $(addprefix $(SAIL_RISCV_MODEL_DIR)/,$(SAIL_ARCH_SRCS) $(SAIL_SEQ_INST_SRCS))
|
||||
113
dv/formal/buildspec.py
Normal file
113
dv/formal/buildspec.py
Normal file
|
|
@ -0,0 +1,113 @@
|
|||
# Copyright lowRISC contributors.
|
||||
# Copyright 2024 University of Oxford, see also CREDITS.md.
|
||||
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
|
||||
# Original author: Louis-Emile Ploix
|
||||
# SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
# This script is called from the Makefile.
|
||||
# Essentially it is a way to enable and disable instructions from the Sail specification to make proofs easier.
|
||||
|
||||
import json
|
||||
import re
|
||||
import sys
|
||||
|
||||
with open("instrs.json", "r") as f:
|
||||
INSTRS = set(json.load(f))
|
||||
|
||||
class SpecConfig:
|
||||
def __init__(self):
|
||||
self.instrs = set()
|
||||
|
||||
def add(self, *instrs):
|
||||
for instr in instrs:
|
||||
assert instr in INSTRS
|
||||
self.instrs.add(instr)
|
||||
|
||||
def add_all(self):
|
||||
self.instrs = INSTRS
|
||||
|
||||
def add_noncompressed(self):
|
||||
self.instrs = {x for x in INSTRS if not x.startswith("C_")}
|
||||
|
||||
def remove(self, instr):
|
||||
assert instr in INSTRS
|
||||
self.instrs.discard(instr)
|
||||
|
||||
def make_sail_unreachables(self):
|
||||
return " ".join(f"-sv_unreachable execute_{instr}" for instr in INSTRS.difference(self.instrs))
|
||||
|
||||
def make_sv_header(self):
|
||||
return "\n".join([
|
||||
"`ifndef SPEC_INSTRS",
|
||||
"`define SPEC_INSTRS",
|
||||
"",
|
||||
*[f"`define SPEC_{instr.upper()} {int(instr in self.instrs)}" for instr in INSTRS],
|
||||
"",
|
||||
"`endif"
|
||||
])
|
||||
|
||||
def add_jmps(self):
|
||||
self.add("RISCV_JAL", "RISCV_JALR")
|
||||
|
||||
def add_itype(self):
|
||||
self.add("ITYPE")
|
||||
self.add("SHIFTIOP")
|
||||
|
||||
def add_rtype(self):
|
||||
self.add("RTYPE")
|
||||
|
||||
def add_fences(self):
|
||||
self.add("FENCE", "FENCEI")
|
||||
|
||||
def add_loads(self):
|
||||
self.add("LOAD")
|
||||
|
||||
def add_stores(self):
|
||||
self.add("STORE")
|
||||
|
||||
def add_mtypes(self):
|
||||
self.add("MUL", "DIV", "REM")
|
||||
|
||||
def add_illegal(self, extra=True):
|
||||
self.add("ILLEGAL", "C_ILLEGAL")
|
||||
if extra:
|
||||
self.add("CSR")
|
||||
self.add("MRET", "WFI")
|
||||
|
||||
def add_system(self):
|
||||
self.add("ECALL", "EBREAK", "MRET", "WFI")
|
||||
|
||||
def add_csr(self):
|
||||
self.add("CSR")
|
||||
|
||||
def add_utypes(self):
|
||||
self.add("UTYPE")
|
||||
|
||||
def add_btypes(self):
|
||||
self.add("BTYPE")
|
||||
|
||||
conf = SpecConfig()
|
||||
conf.add_noncompressed()
|
||||
|
||||
if len(sys.argv) > 1:
|
||||
if sys.argv[1] == "unreachables":
|
||||
print(conf.make_sail_unreachables())
|
||||
elif sys.argv[1] == "header":
|
||||
print(conf.make_sv_header())
|
||||
elif sys.argv[1] == "unreachable_loc_hack":
|
||||
with open("build/ibexspec.sv", "r") as f:
|
||||
c = f.read()
|
||||
c = c.replace(
|
||||
"sail_reached_unreachable = 1;",
|
||||
"begin sail_reached_unreachable = 1; sail_reached_unreachable_loc = `__LINE__; end"
|
||||
).replace(
|
||||
"sail_reached_unreachable = 0;",
|
||||
"begin sail_reached_unreachable = 0; sail_reached_unreachable_loc = -1; end"
|
||||
).replace(
|
||||
"bit sail_reached_unreachable;",
|
||||
"bit sail_reached_unreachable;\n\tlogic [31:0] sail_reached_unreachable_loc;"
|
||||
)
|
||||
with open("build/ibexspec.sv", "w") as f:
|
||||
f.write(c)
|
||||
else:
|
||||
print("Intended usage is to run make sv")
|
||||
151
dv/formal/check/encodings.sv
Normal file
151
dv/formal/check/encodings.sv
Normal file
|
|
@ -0,0 +1,151 @@
|
|||
// Copyright lowRISC contributors.
|
||||
// Copyright 2024 University of Oxford, see also CREDITS.md.
|
||||
// Licensed under the Apache License, Version 2.0, see LICENSE for details.
|
||||
// Original author: Louis-Emile Ploix
|
||||
// SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
`include "../build/ibexspec_instrs.sv"
|
||||
|
||||
`ifndef CMP_INSNS
|
||||
`define CMP_INSNS
|
||||
|
||||
`define IS_ITYPE(idx) (`INSTR[6:0] == 7'b0010011 && `INSTR[14:12] == idx)
|
||||
`define IS_ADDI `IS_ITYPE(3'b000)
|
||||
`define IS_SLTI `IS_ITYPE(3'b010)
|
||||
`define IS_SLTIU `IS_ITYPE(3'b011)
|
||||
`define IS_XORI `IS_ITYPE(3'b100)
|
||||
`define IS_ORI `IS_ITYPE(3'b110)
|
||||
`define IS_ANDI `IS_ITYPE(3'b111)
|
||||
`define IS_ANY_ITYPE ( \
|
||||
`IS_ADDI | `IS_SLTI | `IS_SLTIU | `IS_XORI | \
|
||||
`IS_ORI | `IS_ANDI \
|
||||
)
|
||||
|
||||
`define ISS_ADDI (`IS_ADDI & `SPEC_ITYPE)
|
||||
`define ISS_SLTI (`IS_SLTI & `SPEC_ITYPE)
|
||||
`define ISS_SLTIU (`IS_SLTIU & `SPEC_ITYPE)
|
||||
`define ISS_XORI (`IS_XORI & `SPEC_ITYPE)
|
||||
`define ISS_ORI (`IS_ORI & `SPEC_ITYPE)
|
||||
`define ISS_ANDI (`IS_ANDI & `SPEC_ITYPE)
|
||||
|
||||
`define IS_SLLI (`IS_ITYPE(3'b001) && `INSTR[31:25] == 7'b0000000)
|
||||
`define IS_SRLI (`IS_ITYPE(3'b101) && `INSTR[31:25] == 7'b0000000)
|
||||
`define IS_SRAI (`IS_ITYPE(3'b101) && `INSTR[31:25] == 7'b0100000)
|
||||
|
||||
`define IS_SHIFTIOP (`IS_SLLI | `IS_SRLI | `IS_SRAI)
|
||||
|
||||
`define ISS_SLLI (`IS_SLLI & `SPEC_SHIFTIOP)
|
||||
`define ISS_SRLI (`IS_SRLI & `SPEC_SHIFTIOP)
|
||||
`define ISS_SRAI (`IS_SRAI & `SPEC_SHIFTIOP)
|
||||
|
||||
`define ISS_SHIFTIOP (`ISS_SLLI | `ISS_SRLI | `ISS_SRAI)
|
||||
|
||||
`define IS_RTYPE_0(idx) \
|
||||
(`INSTR[6:0] == 7'b0110011 && `INSTR[31:25] == 7'b0000000 && `INSTR[14:12] == idx)
|
||||
`define IS_RTYPE_1(idx) \
|
||||
(`INSTR[6:0] == 7'b0110011 && `INSTR[31:25] == 7'b0100000 && `INSTR[14:12] == idx)
|
||||
`define IS_ADD `IS_RTYPE_0(3'b000)
|
||||
`define IS_SUB `IS_RTYPE_1(3'b000)
|
||||
`define IS_SLL `IS_RTYPE_0(3'b001)
|
||||
`define IS_SLT `IS_RTYPE_0(3'b010)
|
||||
`define IS_SLTU `IS_RTYPE_0(3'b011)
|
||||
`define IS_XOR `IS_RTYPE_0(3'b100)
|
||||
`define IS_SRL `IS_RTYPE_0(3'b101)
|
||||
`define IS_SRA `IS_RTYPE_1(3'b101)
|
||||
`define IS_OR `IS_RTYPE_0(3'b110)
|
||||
`define IS_AND `IS_RTYPE_0(3'b111)
|
||||
|
||||
`define ISS_ADD (`IS_ADD & `SPEC_RTYPE)
|
||||
`define ISS_SUB (`IS_SUB & `SPEC_RTYPE)
|
||||
`define ISS_SLL (`IS_SLL & `SPEC_RTYPE)
|
||||
`define ISS_SLT (`IS_SLT & `SPEC_RTYPE)
|
||||
`define ISS_SLTU (`IS_SLTU & `SPEC_RTYPE)
|
||||
`define ISS_XOR (`IS_XOR & `SPEC_RTYPE)
|
||||
`define ISS_SRL (`IS_SRL & `SPEC_RTYPE)
|
||||
`define ISS_SRA (`IS_SRA & `SPEC_RTYPE)
|
||||
`define ISS_OR (`IS_OR & `SPEC_RTYPE)
|
||||
`define ISS_AND (`IS_AND & `SPEC_RTYPE)
|
||||
|
||||
`define IS_FENCETYPE(idx) ( \
|
||||
`INSTR[31:25] == 4'b0000 && `INSTR[19:15] == 5'b00000 && \
|
||||
`INSTR[11:0] == 12'b000000001111 && `INSTR[14:12] == idx)
|
||||
`define IS_FENCE (`INSTR[31:28] == 4'b0 && `INSTR[19:0] == 20'b0001111)
|
||||
`define IS_FENCEI (`INSTR == 32'h100f)
|
||||
|
||||
`define ISS_FENCE (`IS_FENCE & `SPEC_FENCE)
|
||||
`define ISS_FENCEI (`IS_FENCEI & `SPEC_FENCEI)
|
||||
|
||||
`define IS_LOAD(idx) (`INSTR[6:0] == 7'b0000011 && `INSTR[14:12] == idx)
|
||||
`define IS_LB `IS_LOAD(3'b000)
|
||||
`define IS_LH `IS_LOAD(3'b001)
|
||||
`define IS_LW `IS_LOAD(3'b010)
|
||||
`define IS_LBU `IS_LOAD(3'b100)
|
||||
`define IS_LHU `IS_LOAD(3'b101)
|
||||
|
||||
`define ISS_LB (`IS_LB & `SPEC_LOAD)
|
||||
`define ISS_LH (`IS_LH & `SPEC_LOAD)
|
||||
`define ISS_LW (`IS_LW & `SPEC_LOAD)
|
||||
`define ISS_LBU (`IS_LBU & `SPEC_LOAD)
|
||||
`define ISS_LHU (`IS_LHU & `SPEC_LOAD)
|
||||
|
||||
`define IS_STORE(idx) (`INSTR[6:0] == 7'b0100011 && `INSTR[14:12] == idx)
|
||||
`define IS_SB `IS_STORE(3'b000)
|
||||
`define IS_SH `IS_STORE(3'b001)
|
||||
`define IS_SW `IS_STORE(3'b010)
|
||||
|
||||
`define ISS_SB (`IS_SB & `SPEC_STORE)
|
||||
`define ISS_SH (`IS_SH & `SPEC_STORE)
|
||||
`define ISS_SW (`IS_SW & `SPEC_STORE)
|
||||
|
||||
`define IS_JAL (`INSTR[6:0] == 7'h6f)
|
||||
`define IS_JALR (`INSTR[6:0] == 7'h67 && `INSTR[14:12] == 3'b0)
|
||||
|
||||
`define ISS_JAL (`IS_JAL & `SPEC_RISCV_JAL)
|
||||
`define ISS_JALR (`IS_JALR & `SPEC_RISCV_JALR)
|
||||
|
||||
`define IS_MTYPE(idx) \
|
||||
(`INSTR[6:0] == 7'b0110011 && `INSTR[31:25] == 7'b0000001 && `INSTR[14:12] == idx)
|
||||
`define IS_MUL `IS_MTYPE(3'b000)
|
||||
`define IS_MULH `IS_MTYPE(3'b001)
|
||||
`define IS_MULHSH `IS_MTYPE(3'b010)
|
||||
`define IS_MULHU `IS_MTYPE(3'b011)
|
||||
`define IS_DIV `IS_MTYPE(3'b100)
|
||||
`define IS_DIVU `IS_MTYPE(3'b101)
|
||||
`define IS_REM `IS_MTYPE(3'b110)
|
||||
`define IS_REMU `IS_MTYPE(3'b111)
|
||||
|
||||
`define ISS_MUL (`IS_MUL & `SPEC_MUL)
|
||||
`define ISS_MULH (`IS_MULH & `SPEC_MUL)
|
||||
`define ISS_MULHSH (`IS_MULHSH & `SPEC_MUL)
|
||||
`define ISS_MULHU (`IS_MULHU & `SPEC_MUL)
|
||||
`define ISS_DIV (`IS_DIV & `SPEC_DIV)
|
||||
`define ISS_DIVU (`IS_DIVU & `SPEC_DIV)
|
||||
`define ISS_REM (`IS_REM & `SPEC_REM)
|
||||
`define ISS_REMU (`IS_REMU & `SPEC_REM)
|
||||
|
||||
`define IS_CSR (`INSTR[6:0] == 7'b1110011 && (|`INSTR[13:12]))
|
||||
`define CSR_ADDR (`INSTR[31:20])
|
||||
`define ISS_CSR (`IS_CSR & `SPEC_CSR)
|
||||
|
||||
`define IS_ECALL (`INSTR == 32'b00000000000000000000000001110011)
|
||||
`define ISS_ECALL (`IS_ECALL & `SPEC_ECALL)
|
||||
|
||||
`define IS_EBREAK (`INSTR == 32'b00000000000100000000000001110011)
|
||||
`define ISS_EBREAK (`IS_EBREAK & `SPEC_EBREAK)
|
||||
|
||||
`define IS_LUI (`INSTR[6:0] == 7'b0110111)
|
||||
`define ISS_LUI (`IS_LUI & `SPEC_UTYPE)
|
||||
|
||||
`define IS_AUIPC (`INSTR[6:0] == 7'b0010111)
|
||||
`define ISS_AUIPC (`IS_AUIPC & `SPEC_UTYPE)
|
||||
|
||||
`define IS_BTYPE (`INSTR[6:0] == 7'b1100011 && (`INSTR[13] -> `INSTR[14]))
|
||||
`define ISS_BTYPE (`IS_BTYPE & `SPEC_BTYPE)
|
||||
|
||||
`define IS_MRET (`INSTR == 32'b00110000001000000000000001110011)
|
||||
`define ISS_MRET (`IS_MRET & `SPEC_MRET)
|
||||
|
||||
`define IS_WFI (`INSTR == 32'b00010000010100000000000001110011)
|
||||
`define ISS_WFI (`IS_WFI & `SPEC_WFI)
|
||||
|
||||
`endif
|
||||
107
dv/formal/check/peek/abs.sv
Normal file
107
dv/formal/check/peek/abs.sv
Normal file
|
|
@ -0,0 +1,107 @@
|
|||
// Copyright lowRISC contributors.
|
||||
// Copyright 2024 University of Oxford, see also CREDITS.md.
|
||||
// Licensed under the Apache License, Version 2.0, see LICENSE for details.
|
||||
// Original author: Louis-Emile Ploix
|
||||
// SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
/*
|
||||
This file implements the abstract state for Ibex, it maps Ibex microarchitectural state to Sail architectural state.
|
||||
pre_* is the pre_state, i.e. if an instruction is starting to run now, this is the architectural state that it observes.
|
||||
post_* is the post_state, i.e. if an instruction starts in the next cycle, this is the architectural state that it will observe.
|
||||
If this is wrong it does not matter, due to the wrap around proofs.
|
||||
*/
|
||||
|
||||
/////////////// GPR Pre-State ///////////////
|
||||
|
||||
assign pre_regs[0] = 32'h0;
|
||||
for (genvar i = 1; i < 32; i++) begin: g_pre_regs
|
||||
// Resolve forwarding
|
||||
assign pre_regs[i] = (`CR.rf_write_wb && `CR.rf_waddr_wb == i) ?
|
||||
`CR.rf_wdata_fwd_wb : `RF.rf_reg[i];
|
||||
end
|
||||
|
||||
// FIXME: Redefined from ibex_cs_registers
|
||||
typedef struct packed {
|
||||
logic mie;
|
||||
logic mpie;
|
||||
priv_lvl_e mpp;
|
||||
logic mprv;
|
||||
logic tw;
|
||||
} status_t;
|
||||
|
||||
/////////////// CSR Pre-State ///////////////
|
||||
|
||||
assign pre_pc = wbexc_handling_irq? `CR.pc_if:`CR.pc_id;
|
||||
assign pre_nextpc = `CR.pc_id + (`CR.instr_is_compressed_id ? 2 : 4);
|
||||
assign pre_priv = `CSR.priv_lvl_q == PRIV_LVL_M ? Machine : User;
|
||||
assign pre_mstatus = '{
|
||||
mie: `CSR.mstatus_q.mie,
|
||||
mpie: `CSR.mstatus_q.mpie,
|
||||
tw: `CSR.mstatus_q.tw,
|
||||
mprv: `CSR.mstatus_q.mprv,
|
||||
mpp: `CSR.mstatus_q.mpp
|
||||
};
|
||||
assign pre_mip = irqsToMInterrupts(`CSR.mip);
|
||||
assign pre_mie = irqsToMInterrupts(`CSR.mie_q);
|
||||
assign pre_mcause = widenMCause(`CSR.mcause_q);
|
||||
assign pre_mtval = `CSR.mtval_q;
|
||||
assign pre_mtvec = `CSR.mtvec_q;
|
||||
assign pre_mscratch = `CSR.mscratch_q;
|
||||
assign pre_mepc = `CSR.mepc_q;
|
||||
assign pre_mcounteren = '0; // ibex hardwires to zero
|
||||
assign pre_mseccfg = mseccfgToBits(`CSRP.pmp_mseccfg_q);
|
||||
for (genvar i = 0; i < PMPNumRegions; i++) begin: g_pmp_pre
|
||||
assign pre_pmp_cfg[i] = pmpCfgToBits(`CSRP.pmp_cfg[i]);
|
||||
assign pre_pmp_addr[i] = `CSRP.pmp_addr[i];
|
||||
end
|
||||
|
||||
/////////////// CSR Post-State ///////////////
|
||||
|
||||
// Bit 0 of fetch addr n is always cleared.
|
||||
assign post_pc = `IF.branch_req ? {`IF.fetch_addr_n[31:1], 1'b0} : `CSR.pc_if_i;
|
||||
assign post_mie = `CSR.mie_en ? irqsToMInterrupts(`CSR.mie_d) : pre_mie;
|
||||
assign post_priv = `CSR.priv_lvl_d == PRIV_LVL_M ? Machine : User;
|
||||
assign post_mstatus = `CSR.mstatus_en ? '{
|
||||
mie: `CSR.mstatus_d.mie,
|
||||
mpie: `CSR.mstatus_d.mpie,
|
||||
tw: `CSR.mstatus_d.tw,
|
||||
mprv: `CSR.mstatus_d.mprv,
|
||||
mpp: `CSR.mstatus_d.mpp
|
||||
}:pre_mstatus;
|
||||
assign post_mcause = `CSR.mcause_en ? widenMCause(`CSR.mcause_d) : pre_mcause;
|
||||
assign post_mtval = `CSR.mtval_en ? `CSR.mtval_d : pre_mtval;
|
||||
assign post_mtvec = `CSR.mtvec_en ? `CSR.mtvec_d : pre_mtvec;
|
||||
assign post_mepc = `CSR.mepc_en ? `CSR.mepc_d : pre_mepc;
|
||||
assign post_mscratch = `CSR.mscratch_en? `CSR.csr_wdata_int : pre_mscratch;
|
||||
assign post_mcounteren = '0;
|
||||
assign post_mseccfg = `CSRP.pmp_mseccfg_we ? mseccfgToBits(`CSRP.pmp_mseccfg_d) : pre_mseccfg;
|
||||
for (genvar i = 0; i < PMPNumRegions; i++) begin: g_pmp_post
|
||||
assign post_pmp_cfg[i] =
|
||||
`CSRP.pmp_cfg_we[i] ? pmpCfgToBits(`CSRP.pmp_cfg_wdata[i]) : pre_pmp_cfg[i];
|
||||
assign post_pmp_addr[i] = `CSRP.pmp_addr_we[i] ? `CSR.csr_wdata_int : pre_pmp_addr[i];
|
||||
end
|
||||
|
||||
/////////////// Encoders ///////////////
|
||||
|
||||
function automatic logic [7:0] pmpCfgToBits(pmp_cfg_t cfg);
|
||||
return {cfg.lock, 2'b0, cfg.mode, cfg.exec, cfg.write, cfg.read};
|
||||
endfunction
|
||||
|
||||
function automatic logic [31:0] mseccfgToBits(pmp_mseccfg_t mseccfg);
|
||||
return {29'h0, mseccfg.rlb, mseccfg.mmwp, mseccfg.mml};
|
||||
endfunction
|
||||
|
||||
function automatic logic [31:0] irqsToMInterrupts(irqs_t irqs);
|
||||
// Sail has no notion of fast interrupts
|
||||
return
|
||||
(32'(irqs.irq_software) << 3) |
|
||||
(32'(irqs.irq_timer) << 7) |
|
||||
(32'(irqs.irq_external) << 11);
|
||||
endfunction
|
||||
|
||||
function automatic logic[31:0] widenMCause(exc_cause_t mcause);
|
||||
// Intneral exceptions are not specified, maybe we should just ignore them?
|
||||
return {mcause.irq_ext | mcause.irq_int,
|
||||
mcause.irq_int ? {26{1'b1}} : 26'b0,
|
||||
mcause.lower_cause[4:0]};
|
||||
endfunction
|
||||
279
dv/formal/check/peek/alt_lsu.sv
Normal file
279
dv/formal/check/peek/alt_lsu.sv
Normal file
|
|
@ -0,0 +1,279 @@
|
|||
// Copyright lowRISC contributors.
|
||||
// Copyright 2018 ETH Zurich and University of Bologna, see also CREDITS.md.
|
||||
// Licensed under the Apache License, Version 2.0, see LICENSE for details.
|
||||
// SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
|
||||
/**
|
||||
* Load Store Unit
|
||||
*
|
||||
* Load Store Unit, used to eliminate multiple access during processor stalls,
|
||||
* and to align bytes and halfwords.
|
||||
*/
|
||||
|
||||
`include "prim_assert.sv"
|
||||
`include "dv_fcov_macros.svh"
|
||||
|
||||
module alt_lsu #(
|
||||
parameter bit MemECC = 1'b0,
|
||||
parameter int unsigned MemDataWidth = MemECC ? 32 + 7 : 32
|
||||
) (
|
||||
input logic clk_i,
|
||||
input logic rst_ni,
|
||||
|
||||
// data interface
|
||||
output logic data_req_o,
|
||||
input logic data_gnt_i,
|
||||
input logic data_rvalid_i,
|
||||
input logic data_bus_err_i,
|
||||
input logic data_pmp_err_i,
|
||||
|
||||
output logic [31:0] data_addr_o,
|
||||
output logic data_we_o,
|
||||
output logic [3:0] data_be_o,
|
||||
output logic [MemDataWidth-1:0] data_wdata_o,
|
||||
input logic [MemDataWidth-1:0] data_rdata_i,
|
||||
|
||||
// signals to/from ID/EX stage
|
||||
input logic lsu_we_i, // write enable -> from ID/EX
|
||||
input logic [1:0] lsu_type_i, // data type: word, half word, byte -> from ID/EX
|
||||
input logic [31:0] lsu_wdata_i, // data to write to memory -> from ID/EX
|
||||
input logic lsu_sign_ext_i, // sign extension -> from ID/EX
|
||||
|
||||
output logic [31:0] lsu_rdata_o, // requested data -> to ID/EX
|
||||
output logic lsu_rdata_valid_o,
|
||||
input logic lsu_req_i, // data request -> from ID/EX
|
||||
|
||||
input logic [31:0] adder_result_ex_i, // address computed in ALU -> from ID/EX
|
||||
|
||||
output logic addr_incr_req_o, // request address increment for
|
||||
// misaligned accesses -> to ID/EX
|
||||
output logic [31:0] addr_last_o, // address of last transaction -> to controller
|
||||
// -> mtval
|
||||
// -> AGU for misaligned accesses
|
||||
|
||||
output logic lsu_req_done_o, // Signals that data request is complete
|
||||
// (only need to await final data
|
||||
// response) -> to ID/EX
|
||||
|
||||
output logic lsu_resp_valid_o, // LSU has response from transaction -> to ID/EX
|
||||
|
||||
// exception signals
|
||||
output logic load_err_o,
|
||||
output logic load_reXsp_intg_err_o,
|
||||
output logic store_err_o,
|
||||
output logic store_resp_intg_err_o,
|
||||
|
||||
output logic busy_o,
|
||||
|
||||
output logic perf_load_o,
|
||||
output logic perf_store_o,
|
||||
|
||||
input logic [31:0] addr_last_q,
|
||||
input logic [31:8] rdata_q,
|
||||
input logic [1:0] rdata_offset_q,
|
||||
input logic [1:0] data_type_q,
|
||||
input logic data_sign_ext_q,
|
||||
input logic data_we_q,
|
||||
input logic handle_misaligned_q,
|
||||
input logic pmp_err_q,
|
||||
input logic lsu_err_q
|
||||
);
|
||||
|
||||
logic [31:0] data_addr;
|
||||
logic [31:0] data_addr_w_aligned;
|
||||
logic [31:0] addr_last_d;
|
||||
|
||||
logic addr_update;
|
||||
logic ctrl_update;
|
||||
logic rdata_update;
|
||||
|
||||
logic [1:0] data_offset; // mux control for data to be written to memory
|
||||
|
||||
logic [3:0] data_be;
|
||||
logic [31:0] data_wdata;
|
||||
|
||||
logic [31:0] data_rdata_ext;
|
||||
|
||||
logic [31:0] rdata_w_ext; // word realignment for misaligned loads
|
||||
logic [31:0] rdata_h_ext; // sign extension for half words
|
||||
logic [31:0] rdata_b_ext; // sign extension for bytes
|
||||
|
||||
logic split_misaligned_access;
|
||||
logic handle_misaligned_d; // high after receiving grant for first
|
||||
// part of a misaligned access
|
||||
logic pmp_err_d;
|
||||
logic lsu_err_d;
|
||||
logic data_intg_err, data_or_pmp_err;
|
||||
|
||||
assign data_addr = adder_result_ex_i;
|
||||
assign data_offset = data_addr[1:0];
|
||||
|
||||
// Store last address for mtval + AGU for misaligned transactions. Do not update in case of
|
||||
// errors, mtval needs the (first) failing address. Where an aligned access or the first half of
|
||||
// a misaligned access sees an error provide the calculated access address. For the second half of
|
||||
// a misaligned access provide the word aligned address of the second half.
|
||||
assign addr_last_d = addr_incr_req_o ? data_addr_w_aligned : data_addr;
|
||||
|
||||
// take care of misaligned words
|
||||
always_comb begin
|
||||
unique case (rdata_offset_q)
|
||||
2'b00: rdata_w_ext = data_rdata_i[31:0];
|
||||
2'b01: rdata_w_ext = {data_rdata_i[ 7:0], rdata_q[31:8]};
|
||||
2'b10: rdata_w_ext = {data_rdata_i[15:0], rdata_q[31:16]};
|
||||
2'b11: rdata_w_ext = {data_rdata_i[23:0], rdata_q[31:24]};
|
||||
default: rdata_w_ext = data_rdata_i[31:0];
|
||||
endcase
|
||||
end
|
||||
|
||||
////////////////////
|
||||
// Sign extension //
|
||||
////////////////////
|
||||
|
||||
// sign extension for half words
|
||||
always_comb begin
|
||||
unique case (rdata_offset_q)
|
||||
2'b00: begin
|
||||
if (!data_sign_ext_q) begin
|
||||
rdata_h_ext = {16'h0000, data_rdata_i[15:0]};
|
||||
end else begin
|
||||
rdata_h_ext = {{16{data_rdata_i[15]}}, data_rdata_i[15:0]};
|
||||
end
|
||||
end
|
||||
|
||||
2'b01: begin
|
||||
if (!data_sign_ext_q) begin
|
||||
rdata_h_ext = {16'h0000, data_rdata_i[23:8]};
|
||||
end else begin
|
||||
rdata_h_ext = {{16{data_rdata_i[23]}}, data_rdata_i[23:8]};
|
||||
end
|
||||
end
|
||||
|
||||
2'b10: begin
|
||||
if (!data_sign_ext_q) begin
|
||||
rdata_h_ext = {16'h0000, data_rdata_i[31:16]};
|
||||
end else begin
|
||||
rdata_h_ext = {{16{data_rdata_i[31]}}, data_rdata_i[31:16]};
|
||||
end
|
||||
end
|
||||
|
||||
2'b11: begin
|
||||
if (!data_sign_ext_q) begin
|
||||
rdata_h_ext = {16'h0000, data_rdata_i[7:0], rdata_q[31:24]};
|
||||
end else begin
|
||||
rdata_h_ext = {{16{data_rdata_i[7]}}, data_rdata_i[7:0], rdata_q[31:24]};
|
||||
end
|
||||
end
|
||||
|
||||
default: rdata_h_ext = {16'h0000, data_rdata_i[15:0]};
|
||||
endcase // case (rdata_offset_q)
|
||||
end
|
||||
|
||||
// sign extension for bytes
|
||||
always_comb begin
|
||||
unique case (rdata_offset_q)
|
||||
2'b00: begin
|
||||
if (!data_sign_ext_q) begin
|
||||
rdata_b_ext = {24'h00_0000, data_rdata_i[7:0]};
|
||||
end else begin
|
||||
rdata_b_ext = {{24{data_rdata_i[7]}}, data_rdata_i[7:0]};
|
||||
end
|
||||
end
|
||||
|
||||
2'b01: begin
|
||||
if (!data_sign_ext_q) begin
|
||||
rdata_b_ext = {24'h00_0000, data_rdata_i[15:8]};
|
||||
end else begin
|
||||
rdata_b_ext = {{24{data_rdata_i[15]}}, data_rdata_i[15:8]};
|
||||
end
|
||||
end
|
||||
|
||||
2'b10: begin
|
||||
if (!data_sign_ext_q) begin
|
||||
rdata_b_ext = {24'h00_0000, data_rdata_i[23:16]};
|
||||
end else begin
|
||||
rdata_b_ext = {{24{data_rdata_i[23]}}, data_rdata_i[23:16]};
|
||||
end
|
||||
end
|
||||
|
||||
2'b11: begin
|
||||
if (!data_sign_ext_q) begin
|
||||
rdata_b_ext = {24'h00_0000, data_rdata_i[31:24]};
|
||||
end else begin
|
||||
rdata_b_ext = {{24{data_rdata_i[31]}}, data_rdata_i[31:24]};
|
||||
end
|
||||
end
|
||||
|
||||
default: rdata_b_ext = {24'h00_0000, data_rdata_i[7:0]};
|
||||
endcase // case (rdata_offset_q)
|
||||
end
|
||||
|
||||
// select word, half word or byte sign extended version
|
||||
always_comb begin
|
||||
unique case (data_type_q)
|
||||
2'b00: data_rdata_ext = rdata_w_ext;
|
||||
2'b01: data_rdata_ext = rdata_h_ext;
|
||||
2'b10,2'b11: data_rdata_ext = rdata_b_ext;
|
||||
default: data_rdata_ext = rdata_w_ext;
|
||||
endcase // case (data_type_q)
|
||||
end
|
||||
|
||||
///////////////////////////////
|
||||
// Read data integrity check //
|
||||
///////////////////////////////
|
||||
|
||||
assign data_intg_err = 1'b0;
|
||||
|
||||
/////////////
|
||||
// LSU FSM //
|
||||
/////////////
|
||||
|
||||
// check for misaligned accesses that need to be split into two word-aligned accesses
|
||||
assign split_misaligned_access =
|
||||
((lsu_type_i == 2'b00) && (data_offset != 2'b00)) || // misaligned word access
|
||||
((lsu_type_i == 2'b01) && (data_offset == 2'b11)); // misaligned half-word access
|
||||
|
||||
/////////////
|
||||
// Outputs //
|
||||
/////////////
|
||||
|
||||
assign data_or_pmp_err = lsu_err_q | data_bus_err_i | pmp_err_q;
|
||||
assign lsu_resp_valid_o = (data_rvalid_i | pmp_err_q);
|
||||
assign lsu_rdata_valid_o =
|
||||
data_rvalid_i & ~data_or_pmp_err & ~data_we_q & ~data_intg_err;
|
||||
|
||||
// output to register file
|
||||
assign lsu_rdata_o = data_rdata_ext;
|
||||
|
||||
// output data address must be word aligned
|
||||
assign data_addr_w_aligned = {data_addr[31:2], 2'b00};
|
||||
|
||||
// output to data interface
|
||||
assign data_addr_o = data_addr_w_aligned;
|
||||
assign data_we_o = lsu_we_i;
|
||||
assign data_be_o = data_be;
|
||||
|
||||
/////////////////////////////////////
|
||||
// Write data integrity generation //
|
||||
/////////////////////////////////////
|
||||
|
||||
// SEC_CM: BUS.INTEGRITY
|
||||
assign data_wdata_o = data_wdata;
|
||||
|
||||
// output to ID stage: mtval + AGU for misaligned transactions
|
||||
assign addr_last_o = addr_last_q;
|
||||
|
||||
// Signal a load or store error depending on the transaction type outstanding
|
||||
assign load_err_o = data_or_pmp_err & ~data_we_q & lsu_resp_valid_o;
|
||||
assign store_err_o = data_or_pmp_err & data_we_q & lsu_resp_valid_o;
|
||||
// Integrity errors are their own category for timing reasons. load_err_o is factored directly
|
||||
// into data_req_o to enable synchronous exception on load errors without performance loss (An
|
||||
// upcoming load cannot request until the current load has seen its response, so the earliest
|
||||
// point the new request can be sent is the same cycle the response is seen). If load_err_o isn't
|
||||
// factored into data_req_o there would have to be a stall cycle between all back to back loads.
|
||||
// The data_intg_err signal is generated combinatorially from the incoming data_rdata_i. Were it
|
||||
// to be factored into load_err_o there would be a feedthrough path from data_rdata_i to
|
||||
// data_req_o which is undesirable.
|
||||
assign load_resp_intg_err_o = data_intg_err & data_rvalid_i & ~data_we_q;
|
||||
assign store_resp_intg_err_o = data_intg_err & data_rvalid_i & data_we_q;
|
||||
endmodule
|
||||
126
dv/formal/check/peek/compare_helper.sv
Normal file
126
dv/formal/check/peek/compare_helper.sv
Normal file
|
|
@ -0,0 +1,126 @@
|
|||
// Copyright lowRISC contributors.
|
||||
// Copyright 2024 University of Oxford, see also CREDITS.md.
|
||||
// Licensed under the Apache License, Version 2.0, see LICENSE for details.
|
||||
// Original author: Louis-Emile Ploix
|
||||
// SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
/*
|
||||
These are various signals used in assertions. A lot of it is just convenient instruction checks,
|
||||
some of it is checking spec conformance.
|
||||
*/
|
||||
|
||||
`define INSTR wbexc_decompressed_instr
|
||||
|
||||
assign wbexc_is_pres_load_instr = `ISS_LB | `ISS_LBU | `ISS_LH | `ISS_LHU | `ISS_LW;
|
||||
assign wbexc_is_pres_store_instr = `ISS_SB | `ISS_SH | `ISS_SW;
|
||||
assign wbexc_is_pres_mem_instr = wbexc_is_pres_load_instr | wbexc_is_pres_store_instr;
|
||||
|
||||
assign wbexc_is_load_instr = `IS_LB | `IS_LBU | `IS_LH | `IS_LHU | `IS_LW;
|
||||
assign wbexc_is_store_instr = `IS_SB | `IS_SH | `IS_SW;
|
||||
|
||||
assign wbexc_is_mem_instr = `IS_LB | `IS_LBU | `IS_SB |
|
||||
`IS_LH | `IS_LHU | `IS_SH |
|
||||
`IS_LW | `IS_SW;
|
||||
assign wbexc_is_wfi = `IS_WFI & ~wbexc_fetch_err;
|
||||
`undef INSTR
|
||||
|
||||
`define INSTR `CR.instr_rdata_id
|
||||
assign ex_is_load_instr = `IS_LB | `IS_LBU | `IS_LH | `IS_LHU | `IS_LW;
|
||||
assign ex_is_store_instr = `IS_SB | `IS_SH | `IS_SW;
|
||||
assign ex_is_mem_instr = ex_is_load_instr | ex_is_store_instr;
|
||||
|
||||
assign ex_is_pres_load_instr = `ISS_LB | `ISS_LBU | `ISS_LH | `ISS_LHU | `ISS_LW;
|
||||
assign ex_is_pres_store_instr = `ISS_SB | `ISS_SH | `ISS_SW;
|
||||
assign ex_is_pres_mem_instr = ex_is_pres_load_instr | ex_is_pres_store_instr;
|
||||
|
||||
assign ex_is_pres_btype = `ISS_BTYPE;
|
||||
assign ex_is_pres_jump = `ISS_JAL | `ISS_JALR;
|
||||
assign ex_is_wfi = `IS_WFI;
|
||||
assign ex_is_rtype = `IS_ADD | `IS_SUB | `IS_SLL | `IS_SLT | `IS_SLTU | `IS_XOR | `IS_SRL | `IS_SRA | `IS_OR | `IS_AND;
|
||||
assign ex_is_div = `IS_DIV | `IS_DIVU | `IS_REM | `IS_REMU;
|
||||
`undef INSTR
|
||||
|
||||
// real_write checks that there is a write and the dest reg is not x0
|
||||
logic dut_real_write, spec_real_write;
|
||||
assign dut_real_write = `WB.rf_we_wb_o & (|`WB.rf_waddr_wb_o);
|
||||
assign spec_real_write = wbexc_post_wX_en & (|wbexc_post_wX_addr);
|
||||
|
||||
assign addr_match = dut_real_write == spec_real_write &&
|
||||
(spec_real_write -> `WB.rf_waddr_wb_o == wbexc_post_wX_addr);
|
||||
assign data_match = (spec_real_write && dut_real_write) -> wbexc_post_wX == `WB.rf_wdata_wb_o;
|
||||
|
||||
assign finishing_executed = wbexc_finishing & ~wbexc_fetch_err;
|
||||
|
||||
/*
|
||||
Select CSRs based on the current state of the follower, in particular:
|
||||
- In most cases we compare the CSRs that were about to written at the end of ID/EX to the CSRs from the spec also
|
||||
from that time. It's unfortunate to do that now but not a huge hassle.
|
||||
- In the case of an exception or WFI we compare the CSRs about to be written now with the CSRs from the spec at the end of ID/EX
|
||||
- In the case of an IRQ we compare the the CSRs about to be written now with the CSRs from the spec now
|
||||
*/
|
||||
|
||||
`define INSTR `CR.instr_rdata_id
|
||||
|
||||
logic use_curr_dut, use_curr_spec;
|
||||
assign use_curr_dut = wbexc_err | wbexc_handling_irq;
|
||||
assign use_curr_spec = wbexc_handling_irq;
|
||||
|
||||
`define X(c) assign wbexc_dut_cmp_post_``c = use_curr_dut ? post_``c : wbexc_dut_post_``c;
|
||||
`X_EACH_CSR
|
||||
`undef X
|
||||
|
||||
`define X(c) assign wbexc_spec_cmp_post_``c = use_curr_spec ? spec_post_``c : wbexc_post_``c;
|
||||
`X_EACH_CSR
|
||||
`undef X
|
||||
|
||||
`define X_DISABLE_PC
|
||||
`define X(c) wbexc_dut_cmp_post_``c == wbexc_spec_cmp_post_``c &&
|
||||
assign csrs_match = `X_EACH_CSR 1;
|
||||
`undef X
|
||||
`undef X_DISABLE_PC
|
||||
|
||||
assign pc_match = wbexc_dut_cmp_post_pc == wbexc_spec_cmp_post_pc;
|
||||
|
||||
`define X_DISABLE_PC
|
||||
assign csrs_didnt_change =
|
||||
`define X(c) pre_``c == wbexc_dut_post_``c &&
|
||||
`X_EACH_CSR
|
||||
`undef X
|
||||
1;
|
||||
`undef X_DISABLE_PC
|
||||
|
||||
`define X_DISABLE_PC
|
||||
assign ex_csrs_match =
|
||||
`define X(c) post_``c == spec_post_``c &&
|
||||
`X_EACH_CSR
|
||||
`undef X
|
||||
1;
|
||||
`undef X_DISABLE_PC
|
||||
|
||||
assign csrs_match_non_exc =
|
||||
`define X(c) post_``c == wbexc_post_``c &&
|
||||
`X(mstatus.mprv)
|
||||
`X(mstatus.tw)
|
||||
`X(mie)
|
||||
`X(mtvec)
|
||||
`X(mscratch)
|
||||
`X(mcounteren)
|
||||
`X(pmp_cfg)
|
||||
`X(pmp_addr)
|
||||
`X(mseccfg)
|
||||
`undef X
|
||||
1;
|
||||
|
||||
assign ex_csrs_match_non_exc =
|
||||
`define X(c) post_``c == spec_post_``c &&
|
||||
`X(mstatus.mprv)
|
||||
`X(mstatus.tw)
|
||||
`X(mie)
|
||||
`X(mtvec)
|
||||
`X(mscratch)
|
||||
`X(mcounteren)
|
||||
`X(pmp_cfg)
|
||||
`X(pmp_addr)
|
||||
`X(mseccfg)
|
||||
`undef X
|
||||
1;
|
||||
132
dv/formal/check/peek/follower.sv
Normal file
132
dv/formal/check/peek/follower.sv
Normal file
|
|
@ -0,0 +1,132 @@
|
|||
// Copyright lowRISC contributors.
|
||||
// Copyright 2024 University of Oxford, see also CREDITS.md.
|
||||
// Licensed under the Apache License, Version 2.0, see LICENSE for details.
|
||||
// Original author: Louis-Emile Ploix
|
||||
// SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
/*
|
||||
The following implements the pipeline follower. It is pretty simple since the pipeline is short.
|
||||
|
||||
The top of this file contains signals to indicate when an instruction moves from a pipeline stage,
|
||||
and when it does so on what terms.
|
||||
|
||||
We record both the spec post state and the implementation CSR post state as soon as the instruction moves on from ID/EX.
|
||||
The latter is stored so that we can make comparisons at the same time, independent of when the instruction retires. We
|
||||
probably could do this earlier in the cases where no exception occurs, but that would require special treatment for
|
||||
exception vs non-exception cases. In fairness there is already a difference, but that's only a case split which can be unified.
|
||||
*/
|
||||
|
||||
`define INSTR `CR.instr_rdata_id
|
||||
|
||||
// These control signals are all extremely specific and probably very fragile.
|
||||
|
||||
assign ex_success = `ID.instr_done;
|
||||
assign ex_err = `IDC.exc_req_d;
|
||||
assign ex_kill = `ID.wb_exception | ~`ID.controller_run;
|
||||
// Note that this only kills instructions because e.g. of a jump ahead of it or an exception
|
||||
|
||||
assign exc_finishing = `IDC.ctrl_fsm_cs == `ID.controller_i.FLUSH;
|
||||
assign wbexc_handling_irq = `IDC.ctrl_fsm_cs == `ID.controller_i.IRQ_TAKEN;
|
||||
|
||||
assign wb_finishing = wbexc_is_wfi? wfi_will_finish:`CR.instr_done_wb;
|
||||
|
||||
assign wfi_will_finish = `IDC.ctrl_fsm_cs == `ID.controller_i.FLUSH;
|
||||
|
||||
assign wbexc_err = wbexc_ex_err |
|
||||
`IDC.wb_exception_o |
|
||||
((`IDC.ctrl_fsm_cs == `ID.controller_i.FLUSH) & ~wbexc_csr_pipe_flush);
|
||||
// CSR pipe flushes don't count as exceptions
|
||||
|
||||
assign wbexc_finishing =
|
||||
wbexc_exists & (wbexc_err ? exc_finishing : wb_finishing);
|
||||
|
||||
assign instr_will_progress = (~wbexc_exists | wbexc_finishing) & ~ex_kill & (ex_success | ex_err);
|
||||
|
||||
always_comb begin
|
||||
if (`CR.instr_new_id) begin
|
||||
ex_has_branched_d = 1'b0;
|
||||
end else begin
|
||||
ex_has_branched_d = ex_has_branched_q;
|
||||
end
|
||||
|
||||
ex_has_branched_d = (ex_has_branched_d | `IF.branch_req) && ~ex_kill && (`IDC.ctrl_fsm_cs == `IDC.DECODE);
|
||||
end
|
||||
|
||||
always @(posedge clk_i or negedge rst_ni) begin
|
||||
if (~rst_ni) begin
|
||||
wbexc_exists <= 1'b0;
|
||||
ex_has_compressed_instr <= 1'b0;
|
||||
ex_has_branched_q <= 1'b0;
|
||||
wbexc_csr_pipe_flush <= 1'b0;
|
||||
end else begin
|
||||
if (wbexc_finishing) begin
|
||||
wbexc_exists <= 1'b0;
|
||||
end
|
||||
|
||||
ex_has_branched_q <= ex_has_branched_d;
|
||||
if (instr_will_progress) begin
|
||||
ex_has_branched_q <= 1'b0;
|
||||
wbexc_post_wX <= spec_post_wX;
|
||||
wbexc_post_wX_addr <= spec_post_wX_addr;
|
||||
wbexc_post_wX_en <= spec_post_wX_en;
|
||||
|
||||
`define X(n) wbexc_post_``n <= spec_post_``n;
|
||||
`X_EACH_CSR
|
||||
`undef X
|
||||
|
||||
`define X(n) wbexc_dut_post_``n <= post_``n;
|
||||
`X_EACH_CSR
|
||||
`undef X
|
||||
|
||||
wbexc_instr <= ex_compressed_instr;
|
||||
wbexc_decompressed_instr <= `CR.instr_rdata_id;
|
||||
wbexc_compressed_illegal <= `CR.illegal_c_insn_id;
|
||||
wbexc_exists <= 1'b1;
|
||||
wbexc_ex_err <= ex_err;
|
||||
wbexc_fetch_err <= `ID.instr_fetch_err_i;
|
||||
wbexc_post_int_err <= spec_int_err;
|
||||
wbexc_illegal <= `CR.illegal_insn_id;
|
||||
wbexc_pc <= `CR.pc_id;
|
||||
wbexc_csr_pipe_flush <= `IDC.csr_pipe_flush;
|
||||
wbexc_is_checkable_csr <= ex_is_checkable_csr;
|
||||
|
||||
wbexc_spec_mem_read_fst_rdata <= spec_mem_read_fst_rdata;
|
||||
wbexc_spec_mem_read_snd_rdata <= spec_mem_read_snd_rdata;
|
||||
wbexc_mem_had_snd_req <= mem_gnt_snd_q | mem_gnt_snd_d;
|
||||
end
|
||||
|
||||
if (`IF.if_id_pipe_reg_we) begin
|
||||
ex_compressed_instr <= `IF.if_instr_rdata;
|
||||
ex_has_compressed_instr <= 1'b1;
|
||||
end
|
||||
end
|
||||
end
|
||||
|
||||
assign spec_en = wbexc_handling_irq | instr_will_progress;
|
||||
// The definition of spec_en doesn't matter so long as it's live (which it is since
|
||||
// instr will progress is live), so long as the necessary wraparound properties prove.
|
||||
|
||||
always @(posedge clk_i) begin
|
||||
if (~rst_ni) begin
|
||||
has_spec_past = 1'b0;
|
||||
spec_past_has_reg = 32'b0;
|
||||
end else if (spec_en) begin
|
||||
has_spec_past = `IS_CSR -> ex_is_checkable_csr;
|
||||
|
||||
if (spec_post_wX_en) begin
|
||||
spec_past_regs[spec_post_wX_addr] = spec_post_wX;
|
||||
spec_past_has_reg[spec_post_wX_addr] = 1'b1;
|
||||
end
|
||||
if (`IS_CSR & ~ex_is_checkable_csr) begin
|
||||
// Clear out everything, since we don't know what has been written to any more
|
||||
// We could be stricter but there's little point in doing so.
|
||||
spec_past_has_reg = 32'b0;
|
||||
end
|
||||
|
||||
`define X(n) spec_past_``n = spec_post_``n;
|
||||
`X_EACH_CSR
|
||||
`undef X
|
||||
end
|
||||
end
|
||||
|
||||
`undef INSTR
|
||||
122
dv/formal/check/peek/mem.sv
Normal file
122
dv/formal/check/peek/mem.sv
Normal file
|
|
@ -0,0 +1,122 @@
|
|||
// Copyright lowRISC contributors.
|
||||
// Copyright 2024 University of Oxford, see also CREDITS.md.
|
||||
// Licensed under the Apache License, Version 2.0, see LICENSE for details.
|
||||
// Original author: Louis-Emile Ploix
|
||||
// SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
/*
|
||||
This file implements the tracking of ibex memory. It (by assumption) sets data_rvalid_i to the corresponding value that was
|
||||
sent to the spec. The interpretation of the signals used is justified in the proofs.
|
||||
*/
|
||||
|
||||
logic has_snd_req;
|
||||
assign has_snd_req = mem_gnt_snd_d | (mem_gnt_fst_q & `CR.data_req_out);
|
||||
|
||||
logic outstanding_resp;
|
||||
assign outstanding_resp = `CR.outstanding_load_wb | `CR.outstanding_store_wb;
|
||||
|
||||
/*
|
||||
Some definitions:
|
||||
- An 'early response' is a response made to a memory instruction before the instruction has progressed to the WB stage,
|
||||
i.e. while it is still in the ID/EX stage. This is only possible for multi-request instructions, and only one
|
||||
early response can be made.
|
||||
- A 'late response' is a response received during the WB stage. There can be at most one late response, since
|
||||
if a memory instruction sends two requests, it won't go to WB until it has sent one request.
|
||||
Responses are given in the order they are requested, so it suffices to check if WB is waiting on a response.
|
||||
*/
|
||||
logic early_resp, late_resp;
|
||||
assign early_resp = data_rvalid_i & ~outstanding_resp;
|
||||
assign late_resp = data_rvalid_i & outstanding_resp;
|
||||
|
||||
// If we receive an early response, give it the data sent to the spec directly
|
||||
LoadMemEarlyResp: assume property (
|
||||
early_resp |-> data_rdata_i == spec_mem_read_fst_rdata
|
||||
);
|
||||
|
||||
// If we have a late response, and this is the first response send the low spec data
|
||||
LoadMemLateRespFirst: assume property (
|
||||
late_resp & ~wbexc_mem_had_snd_req |-> data_rdata_i == wbexc_spec_mem_read_fst_rdata
|
||||
);
|
||||
|
||||
// If we have a late response, and this is the second response, send the high spec data
|
||||
LoadMemLateRespSecond: assume property (
|
||||
late_resp & wbexc_mem_had_snd_req |-> data_rdata_i == wbexc_spec_mem_read_snd_rdata
|
||||
);
|
||||
|
||||
// The spec read data cannot change while an instruction is running, only when there is a new one
|
||||
// Note these values are undriven, they are not from the spec as the name would suggest
|
||||
SpecReadDataKeep: assume property (~instr_will_progress |=>
|
||||
spec_mem_read_fst_rdata == $past(spec_mem_read_fst_rdata) &&
|
||||
spec_mem_read_snd_rdata == $past(spec_mem_read_snd_rdata)
|
||||
);
|
||||
|
||||
// Tracks what requests/grants have been since instr_will_progress (and thus spec_en).
|
||||
// It's not dependent on any internal signal besides instr_will_progress, which implies
|
||||
// spec_en, so is 'safe'.
|
||||
assign mem_gnt_fst_d = mem_gnt_fst_q | data_gnt_i;
|
||||
assign mem_gnt_snd_d = mem_gnt_snd_q | (data_gnt_i & mem_gnt_fst_q);
|
||||
|
||||
assign mem_req_fst_d = data_req_o & ~mem_gnt_fst_q;
|
||||
assign mem_req_snd_d = data_req_o & mem_gnt_fst_q;
|
||||
|
||||
always @(posedge clk_i or negedge rst_ni) begin
|
||||
if (~rst_ni | instr_will_progress) begin
|
||||
mem_gnt_fst_q <= 1'b0;
|
||||
mem_gnt_snd_q <= 1'b0;
|
||||
end else begin
|
||||
mem_gnt_fst_q <= mem_gnt_fst_d;
|
||||
mem_gnt_snd_q <= mem_gnt_snd_d;
|
||||
end
|
||||
end
|
||||
|
||||
`define ALT_LSU_STATE_COPY \
|
||||
.data_rvalid_i(1'b1), \
|
||||
.data_bus_err_i(1'b0), \
|
||||
.data_we_q(`LSU.data_we_q), \
|
||||
.handle_misaligned_q(`LSU.handle_misaligned_q), \
|
||||
.pmp_err_q(`LSU.pmp_err_q), \
|
||||
.lsu_err_q(`LSU.lsu_err_q), \
|
||||
|
||||
alt_lsu alt_lsu_late_i (
|
||||
.data_rdata_i(
|
||||
~wbexc_mem_had_snd_req ?
|
||||
wbexc_spec_mem_read_fst_rdata :
|
||||
wbexc_spec_mem_read_snd_rdata
|
||||
),
|
||||
`ALT_LSU_STATE_COPY
|
||||
.data_type_q(`LSU.data_type_q),
|
||||
.rdata_offset_q(`LSU.rdata_offset_q),
|
||||
.data_sign_ext_q(`LSU.data_sign_ext_q),
|
||||
.rdata_q(`LSU.rdata_q)
|
||||
);
|
||||
|
||||
logic [31:0] alt_lsu_late_res;
|
||||
assign alt_lsu_late_res = alt_lsu_late_i.lsu_rdata_o;
|
||||
|
||||
alt_lsu alt_lsu_very_early_i (
|
||||
.data_rdata_i(
|
||||
~`LSU.split_misaligned_access ?
|
||||
spec_mem_read_fst_rdata :
|
||||
spec_mem_read_snd_rdata
|
||||
),
|
||||
`ALT_LSU_STATE_COPY
|
||||
.data_type_q(mem_gnt_fst_q ? `LSU.data_type_q : `LSU.lsu_type_i),
|
||||
.data_sign_ext_q(mem_gnt_fst_q ? `LSU.data_sign_ext_q : `LSU.lsu_sign_ext_i),
|
||||
.rdata_offset_q(mem_gnt_fst_q ? `LSU.rdata_offset_q : `LSU.data_offset),
|
||||
.rdata_q(spec_mem_read_fst_rdata[31:8])
|
||||
);
|
||||
|
||||
logic [31:0] alt_lsu_very_early_res;
|
||||
assign alt_lsu_very_early_res = alt_lsu_very_early_i.lsu_rdata_o;
|
||||
|
||||
alt_lsu alt_lsu_early_i (
|
||||
.data_rdata_i(spec_mem_read_snd_rdata),
|
||||
`ALT_LSU_STATE_COPY
|
||||
.data_type_q(`LSU.data_type_q),
|
||||
.data_sign_ext_q(`LSU.data_sign_ext_q),
|
||||
.rdata_offset_q(`LSU.rdata_offset_q),
|
||||
.rdata_q(`LSU.rdata_q)
|
||||
);
|
||||
|
||||
logic [31:0] alt_lsu_early_res;
|
||||
assign alt_lsu_early_res = alt_lsu_early_i.lsu_rdata_o;
|
||||
26
dv/formal/check/protocol/irqs.sv
Normal file
26
dv/formal/check/protocol/irqs.sv
Normal file
|
|
@ -0,0 +1,26 @@
|
|||
// Copyright lowRISC contributors.
|
||||
// Copyright 2024 University of Oxford, see also CREDITS.md.
|
||||
// Licensed under the Apache License, Version 2.0, see LICENSE for details.
|
||||
// Original author: Louis-Emile Ploix
|
||||
// SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
/*
|
||||
The following give the protocol that IRQs must follow.
|
||||
*/
|
||||
|
||||
// The Sail does not specify either of these
|
||||
NoNMI: assume property (~irq_nm_i);
|
||||
NoFastIRQ: assume property (~(|irq_fast_i));
|
||||
|
||||
// IRQs must remain active until they are cleared by some MMIO memory request
|
||||
// The alternative is that IRQs disappear after just one cycle or something
|
||||
MIPFair: assume property (
|
||||
(|`CSR.mip) |=>
|
||||
$past(`CSR.mip) == ($past(`CSR.mip) & `CSR.mip) || data_gnt_i
|
||||
);
|
||||
|
||||
`define WFI_BOUND 20
|
||||
// If we are asleep we must eventually wake up. This is validated by the WFIStart assumption,
|
||||
// which ensures that this is actually possible. We make the time bounded instead of s_eventually
|
||||
// for conclusivity purposes. This can be commented out if you don't care about liveness.
|
||||
WFIWakeUp: assume property (`IDC.ctrl_fsm_cs == SLEEP |-> ##[0:`WFI_BOUND] `IDC.irq_pending_i);
|
||||
49
dv/formal/check/protocol/mem.sv
Normal file
49
dv/formal/check/protocol/mem.sv
Normal file
|
|
@ -0,0 +1,49 @@
|
|||
// Copyright lowRISC contributors.
|
||||
// Copyright 2024 University of Oxford, see also CREDITS.md.
|
||||
// Licensed under the Apache License, Version 2.0, see LICENSE for details.
|
||||
// Original author: Louis-Emile Ploix
|
||||
// SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
/*
|
||||
The following describes the protocol for the memory interface to Ibex, as defined by the documentation.
|
||||
|
||||
In this case all responses must be within bounded time (`TIME_BOUND cycles). Removing the bound
|
||||
leaves some properties inconclusive.
|
||||
*/
|
||||
|
||||
// Sail does not specify these I don't think
|
||||
NoDataErr: assume property (~data_err_i);
|
||||
NoInstrErr: assume property (~instr_err_i);
|
||||
`define TIME_LIMIT 5
|
||||
|
||||
interface mem_assume_t(
|
||||
input logic req_o,
|
||||
input logic gnt_i,
|
||||
input logic rvalid_i
|
||||
);
|
||||
logic [7:0] outstanding_reqs_q;
|
||||
logic [7:0] outstanding_reqs;
|
||||
assign outstanding_reqs = outstanding_reqs_q + gnt_i - rvalid_i;
|
||||
|
||||
always @(posedge clk_i or negedge rst_ni) begin
|
||||
outstanding_reqs_q <= rst_ni ? outstanding_reqs : 0;
|
||||
end
|
||||
|
||||
// 1. Only send an rvalid if there is an outstanding request, but not in this cycle
|
||||
MemValidBounded: assume property (outstanding_reqs_q == 8'b0 |-> ~rvalid_i);
|
||||
// 2. Grants can only be sent when they are requested
|
||||
MemGntOnRequest: assume property (~req_o |-> ~gnt_i);
|
||||
|
||||
// Grants must respond within TIME_LIMIT cycles
|
||||
GntBound: assume property (req_o |-> ##[0:`TIME_LIMIT] gnt_i);
|
||||
|
||||
// RValid takes no more than TIME_LIMIT cycles
|
||||
MemValidTimer: assume property (outstanding_reqs != 0 |-> ##[0:`TIME_LIMIT] rvalid_i);
|
||||
|
||||
// Responses have to come eventually, implied by the above bounds so removed
|
||||
// MemGntEventually: assume property (req_o |-> s_eventually gnt_i);
|
||||
// MemRespEventually: assume property (always (s_eventually (outstanding_reqs == 8'b0)));
|
||||
endinterface
|
||||
|
||||
mem_assume_t instr_mem_assume(instr_req_o, instr_gnt_i, instr_rvalid_i);
|
||||
mem_assume_t data_mem_assume(data_req_o, data_gnt_i, data_rvalid_i);
|
||||
70
dv/formal/check/spec_instance.sv
Normal file
70
dv/formal/check/spec_instance.sv
Normal file
|
|
@ -0,0 +1,70 @@
|
|||
// Copyright lowRISC contributors.
|
||||
// Copyright 2024 University of Oxford, see also CREDITS.md.
|
||||
// Licensed under the Apache License, Version 2.0, see LICENSE for details.
|
||||
// Original author: Louis-Emile Ploix
|
||||
// SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
/*
|
||||
The following instantiates the specification via the spec api. It also chooses the mode for the spec to run in (see main.sail
|
||||
for more on that).
|
||||
|
||||
It just wires up the pre_* state to the spec_post* state.
|
||||
*/
|
||||
|
||||
t_MainMode main_mode;
|
||||
|
||||
always_comb begin
|
||||
if (wbexc_handling_irq) main_mode = MAIN_IRQ;
|
||||
else if (`ID.instr_fetch_err_i) main_mode = MAIN_IFERR;
|
||||
else main_mode = MAIN_IDEX;
|
||||
end
|
||||
|
||||
spec_api #(
|
||||
.NREGS(32)
|
||||
) spec_api_i (
|
||||
.int_err_o(spec_int_err),
|
||||
.main_mode(main_mode),
|
||||
|
||||
.insn_bits(ex_compressed_instr),
|
||||
|
||||
.rx_a_en_o(spec_rx_a_en),
|
||||
.rx_a_addr_o(spec_rx_a_addr),
|
||||
.rx_a_i(spec_rx_a),
|
||||
.rx_b_en_o(spec_rx_b_en),
|
||||
.rx_b_addr_o(spec_rx_b_addr),
|
||||
.rx_b_i(spec_rx_b),
|
||||
|
||||
.wx_o(spec_post_wX),
|
||||
.wx_addr_o(spec_post_wX_addr),
|
||||
.wx_en_o(spec_post_wX_en),
|
||||
|
||||
.mvendor_id_i(CSR_MVENDORID_VALUE),
|
||||
.march_id_i(CSR_MARCHID_VALUE),
|
||||
.mimp_id_i(CSR_MIMPID_VALUE),
|
||||
.mhart_id_i(hart_id_i),
|
||||
.mconfigptr_i(CSR_MCONFIGPTR_VALUE),
|
||||
|
||||
.misa_i(`CSR.MISA_VALUE),
|
||||
.mip_i(pre_mip),
|
||||
.nextpc_i(pre_nextpc),
|
||||
|
||||
`define X(n) .n``_i(pre_``n), .n``_o(spec_post_``n),
|
||||
`X_EACH_CSR
|
||||
`undef X
|
||||
|
||||
.mem_read_o(spec_mem_read),
|
||||
.mem_read_snd_gran_o(spec_mem_read_snd),
|
||||
.mem_read_fst_addr_o(spec_mem_read_fst_addr),
|
||||
.mem_read_snd_addr_o(spec_mem_read_snd_addr),
|
||||
.mem_read_fst_rdata_i(spec_mem_read_fst_rdata),
|
||||
.mem_read_snd_rdata_i(spec_mem_read_snd_rdata),
|
||||
|
||||
.mem_write_o(spec_mem_write),
|
||||
.mem_write_snd_gran_o(spec_mem_write_snd),
|
||||
.mem_write_fst_addr_o(spec_mem_write_fst_addr),
|
||||
.mem_write_snd_addr_o(spec_mem_write_snd_addr),
|
||||
.mem_write_fst_wdata_o(spec_mem_write_fst_wdata),
|
||||
.mem_write_snd_wdata_o(spec_mem_write_snd_wdata),
|
||||
.mem_write_fst_be_o(spec_mem_write_fst_be),
|
||||
.mem_write_snd_be_o(spec_mem_write_snd_be)
|
||||
);
|
||||
475
dv/formal/check/top.sv
Normal file
475
dv/formal/check/top.sv
Normal file
|
|
@ -0,0 +1,475 @@
|
|||
// Copyright lowRISC contributors.
|
||||
// Copyright 2024 University of Oxford, see also CREDITS.md.
|
||||
// Licensed under the Apache License, Version 2.0, see LICENSE for details.
|
||||
// Original author: Louis-Emile Ploix
|
||||
// SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
/*
|
||||
This is the top module. Everything else in check/* will be included into this file.
|
||||
This module contains the ibex instance, the specification instance and the assertions
|
||||
(included via the built psgen file), most of the non assertion code is setting up
|
||||
infrastructure for those assertions.
|
||||
|
||||
It has the same ports as the ibex top.
|
||||
*/
|
||||
|
||||
// Preprocessor decoding of instructions. Could be replaced with internal signals of the Sail one day
|
||||
`include "encodings.sv"
|
||||
|
||||
`define CR ibex_top_i.u_ibex_core
|
||||
`define CSR `CR.cs_registers_i
|
||||
`define CSRG `CSR.gen_scr
|
||||
`define CSRP `CSR.g_pmp_registers
|
||||
`define LSU `CR.load_store_unit_i
|
||||
`define ID `CR.id_stage_i
|
||||
`define IDG `ID.gen_stall_mem
|
||||
`define IDC `ID.controller_i
|
||||
`define WB `CR.wb_stage_i
|
||||
`define WBG `WB.g_writeback_stage
|
||||
`define RF ibex_top_i.gen_regfile_ff.register_file_i
|
||||
`define IF `CR.if_stage_i
|
||||
`define IFP `IF.gen_prefetch_buffer.prefetch_buffer_i
|
||||
`define MULT `CR.ex_block_i.gen_multdiv_fast.multdiv_i
|
||||
`define MULTG `MULT.gen_mult_fast
|
||||
|
||||
module top import ibex_pkg::*; #(
|
||||
parameter int unsigned DmHaltAddr = 32'h1A110800,
|
||||
parameter int unsigned DmExceptionAddr = 32'h1A110808,
|
||||
parameter bit SecureIbex = 1'b0,
|
||||
parameter bit WritebackStage = 1'b1,
|
||||
parameter bit RV32E = 1'b0,
|
||||
parameter int unsigned PMPNumRegions = 4
|
||||
) (
|
||||
// Clock and Reset
|
||||
input logic clk_i,
|
||||
input logic rst_ni,
|
||||
|
||||
input logic test_en_i, // enable all clock gates for testing
|
||||
input prim_ram_1p_pkg::ram_1p_cfg_t ram_cfg_i,
|
||||
|
||||
input logic [31:0] hart_id_i,
|
||||
input logic [31:0] boot_addr_i,
|
||||
|
||||
// Instruction memory interface
|
||||
output logic instr_req_o,
|
||||
input logic instr_gnt_i,
|
||||
input logic instr_rvalid_i,
|
||||
output logic [31:0] instr_addr_o,
|
||||
input logic [31:0] instr_rdata_i,
|
||||
input logic [6:0] instr_rdata_intg_i,
|
||||
input logic instr_err_i,
|
||||
|
||||
// Data memory interface
|
||||
output logic data_req_o,
|
||||
output logic data_is_cap_o,
|
||||
input logic data_gnt_i,
|
||||
input logic data_rvalid_i,
|
||||
output logic data_we_o,
|
||||
output logic [3:0] data_be_o,
|
||||
output logic [31:0] data_addr_o,
|
||||
output logic [31:0] data_wdata_o,
|
||||
output logic [6:0] data_wdata_intg_o,
|
||||
input logic [31:0] data_rdata_i,
|
||||
input logic [6:0] data_rdata_intg_i,
|
||||
input logic data_err_i,
|
||||
|
||||
// Interrupt inputs
|
||||
input logic irq_software_i,
|
||||
input logic irq_timer_i,
|
||||
input logic irq_external_i,
|
||||
input logic [14:0] irq_fast_i,
|
||||
input logic irq_nm_i, // non-maskeable interrupt
|
||||
|
||||
// Scrambling Interface
|
||||
input logic scramble_key_valid_i,
|
||||
input logic [SCRAMBLE_KEY_W-1:0] scramble_key_i,
|
||||
input logic [SCRAMBLE_NONCE_W-1:0] scramble_nonce_i,
|
||||
output logic scramble_req_o,
|
||||
|
||||
// Debug Interface
|
||||
input logic debug_req_i,
|
||||
output crash_dump_t crash_dump_o,
|
||||
output logic double_fault_seen_o,
|
||||
|
||||
// CPU Control Signals
|
||||
input ibex_mubi_t fetch_enable_i,
|
||||
output logic core_sleep_o,
|
||||
output logic alert_minor_o,
|
||||
output logic alert_major_internal_o,
|
||||
output logic alert_major_bus_o,
|
||||
|
||||
|
||||
// DFT bypass controls
|
||||
input logic scan_rst_ni
|
||||
);
|
||||
|
||||
default clocking @(posedge clk_i); endclocking
|
||||
|
||||
ibex_top #(
|
||||
.DmHaltAddr(DmHaltAddr),
|
||||
.DmExceptionAddr(DmExceptionAddr),
|
||||
.SecureIbex(SecureIbex),
|
||||
.WritebackStage(WritebackStage),
|
||||
.RV32E(RV32E),
|
||||
.BranchTargetALU(1'b1),
|
||||
.PMPEnable(1'b1),
|
||||
.PMPNumRegions(PMPNumRegions)
|
||||
) ibex_top_i(.*);
|
||||
|
||||
// Core constraints
|
||||
// 1. We do not allow going into debug mode
|
||||
NotDebug: assume property (!ibex_top_i.u_ibex_core.debug_mode & !debug_req_i);
|
||||
// 2. The boot address is constant
|
||||
ConstantBoot: assume property (boot_addr_i == $past(boot_addr_i));
|
||||
// 3. Always fetch enable
|
||||
FetchEnable: assume property (fetch_enable_i == IbexMuBiOn);
|
||||
// 4. Never try to sleep if we couldn't ever wake up
|
||||
WFIStart: assume property (`IDC.ctrl_fsm_cs == SLEEP |-> `CSR.mie_q.irq_software | `CSR.mie_q.irq_timer | `CSR.mie_q.irq_external);
|
||||
// 5. Disable clock gating
|
||||
TestEn: assume property (test_en_i);
|
||||
// See protocol/* for further assumptions
|
||||
|
||||
///////////////////////////////// Declarations /////////////////////////////////
|
||||
|
||||
// Helpful macros to define each relevant, checked CSR and their types.
|
||||
// Some CSRs are not checked or tracked, see ex_is_checkable_csr below.
|
||||
`define X_EACH_CSR \
|
||||
`ifndef X_DISABLE_PC `X(pc) `endif \
|
||||
`X(priv) \
|
||||
`X(mstatus) \
|
||||
`X(mie) \
|
||||
`X(mcause) \
|
||||
`X(mtval) \
|
||||
`X(mtvec) \
|
||||
`X(mscratch) \
|
||||
`X(mepc) \
|
||||
`X(mcounteren) \
|
||||
`X(pmp_cfg) \
|
||||
`X(pmp_addr) \
|
||||
`X(mseccfg)
|
||||
|
||||
`define X_EACH_CSR_TYPED \
|
||||
logic [31:0] `X(pc); \
|
||||
t_Privilege `X(priv); \
|
||||
mstatus_t `X(mstatus); \
|
||||
logic [31:0] `X(mie); \
|
||||
logic [31:0] `X(mcause); \
|
||||
logic [31:0] `X(mtval); \
|
||||
logic [31:0] `X(mtvec); \
|
||||
logic [31:0] `X(mscratch); \
|
||||
logic [31:0] `X(mepc); \
|
||||
logic [63:0] `X(mcycle); \
|
||||
logic [31:0] `X(mshwmb); \
|
||||
logic [31:0] `X(mshwm); \
|
||||
logic [31:0] `X(mcounteren); \
|
||||
logic [7:0] `X(pmp_cfg)[PMPNumRegions]; \
|
||||
logic [31:0] `X(pmp_addr)[PMPNumRegions]; \
|
||||
logic [31:0] `X(mseccfg);
|
||||
|
||||
////////////////////// Abstract State //////////////////////
|
||||
|
||||
// Pre state is the architectural state of Ibex at the start of the cycle
|
||||
logic [31:0] pre_regs[31:0];
|
||||
logic [31:0] pre_nextpc;
|
||||
logic [31:0] pre_mip;
|
||||
|
||||
`define X(n) pre_``n
|
||||
`X_EACH_CSR_TYPED
|
||||
`undef X
|
||||
|
||||
// Post state is the architectural state of Ibex at the end of this cycle, or the start of the next
|
||||
`define X(n) post_``n
|
||||
`X_EACH_CSR_TYPED
|
||||
`undef X
|
||||
|
||||
////////////////////// Following //////////////////////
|
||||
// Generally:
|
||||
// - ex_P is 1 if P is true for the instruction in the ID/EX stage.
|
||||
// - wbexc_P is 1 if P is true for the instruction in the WB/EXC (exception) stage.
|
||||
|
||||
logic ex_is_wfi, ex_is_rtype, ex_is_div;
|
||||
logic ex_is_pres_btype, ex_is_pres_jump;
|
||||
logic ex_is_mem_instr, ex_is_load_instr, ex_is_store_instr;
|
||||
logic ex_is_pres_mem_instr, ex_is_pres_load_instr, ex_is_pres_store_instr;
|
||||
|
||||
// Have we branched, or are we branching in this cycle?
|
||||
logic ex_has_branched_d, ex_has_branched_q;
|
||||
logic [31:0] ex_branch_dst;
|
||||
assign ex_branch_dst = `CR.branch_decision ? `CR.branch_target_ex : pre_nextpc;
|
||||
|
||||
logic outstanding_mem;
|
||||
assign outstanding_mem = `ID.outstanding_load_wb_i || `ID.outstanding_store_wb_i;
|
||||
|
||||
logic has_resp_waiting_q, has_resp_waiting_d;
|
||||
assign has_resp_waiting_q = data_mem_assume.outstanding_reqs_q != 8'h0;
|
||||
assign has_resp_waiting_d = data_mem_assume.outstanding_reqs != 8'h0;
|
||||
|
||||
logic has_one_resp_waiting_q, has_one_resp_waiting_d;
|
||||
assign has_one_resp_waiting_q = data_mem_assume.outstanding_reqs_q == 8'h1;
|
||||
assign has_one_resp_waiting_d = data_mem_assume.outstanding_reqs == 8'h1;
|
||||
|
||||
logic has_two_resp_waiting_q, has_two_resp_waiting_d;
|
||||
assign has_two_resp_waiting_q = data_mem_assume.outstanding_reqs_q == 8'h2;
|
||||
assign has_two_resp_waiting_d = data_mem_assume.outstanding_reqs == 8'h2;
|
||||
|
||||
logic wbexc_is_pres_load_instr, wbexc_is_pres_store_instr;
|
||||
logic wbexc_is_load_instr, wbexc_is_store_instr;
|
||||
logic wbexc_is_pres_mem_instr, wbexc_is_mem_instr;
|
||||
logic wbexc_is_wfi;
|
||||
|
||||
logic [31:0] ex_compressed_instr;
|
||||
logic ex_has_compressed_instr;
|
||||
|
||||
// Stored specification post state
|
||||
logic wbexc_post_int_err; // Spec had an internal error
|
||||
|
||||
logic [31:0] wbexc_post_wX;
|
||||
logic [5:0] wbexc_post_wX_addr;
|
||||
logic wbexc_post_wX_en;
|
||||
|
||||
`define X(n) wbexc_post_``n
|
||||
`X_EACH_CSR_TYPED
|
||||
`undef X
|
||||
|
||||
// Stored predetermined memory responses, see check/peek/mem.sv
|
||||
logic [31:0] wbexc_spec_mem_read_fst_rdata;
|
||||
logic [31:0] wbexc_spec_mem_read_snd_rdata;
|
||||
|
||||
// Store DUT CSR post state
|
||||
`define X(n) wbexc_dut_post_``n
|
||||
`X_EACH_CSR_TYPED
|
||||
`undef X
|
||||
|
||||
logic [31:0] wbexc_instr; // original potentially compressed
|
||||
logic [31:0] wbexc_decompressed_instr; // post decompression
|
||||
logic wbexc_is_compressed;
|
||||
|
||||
logic [31:0] wbexc_pc;
|
||||
|
||||
logic mem_gnt_fst_d; // We are having or have had the first gnt
|
||||
logic mem_gnt_fst_q; // We have had the first gnt before now
|
||||
logic mem_gnt_snd_d; // We are having or have had the second gnt
|
||||
logic mem_gnt_snd_q; // We have had the second gnt before now
|
||||
|
||||
logic mem_req_fst_d; // We are having the first req
|
||||
logic mem_req_snd_d; // We are having the second req
|
||||
|
||||
logic wbexc_mem_had_snd_req; // During ID/EX there was a second request
|
||||
|
||||
logic lsu_had_first_resp;
|
||||
assign lsu_had_first_resp = `LSU.ls_fsm_cs == `LSU.WAIT_GNT && `LSU.split_misaligned_access;
|
||||
|
||||
////////////////////// Wrap signals //////////////////////
|
||||
|
||||
logic spec_en; // The specification is being queried in this cycle
|
||||
logic has_spec_past; // There is a previous step to compare against. Will become 0 on uncheckable CSRs and at reset.
|
||||
|
||||
// The previous specification output to be compared with the new input
|
||||
logic [31:0] spec_past_regs[31:0];
|
||||
logic [31:0] spec_past_has_reg; // Registers will have past values only when they are written to.
|
||||
`define X(n) spec_past_``n
|
||||
`X_EACH_CSR_TYPED
|
||||
`undef X
|
||||
|
||||
////////////////////// Pipeline signals //////////////////////
|
||||
|
||||
logic ex_success; // Execute stage succeeding
|
||||
logic ex_err; // Execute stage erroring
|
||||
logic ex_kill; // Execute stage killed
|
||||
logic exc_finishing; // Exception finishing
|
||||
logic wb_finishing; // WB finishing
|
||||
logic wbexc_finishing; // WB/EXC finishing
|
||||
logic wbexc_exists; // Instruction in WB/EXC
|
||||
logic wbexc_ex_err; // EXC has an execute error
|
||||
logic wbexc_fetch_err; // EXC has a fetch error
|
||||
logic wbexc_illegal; // EXC has an illegal instruction
|
||||
logic wbexc_compressed_illegal; // EXC has an illegal instruction
|
||||
logic wbexc_err; // EXC has an error
|
||||
logic instr_will_progress; // Instruction will finish EX
|
||||
logic wfi_will_finish; // WFI instruction retire by flushing the pipeline, but that isn't an exception
|
||||
logic wbexc_csr_pipe_flush; // The pipeline is being flushed due to a CSR write
|
||||
logic wbexc_handling_irq; // Check the results of handling an IRQ
|
||||
|
||||
////////////////////// CSR selection //////////////////////
|
||||
// Decide whether to compare wbexc_post_* and wbexc_dut_post_* or to use live versions.
|
||||
|
||||
// WBEXC CSR dut post state
|
||||
`define X(n) wbexc_dut_cmp_post_``n
|
||||
`X_EACH_CSR_TYPED
|
||||
`undef X
|
||||
|
||||
// WBEXC CSR spec post state
|
||||
`define X(n) wbexc_spec_cmp_post_``n
|
||||
`X_EACH_CSR_TYPED
|
||||
`undef X
|
||||
|
||||
////////////////////// Spec Post //////////////////////
|
||||
|
||||
// These cause combinational cycles, but not severe ones. The problem is fixed in CherIoT-Ibex
|
||||
logic spec_rx_a_en;
|
||||
logic [4:0] spec_rx_a_addr;
|
||||
logic [31:0] spec_rx_a;
|
||||
assign spec_rx_a = pre_regs[spec_rx_a_addr];
|
||||
|
||||
logic spec_rx_b_en;
|
||||
logic [4:0] spec_rx_b_addr;
|
||||
logic [31:0] spec_rx_b;
|
||||
assign spec_rx_b = pre_regs[spec_rx_b_addr];
|
||||
|
||||
logic [31:0] spec_post_wX;
|
||||
logic [4:0] spec_post_wX_addr;
|
||||
logic spec_post_wX_en;
|
||||
|
||||
`define X(n) spec_post_``n
|
||||
`X_EACH_CSR_TYPED
|
||||
`undef X
|
||||
|
||||
logic spec_int_err;
|
||||
|
||||
logic spec_fetch_err; // The specification has experienced a fetch error, regardless of whether or not it was told to.
|
||||
assign spec_fetch_err =
|
||||
(main_mode == MAIN_IFERR && spec_api_i.main_result == MAINRES_OK) ||
|
||||
spec_api_i.main_result == MAINRES_IFERR_1 || spec_api_i.main_result == MAINRES_IFERR_2;
|
||||
|
||||
logic spec_mem_read;
|
||||
logic spec_mem_read_snd;
|
||||
logic [31:0] spec_mem_read_fst_addr;
|
||||
logic [31:0] spec_mem_read_snd_addr;
|
||||
logic [31:0] spec_mem_read_fst_rdata; // Undriven
|
||||
logic [31:0] spec_mem_read_snd_rdata; // Undriven
|
||||
|
||||
logic spec_mem_write;
|
||||
logic spec_mem_write_snd;
|
||||
logic [31:0] spec_mem_write_fst_addr;
|
||||
logic [31:0] spec_mem_write_snd_addr;
|
||||
logic [31:0] spec_mem_write_fst_wdata;
|
||||
logic [31:0] spec_mem_write_snd_wdata;
|
||||
logic [3:0] spec_mem_write_fst_be;
|
||||
logic [3:0] spec_mem_write_snd_be;
|
||||
|
||||
logic spec_mem_en;
|
||||
logic spec_mem_en_snd;
|
||||
logic [31:0] spec_mem_fst_addr;
|
||||
logic [31:0] spec_mem_snd_addr;
|
||||
logic spec_has_pmp_err;
|
||||
|
||||
assign spec_mem_en = spec_mem_read | spec_mem_write;
|
||||
assign spec_mem_en_snd = spec_mem_read_snd | spec_mem_write_snd;
|
||||
assign spec_mem_fst_addr = spec_mem_read ? spec_mem_read_fst_addr : spec_mem_write_fst_addr;
|
||||
assign spec_mem_snd_addr = spec_mem_read ? spec_mem_read_snd_addr : spec_mem_write_snd_addr;
|
||||
assign spec_has_pmp_err = ~spec_mem_en || (`LSU.split_misaligned_access && ~spec_mem_en_snd);
|
||||
|
||||
logic [31:0] fst_mask, snd_mask;
|
||||
assign fst_mask = {
|
||||
{8{spec_mem_write_fst_be[3]}}, {8{spec_mem_write_fst_be[2]}},
|
||||
{8{spec_mem_write_fst_be[1]}}, {8{spec_mem_write_fst_be[0]}}
|
||||
};
|
||||
assign snd_mask = {
|
||||
{8{spec_mem_write_snd_be[3]}}, {8{spec_mem_write_snd_be[2]}},
|
||||
{8{spec_mem_write_snd_be[1]}}, {8{spec_mem_write_snd_be[0]}}
|
||||
};
|
||||
|
||||
logic fst_mem_cmp; // Condition for the first outgoing request to be spec conformant
|
||||
assign fst_mem_cmp = (spec_mem_write == data_we_o) && (spec_mem_read == ~data_we_o) &&
|
||||
(data_addr_o == spec_mem_fst_addr) &&
|
||||
(data_we_o ->
|
||||
(data_wdata_o & fst_mask) == (spec_mem_write_fst_wdata & fst_mask));
|
||||
logic snd_mem_cmp; // Condition for the second outgoing request to be spec conformant
|
||||
assign snd_mem_cmp = (spec_mem_write_snd == data_we_o) && (spec_mem_read_snd == ~data_we_o) &&
|
||||
(data_addr_o == spec_mem_snd_addr) &&
|
||||
(data_we_o ->
|
||||
(data_wdata_o & snd_mask) == (spec_mem_write_snd_wdata & snd_mask));
|
||||
|
||||
logic lsu_waiting_for_misal;
|
||||
assign lsu_waiting_for_misal =
|
||||
((`LSU.data_type_q == 2'b00) && (`LSU.rdata_offset_q != 2'b00)) ||
|
||||
((`LSU.data_type_q == 2'b01) && (`LSU.rdata_offset_q == 2'b11));
|
||||
|
||||
logic addr_last_matches;
|
||||
assign addr_last_matches = `ID.rf_rdata_a_fwd + (ex_is_store_instr? `ID.imm_s_type : `ID.imm_i_type) == `LSU.addr_last_q;
|
||||
|
||||
logic addr_last_d_matches;
|
||||
assign addr_last_d_matches = `ID.rf_rdata_a_fwd + (ex_is_store_instr? `ID.imm_s_type : `ID.imm_i_type) == `LSU.addr_last_d;
|
||||
|
||||
////////////////////// Compare //////////////////////
|
||||
|
||||
logic addr_match; // Register write index match
|
||||
logic data_match; // Register write data match
|
||||
logic csrs_match;
|
||||
logic ex_csrs_match;
|
||||
logic csrs_match_non_exc;
|
||||
logic ex_csrs_match_non_exc;
|
||||
logic pc_match;
|
||||
logic finishing_executed; // Finishing normal case
|
||||
|
||||
`define INSTR `CR.instr_rdata_id
|
||||
|
||||
logic wbexc_is_checkable_csr;
|
||||
logic ex_is_checkable_csr;
|
||||
assign ex_is_checkable_csr = ~(
|
||||
((CSR_MHPMCOUNTER3H <= `CSR_ADDR) && (`CSR_ADDR <= CSR_MHPMCOUNTER31H)) |
|
||||
((CSR_MHPMCOUNTER3 <= `CSR_ADDR) && (`CSR_ADDR <= CSR_MHPMCOUNTER31)) |
|
||||
((CSR_MHPMEVENT3 <= `CSR_ADDR) && (`CSR_ADDR <= CSR_MHPMEVENT31)) |
|
||||
(`CSR_ADDR == CSR_CPUCTRLSTS) | (`CSR_ADDR == CSR_SECURESEED) |
|
||||
(`CSR_ADDR == CSR_MIE) |
|
||||
(`CSR_ADDR == CSR_MCYCLE) | (`CSR_ADDR == CSR_MCYCLEH) |
|
||||
|
||||
// TODO:
|
||||
(`CSR_ADDR == CSR_MINSTRET) | (`CSR_ADDR == CSR_MINSTRETH) |
|
||||
(`CSR_ADDR == CSR_MCOUNTINHIBIT)
|
||||
);
|
||||
|
||||
`undef INSTR
|
||||
`define INSTR wbexc_decompressed_instr
|
||||
|
||||
// Illegal instructions arent checkable unless the relevant specifications are present.
|
||||
logic can_check_illegal;
|
||||
assign can_check_illegal = `SPEC_ILLEGAL & `SPEC_CSR & `SPEC_MRET & `SPEC_WFI;
|
||||
|
||||
`undef INSTR
|
||||
|
||||
////////////////////// Decompression Invariant Defs //////////////////////
|
||||
// These will be used to show that the decompressed instruction stored is in fact the decompressed version of the compressed instruction.
|
||||
|
||||
logic [31:0] decompressed_instr;
|
||||
logic decompressed_instr_illegal;
|
||||
ibex_compressed_decoder decompression_assertion_decoder(
|
||||
.clk_i,
|
||||
.rst_ni,
|
||||
.valid_i(1'b1),
|
||||
.instr_i(ex_compressed_instr),
|
||||
.instr_o(decompressed_instr),
|
||||
.is_compressed_o(),
|
||||
.illegal_instr_o(decompressed_instr_illegal)
|
||||
);
|
||||
|
||||
logic [31:0] decompressed_instr_2;
|
||||
logic decompressed_instr_illegal_2;
|
||||
ibex_compressed_decoder decompression_assertion_decoder_2(
|
||||
.clk_i,
|
||||
.rst_ni,
|
||||
.valid_i(1'b1),
|
||||
.instr_i(wbexc_instr),
|
||||
.instr_o(decompressed_instr_2),
|
||||
.is_compressed_o(wbexc_is_compressed),
|
||||
.illegal_instr_o(decompressed_instr_illegal_2)
|
||||
);
|
||||
|
||||
////////////////////// IRQ + Memory Protocols //////////////////////
|
||||
`include "protocol/irqs.sv"
|
||||
`include "protocol/mem.sv"
|
||||
|
||||
////////////////////// Following //////////////////////
|
||||
`include "peek/abs.sv" // Abstract state
|
||||
`include "peek/mem.sv" // Memory tracking
|
||||
`include "peek/follower.sv" // Pipeline follower
|
||||
`include "spec_instance.sv" // Instantiate the specification
|
||||
|
||||
////////////////////// Proof helpers ///////////////////////
|
||||
`include "peek/compare_helper.sv"
|
||||
|
||||
////////////////////// Proof //////////////////////
|
||||
`define INSTR wbexc_decompressed_instr
|
||||
`include "../build/psgen.sv"
|
||||
|
||||
endmodule
|
||||
58
dv/formal/instrs.json
Normal file
58
dv/formal/instrs.json
Normal file
|
|
@ -0,0 +1,58 @@
|
|||
[
|
||||
"UTYPE",
|
||||
"ITYPE",
|
||||
"RTYPE",
|
||||
"FENCE",
|
||||
"FENCEI",
|
||||
"LOAD",
|
||||
"STORE",
|
||||
"SHIFTIOP",
|
||||
"ILLEGAL",
|
||||
"BTYPE",
|
||||
"CSR",
|
||||
"DIV",
|
||||
"EBREAK",
|
||||
"ECALL",
|
||||
"MRET",
|
||||
"MUL",
|
||||
"REM",
|
||||
"RISCV_JAL",
|
||||
"RISCV_JALR",
|
||||
"WFI",
|
||||
|
||||
"C_ADD",
|
||||
"C_ADDI",
|
||||
"C_ADDI16SP",
|
||||
"C_ADDI4SPN",
|
||||
"C_ADDIW",
|
||||
"C_ADDW",
|
||||
"C_AND",
|
||||
"C_ANDI",
|
||||
"C_BEQZ",
|
||||
"C_BNEZ",
|
||||
"C_EBREAK",
|
||||
"C_ILLEGAL",
|
||||
"C_J",
|
||||
"C_JAL",
|
||||
"C_JALR",
|
||||
"C_JR",
|
||||
"C_LD",
|
||||
"C_LDSP",
|
||||
"C_LI",
|
||||
"C_LUI",
|
||||
"C_LW",
|
||||
"C_LWSP",
|
||||
"C_MV",
|
||||
"C_NOP",
|
||||
"C_OR",
|
||||
"C_SD",
|
||||
"C_SDSP",
|
||||
"C_SLLI",
|
||||
"C_SRAI",
|
||||
"C_SRLI",
|
||||
"C_SUB",
|
||||
"C_SUBW",
|
||||
"C_SW",
|
||||
"C_SWSP",
|
||||
"C_XOR"
|
||||
]
|
||||
46
dv/formal/rtl-changes.patch
Normal file
46
dv/formal/rtl-changes.patch
Normal file
|
|
@ -0,0 +1,46 @@
|
|||
diff --git a/rtl/ibex_id_stage.sv b/rtl/ibex_id_stage.sv
|
||||
index 3a358af7..3c19d763 100644
|
||||
--- a/rtl/ibex_id_stage.sv
|
||||
+++ b/rtl/ibex_id_stage.sv
|
||||
@@ -522,7 +522,7 @@ module ibex_id_stage #(
|
||||
// - When modifying any PMP CSR, PMP check of the next instruction might get invalidated.
|
||||
// Hence, a pipeline flush is needed to instantiate another PMP check with the updated CSRs.
|
||||
// - When modifying debug CSRs.
|
||||
- if (csr_op_en_o == 1'b1 && (csr_op_o == CSR_OP_WRITE || csr_op_o == CSR_OP_SET)) begin
|
||||
+ if (csr_op_en_o == 1'b1 && (csr_op_o == CSR_OP_WRITE || csr_op_o == CSR_OP_SET || csr_op_o == CSR_OP_CLEAR)) begin
|
||||
if (csr_num_e'(instr_rdata_i[31:20]) == CSR_MSTATUS ||
|
||||
csr_num_e'(instr_rdata_i[31:20]) == CSR_MIE ||
|
||||
csr_num_e'(instr_rdata_i[31:20]) == CSR_MSECCFG ||
|
||||
diff --git a/rtl/ibex_top.sv b/rtl/ibex_top.sv
|
||||
index 81e49633..17b36c17 100644
|
||||
--- a/rtl/ibex_top.sv
|
||||
+++ b/rtl/ibex_top.sv
|
||||
@@ -142,7 +142,7 @@ module ibex_top import ibex_pkg::*; #(
|
||||
);
|
||||
|
||||
localparam bit Lockstep = SecureIbex;
|
||||
- localparam bit ResetAll = Lockstep;
|
||||
+ localparam bit ResetAll = 1;
|
||||
localparam bit DummyInstructions = SecureIbex;
|
||||
localparam bit RegFileECC = SecureIbex;
|
||||
localparam bit RegFileWrenCheck = SecureIbex;
|
||||
@@ -236,12 +236,13 @@ module ibex_top import ibex_pkg::*; #(
|
||||
|
||||
assign core_sleep_o = ~clock_en;
|
||||
|
||||
- prim_clock_gating core_clock_gate_i (
|
||||
- .clk_i (clk_i),
|
||||
- .en_i (clock_en),
|
||||
- .test_en_i(test_en_i),
|
||||
- .clk_o (clk)
|
||||
- );
|
||||
+ assign clk = clk_i;
|
||||
+ // prim_clock_gating core_clock_gate_i (
|
||||
+ // .clk_i (clk_i),
|
||||
+ // .en_i (clock_en),
|
||||
+ // .test_en_i(test_en_i),
|
||||
+ // .clk_o (clk)
|
||||
+ // );
|
||||
|
||||
////////////////////////
|
||||
// Core instantiation //
|
||||
28
dv/formal/spec/fix_pmp_bug.py
Normal file
28
dv/formal/spec/fix_pmp_bug.py
Normal file
|
|
@ -0,0 +1,28 @@
|
|||
'''
|
||||
Fixes an issue where the Sail -> SV compiler references t_Pmpcfg_ent (in sail_genlib_ibexspec.sv) before it defines it (in ibexspec.sv)
|
||||
by just moving that definition.
|
||||
'''
|
||||
|
||||
S = """
|
||||
typedef struct {
|
||||
logic [7:0] bits;
|
||||
} t_Pmpcfg_ent;
|
||||
"""
|
||||
|
||||
T = """
|
||||
typedef logic [127:0] sail_int;
|
||||
"""
|
||||
|
||||
with open("build/ibexspec.sv", "r") as f:
|
||||
c = f.read()
|
||||
|
||||
c = c.replace(S, "")
|
||||
|
||||
with open("build/ibexspec.sv", "w") as f:
|
||||
f.write(c)
|
||||
|
||||
with open("build/sail_genlib_ibexspec.sv", "r") as f:
|
||||
c = f.read()
|
||||
|
||||
with open("build/sail_genlib_ibexspec.sv", "w") as f:
|
||||
f.write(S + "\n" + c)
|
||||
94
dv/formal/spec/main.sail
Normal file
94
dv/formal/spec/main.sail
Normal file
|
|
@ -0,0 +1,94 @@
|
|||
// Copyright lowRISC contributors.
|
||||
// Copyright 2024 University of Oxford, see also CREDITS.md.
|
||||
// Licensed under the Apache License, Version 2.0, see LICENSE for details.
|
||||
// Original author: Louis-Emile Ploix
|
||||
// SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
/*
|
||||
This file contains the main function which is 'invoked' by the SystemVerilog.
|
||||
main is equivalent to the Sail step function, it has some differences however:
|
||||
1. It uses the decompress function we added.
|
||||
2. It can operate in one of three modes, based on what it has been told to do by the SV.
|
||||
This is done for a couple of reasons:
|
||||
1. It's difficult to compare IRQ handling, since ibex takes them later than the Sail would. This is OK since it's not really
|
||||
fair to enforce that IRQs are handled between any two specific instructions, so long as it is eventually.
|
||||
2. The three modes are a useful case analysis we can make. This means that to prove correctness of an I-Type instruction, for example, we
|
||||
can more easily seperate out the check for instruction fetch correctness, which makes things faster and avoids repeated work.
|
||||
*/
|
||||
|
||||
union FetchResult = {
|
||||
F_Ext_Error : ext_fetch_addr_error, /* For extensions */
|
||||
F_Base : word, /* Base ISA */
|
||||
F_RVC : half, /* Compressed ISA */
|
||||
F_Error : (ExceptionType, xlenbits) /* standard exception and PC */
|
||||
}
|
||||
|
||||
function isRVC(h : bits(16)) -> bool = ~ (h[1 .. 0] == 0b11)
|
||||
|
||||
// modified version of what one can find in riscv_fetch.sail
|
||||
val altFetch : (bits(16), bits(16)) -> FetchResult
|
||||
function altFetch(ilo: bits(16), ihi: bits(16)) -> FetchResult =
|
||||
match mem_read_i(Execute(), PC, if isRVC(ilo) then 2 else 4) {
|
||||
MemException(a, e) => F_Error(e, a),
|
||||
MemValue(()) => if isRVC(ilo) then F_RVC(ilo) else F_Base(ihi @ ilo)
|
||||
}
|
||||
|
||||
|
||||
enum MainMode = { MAIN_IDEX, MAIN_IFERR, MAIN_IRQ }
|
||||
enum MainResult = { MAINRES_OK, MAINRES_IFERR_1, MAINRES_IFERR_2, MAINRES_NOIFERR, MAINRES_IRQ, MAINRES_NOIRQ }
|
||||
|
||||
function main(insn_bits, mode) : (bits(32), MainMode) -> MainResult = {
|
||||
let insn = if isRVC(insn_bits[15..0]) then {
|
||||
instbits = 0x0000 @ insn_bits[15..0];
|
||||
encdec_compressed(insn_bits[15..0])
|
||||
} else {
|
||||
instbits = insn_bits;
|
||||
encdec(insn_bits)
|
||||
};
|
||||
|
||||
let irq = dispatchInterrupt(cur_privilege);
|
||||
let f : FetchResult = altFetch(insn_bits[15..0], insn_bits[31..16]);
|
||||
|
||||
let res : MainResult = match mode {
|
||||
MAIN_IDEX => {
|
||||
match decompress(insn) {
|
||||
Some(decompressed) => {
|
||||
let _ = execute(decompressed);
|
||||
},
|
||||
None() => ()
|
||||
};
|
||||
|
||||
match f {
|
||||
F_Ext_Error(e) => MAINRES_IFERR_1,
|
||||
F_Error(e, addr) => MAINRES_IFERR_2,
|
||||
F_RVC(h) => MAINRES_OK,
|
||||
F_Base(w) => MAINRES_OK
|
||||
}
|
||||
},
|
||||
MAIN_IFERR => {
|
||||
match f {
|
||||
F_Ext_Error(e) => {
|
||||
ext_handle_fetch_check_error(e);
|
||||
MAINRES_OK
|
||||
},
|
||||
F_Error(e, addr) => {
|
||||
handle_mem_exception(addr, e);
|
||||
MAINRES_OK
|
||||
},
|
||||
F_RVC(h) => MAINRES_NOIFERR,
|
||||
F_Base(w) => MAINRES_NOIFERR
|
||||
}
|
||||
},
|
||||
MAIN_IRQ => {
|
||||
match irq {
|
||||
Some(intr, priv) => {
|
||||
handle_interrupt(intr, priv);
|
||||
MAINRES_OK
|
||||
},
|
||||
None() => MAINRES_NOIRQ
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
res
|
||||
}
|
||||
368
dv/formal/spec/spec_api.sv
Normal file
368
dv/formal/spec/spec_api.sv
Normal file
|
|
@ -0,0 +1,368 @@
|
|||
// Copyright lowRISC contributors.
|
||||
// Copyright 2024 University of Oxford, see also CREDITS.md.
|
||||
// Licensed under the Apache License, Version 2.0, see LICENSE for details.
|
||||
// Original author: Louis-Emile Ploix
|
||||
// SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
/*
|
||||
This module contains the actual instance of the specification. It's quite ugly. Mostly it's just forwaring things to
|
||||
different names and ignoring registers we don't care about.
|
||||
*/
|
||||
|
||||
typedef struct packed {
|
||||
logic mie;
|
||||
logic mpie;
|
||||
logic tw;
|
||||
logic mprv;
|
||||
logic [1:0] mpp;
|
||||
} mstatus_t;
|
||||
|
||||
module spec_api #(
|
||||
parameter int unsigned NREGS = 32,
|
||||
parameter int unsigned PMPNumRegions = 4
|
||||
) (
|
||||
input t_MainMode main_mode,
|
||||
|
||||
output logic rx_a_en_o,
|
||||
output logic [4:0] rx_a_addr_o,
|
||||
input logic [31:0] rx_a_i,
|
||||
output logic rx_b_en_o,
|
||||
output logic [4:0] rx_b_addr_o,
|
||||
input logic [31:0] rx_b_i,
|
||||
|
||||
output logic wx_en_o,
|
||||
output logic [31:0] wx_o,
|
||||
output logic [4:0] wx_addr_o,
|
||||
|
||||
input logic [31:0] nextpc_i,
|
||||
input logic [31:0] pc_i,
|
||||
output logic [31:0] pc_o,
|
||||
|
||||
input logic [31:0] misa_i,
|
||||
input logic [31:0] mip_i,
|
||||
|
||||
input logic [31:0] mvendor_id_i,
|
||||
input logic [31:0] march_id_i,
|
||||
input logic [31:0] mimp_id_i,
|
||||
input logic [31:0] mhart_id_i,
|
||||
input logic [31:0] mconfigptr_i,
|
||||
|
||||
input logic [31:0] mseccfg_i,
|
||||
output logic [31:0] mseccfg_o,
|
||||
input logic [7:0] pmp_cfg_i[PMPNumRegions],
|
||||
output logic [7:0] pmp_cfg_o[PMPNumRegions],
|
||||
input logic [31:0] pmp_addr_i[PMPNumRegions],
|
||||
output logic [31:0] pmp_addr_o[PMPNumRegions],
|
||||
|
||||
input logic [31:0] mie_i,
|
||||
output logic [31:0] mie_o,
|
||||
input t_Privilege priv_i,
|
||||
output t_Privilege priv_o,
|
||||
input mstatus_t mstatus_i,
|
||||
output mstatus_t mstatus_o,
|
||||
input logic [31:0] mcause_i,
|
||||
output logic [31:0] mcause_o,
|
||||
input logic [63:0] mcycle_i,
|
||||
output logic [63:0] mcycle_o,
|
||||
input logic [31:0] mtval_i,
|
||||
output logic [31:0] mtval_o,
|
||||
input logic [31:0] mtvec_i,
|
||||
output logic [31:0] mtvec_o,
|
||||
input logic [31:0] mscratch_i,
|
||||
output logic [31:0] mscratch_o,
|
||||
input logic [31:0] mepc_i,
|
||||
output logic [31:0] mepc_o,
|
||||
input logic [31:0] mshwmb_i,
|
||||
output logic [31:0] mshwmb_o,
|
||||
input logic [31:0] mshwm_i,
|
||||
output logic [31:0] mshwm_o,
|
||||
input logic [31:0] mcounteren_i,
|
||||
output logic [31:0] mcounteren_o,
|
||||
|
||||
input logic [31:0] insn_bits,
|
||||
output logic int_err_o,
|
||||
|
||||
output logic mem_read_o,
|
||||
output logic mem_read_snd_gran_o,
|
||||
output logic[31:0] mem_read_fst_addr_o,
|
||||
output logic[31:0] mem_read_snd_addr_o,
|
||||
input logic[31:0] mem_read_fst_rdata_i,
|
||||
input logic[31:0] mem_read_snd_rdata_i,
|
||||
|
||||
output logic mem_write_o,
|
||||
output logic mem_write_snd_gran_o,
|
||||
output logic[31:0] mem_write_fst_addr_o,
|
||||
output logic[31:0] mem_write_snd_addr_o,
|
||||
output logic[31:0] mem_write_fst_wdata_o,
|
||||
output logic[31:0] mem_write_snd_wdata_o,
|
||||
output logic [3:0] mem_write_fst_be_o,
|
||||
output logic [3:0] mem_write_snd_be_o
|
||||
);
|
||||
|
||||
bit rX_sail_invoke[1:0];
|
||||
logic [31:0] rX_sail_invoke_ret[1:0];
|
||||
logic [63:0] rX_sail_invoke_arg_0[1:0];
|
||||
assign rx_a_en_o = rX_sail_invoke[0];
|
||||
assign rx_a_addr_o = rX_sail_invoke_arg_0[0][4:0];
|
||||
assign rX_sail_invoke_ret[0] = rx_a_i;
|
||||
assign rx_b_en_o = rX_sail_invoke[1];
|
||||
assign rx_b_addr_o = rX_sail_invoke_arg_0[1][4:0];
|
||||
assign rX_sail_invoke_ret[1] = rx_b_i;
|
||||
|
||||
logic wX_sail_invoke[0:0];
|
||||
logic [63:0] wX_sail_invoke_arg_0[0:0];
|
||||
logic [31:0] wX_sail_invoke_arg_1[0:0];
|
||||
assign wx_en_o = wX_sail_invoke[0];
|
||||
assign wx_addr_o = wX_sail_invoke_arg_0[0][4:0];
|
||||
assign wx_o = wX_sail_invoke_arg_1[0];
|
||||
|
||||
logic write_ram_sail_invoke[1:0];
|
||||
logic [31:0] write_ram_sail_invoke_arg_1[1:0];
|
||||
logic [31:0] write_ram_sail_invoke_arg_2[1:0];
|
||||
logic [3:0] write_ram_sail_invoke_arg_3[1:0];
|
||||
assign mem_write_o = write_ram_sail_invoke[0];
|
||||
assign mem_write_snd_gran_o = write_ram_sail_invoke[1];
|
||||
assign mem_write_fst_addr_o = write_ram_sail_invoke_arg_1[0];
|
||||
assign mem_write_snd_addr_o = write_ram_sail_invoke_arg_1[1];
|
||||
assign mem_write_fst_wdata_o = write_ram_sail_invoke_arg_2[0];
|
||||
assign mem_write_snd_wdata_o = write_ram_sail_invoke_arg_2[1];
|
||||
assign mem_write_fst_be_o = write_ram_sail_invoke_arg_3[0];
|
||||
assign mem_write_snd_be_o = write_ram_sail_invoke_arg_3[1];
|
||||
|
||||
logic read_ram_sail_invoke[1:0];
|
||||
logic [31:0] read_ram_sail_invoke_ret[1:0];
|
||||
logic [31:0] read_ram_sail_invoke_arg_1[1:0];
|
||||
assign mem_read_o = read_ram_sail_invoke[0];
|
||||
assign mem_read_snd_gran_o = read_ram_sail_invoke[1];
|
||||
assign mem_read_fst_addr_o = read_ram_sail_invoke_arg_1[0];
|
||||
assign mem_read_snd_addr_o = read_ram_sail_invoke_arg_1[1];
|
||||
assign read_ram_sail_invoke_ret[0] = mem_read_fst_rdata_i;
|
||||
assign read_ram_sail_invoke_ret[1] = mem_read_snd_rdata_i;
|
||||
|
||||
t_MainResult main_result;
|
||||
|
||||
t_Mstatus mstatus_out;
|
||||
assign mstatus_o.mie = mstatus_out.bits[3];
|
||||
assign mstatus_o.mpie = mstatus_out.bits[7];
|
||||
assign mstatus_o.tw = mstatus_out.bits[21];
|
||||
assign mstatus_o.mprv = mstatus_out.bits[17];
|
||||
assign mstatus_o.mpp = mstatus_out.bits[12:11];
|
||||
|
||||
t_Mcause mcause_out;
|
||||
assign mcause_o = mcause_out.bits;
|
||||
|
||||
t_Minterrupts mie_out;
|
||||
assign mie_o = mie_out.bits;
|
||||
|
||||
t_Counteren mcounteren_out;
|
||||
assign mcounteren_o = mcounteren_out.bits;
|
||||
|
||||
t_Mtvec mtvec_out;
|
||||
assign mtvec_o = mtvec_out.bits;
|
||||
|
||||
t_Pmpcfg_ent pmpcfg_n_in[63:0];
|
||||
logic [31:0] pmpaddr_n_in[63:0];
|
||||
t_Pmpcfg_ent pmpcfg_n_out[63:0];
|
||||
logic [31:0] pmpaddr_n_out[63:0];
|
||||
for (genvar i = 0; i < 64; i++) begin: g_pmp_bind
|
||||
if (i < PMPNumRegions) begin: g_pmp_bind_real
|
||||
assign pmpcfg_n_in[i] = '{bits: pmp_cfg_i[i]};
|
||||
assign pmpaddr_n_in[i] = pmp_addr_i[i];
|
||||
|
||||
assign pmp_cfg_o[i] = pmpcfg_n_out[i].bits[7:0];
|
||||
assign pmp_addr_o[i] = pmpaddr_n_out[i];
|
||||
end else begin: g_pmp_bind_zero
|
||||
// These shouldn't ever be used anyway
|
||||
assign pmpcfg_n_in[i] = '{bits: 0};
|
||||
assign pmpaddr_n_in[i] = 0;
|
||||
end
|
||||
end
|
||||
|
||||
t_Mseccfg_ent mseccfg_out;
|
||||
assign mseccfg_o = mseccfg_out.bits;
|
||||
|
||||
sail_ibexspec spec_i(
|
||||
.cur_inst_in(insn_bits),
|
||||
.cur_inst_out(),
|
||||
.cur_privilege_in(priv_i),
|
||||
.cur_privilege_out(priv_o),
|
||||
.instbits_in(insn_bits),
|
||||
.instbits_out(),
|
||||
.marchid_in(march_id_i),
|
||||
.marchid_out(),
|
||||
.mcause_in('{bits: mcause_i}),
|
||||
.mcause_out,
|
||||
.mconfigptr_in(mconfigptr_i),
|
||||
.mconfigptr_out(),
|
||||
.mcounteren_in('{ bits: mcounteren_i }),
|
||||
.mcounteren_out,
|
||||
.mcountinhibit_in(),
|
||||
.mcountinhibit_out(),
|
||||
.mcycle_in(mcycle_i),
|
||||
.mcycle_out(mcycle_o),
|
||||
.medeleg_in('{bits: 32'h0}),
|
||||
.medeleg_out(),
|
||||
.menvcfg_in('{bits: 32'h0}),
|
||||
.menvcfg_out(),
|
||||
.mepc_in(mepc_i),
|
||||
.mepc_out(mepc_o),
|
||||
.mhartid_in(mhart_id_i),
|
||||
.mhartid_out(mhart_id_o),
|
||||
.mideleg_in(),
|
||||
.mideleg_out(),
|
||||
.mie_in('{bits: mie_i}),
|
||||
.mie_out,
|
||||
.mimpid_in(mimp_id_i),
|
||||
.mimpid_out(mimp_id_o),
|
||||
.minstret_in(minstret_i),
|
||||
.minstret_out(minstret_o),
|
||||
.minstret_increment_in(),
|
||||
.minstret_increment_out(),
|
||||
.mip_in('{bits: mip_i}),
|
||||
.mip_out(),
|
||||
.misa_in('{bits: misa_i}),
|
||||
.misa_out(),
|
||||
.mscratch_in(mscratch_i),
|
||||
.mscratch_out(mscratch_o),
|
||||
.mstatus_in('{bits:
|
||||
(32'(mstatus_i.mie) << 3) |
|
||||
(32'(mstatus_i.mpie) << 7) |
|
||||
(32'(mstatus_i.tw) << 21) |
|
||||
(32'(mstatus_i.mprv) << 17) |
|
||||
(32'(mstatus_i.mpp) << 11)
|
||||
}),
|
||||
.mstatus_out,
|
||||
.mstatush_in('{bits: 32'b0}),
|
||||
.mstatush_out(),
|
||||
.mtval_in(mtval_i),
|
||||
.mtval_out(mtval_o),
|
||||
.mtvec_in('{bits: mtvec_i}),
|
||||
.mtvec_out,
|
||||
.mvendorid_in(mvendor_id_i),
|
||||
.mvendorid_out(mvendor_id_o),
|
||||
.nextPC_in(nextpc_i),
|
||||
.nextPC_out(pc_o),
|
||||
.PC_in(pc_i),
|
||||
.PC_out(),
|
||||
.mseccfg_in('{bits: mseccfg_i}),
|
||||
.mseccfg_out,
|
||||
.mseccfgh_in(32'h0),
|
||||
.mseccfgh_out(),
|
||||
.pmpaddr_n_in,
|
||||
.pmpaddr_n_out,
|
||||
.pmpcfg_n_in,
|
||||
.pmpcfg_n_out,
|
||||
.scause_in(),
|
||||
.scause_out(),
|
||||
.scounteren_in(),
|
||||
.scounteren_out(),
|
||||
.sedeleg_in(),
|
||||
.sedeleg_out(),
|
||||
.senvcfg_in(),
|
||||
.senvcfg_out(),
|
||||
.sepc_in(),
|
||||
.sepc_out(),
|
||||
.sideleg_in(),
|
||||
.sideleg_out(),
|
||||
.sscratch_in(),
|
||||
.sscratch_out(),
|
||||
.stval_in(),
|
||||
.stval_out(),
|
||||
.stvec_in(),
|
||||
.stvec_out(),
|
||||
.tselect_in(),
|
||||
.tselect_out(),
|
||||
.x1_in(),
|
||||
.x1_out(),
|
||||
.x2_in(),
|
||||
.x2_out(),
|
||||
.x3_in(),
|
||||
.x3_out(),
|
||||
.x4_in(),
|
||||
.x4_out(),
|
||||
.x5_in(),
|
||||
.x5_out(),
|
||||
.x6_in(),
|
||||
.x6_out(),
|
||||
.x7_in(),
|
||||
.x7_out(),
|
||||
.x8_in(),
|
||||
.x8_out(),
|
||||
.x9_in(),
|
||||
.x9_out(),
|
||||
.x10_in(),
|
||||
.x10_out(),
|
||||
.x11_in(),
|
||||
.x11_out(),
|
||||
.x12_in(),
|
||||
.x12_out(),
|
||||
.x13_in(),
|
||||
.x13_out(),
|
||||
.x14_in(),
|
||||
.x14_out(),
|
||||
.x15_in(),
|
||||
.x15_out(),
|
||||
.x16_in(),
|
||||
.x16_out(),
|
||||
.x17_in(),
|
||||
.x17_out(),
|
||||
.x18_in(),
|
||||
.x18_out(),
|
||||
.x19_in(),
|
||||
.x19_out(),
|
||||
.x20_in(),
|
||||
.x20_out(),
|
||||
.x21_in(),
|
||||
.x21_out(),
|
||||
.x22_in(),
|
||||
.x22_out(),
|
||||
.x23_in(),
|
||||
.x23_out(),
|
||||
.x24_in(),
|
||||
.x24_out(),
|
||||
.x25_in(),
|
||||
.x25_out(),
|
||||
.x26_in(),
|
||||
.x26_out(),
|
||||
.x27_in(),
|
||||
.x27_out(),
|
||||
.x28_in(),
|
||||
.x28_out(),
|
||||
.x29_in(),
|
||||
.x29_out(),
|
||||
.x30_in(),
|
||||
.x30_out(),
|
||||
.x31_in(),
|
||||
.x31_out(),
|
||||
|
||||
.wX_sail_invoke,
|
||||
.wX_sail_invoke_ret(),
|
||||
.wX_sail_invoke_arg_0,
|
||||
.wX_sail_invoke_arg_1,
|
||||
|
||||
.rX_sail_invoke,
|
||||
.rX_sail_invoke_ret,
|
||||
.rX_sail_invoke_arg_0,
|
||||
|
||||
.write_ram_sail_invoke,
|
||||
.write_ram_sail_invoke_ret(),
|
||||
.write_ram_sail_invoke_arg_0(),
|
||||
.write_ram_sail_invoke_arg_1,
|
||||
.write_ram_sail_invoke_arg_2,
|
||||
.write_ram_sail_invoke_arg_3,
|
||||
|
||||
.read_ram_sail_invoke,
|
||||
.read_ram_sail_invoke_ret,
|
||||
.read_ram_sail_invoke_arg_0(),
|
||||
.read_ram_sail_invoke_arg_1,
|
||||
|
||||
.main_result(main_result),
|
||||
.insn_bits(insn_bits),
|
||||
.mode(main_mode)
|
||||
);
|
||||
|
||||
assign int_err_o = spec_i.sail_reached_unreachable |
|
||||
spec_i.sail_have_exception |
|
||||
(main_result != MAINRES_OK);
|
||||
|
||||
endmodule
|
||||
80
dv/formal/spec/stub.sv
Normal file
80
dv/formal/spec/stub.sv
Normal file
|
|
@ -0,0 +1,80 @@
|
|||
// Copyright lowRISC contributors.
|
||||
// Copyright 2024 University of Oxford, see also CREDITS.md.
|
||||
// Licensed under the Apache License, Version 2.0, see LICENSE for details.
|
||||
// Original author: Louis-Emile Ploix
|
||||
// SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
/*
|
||||
Provides stubs (mostly) for the native functions the Sail expects to see, mostly
|
||||
handling config stuff.
|
||||
*/
|
||||
|
||||
function automatic logic[127:0] sail_emod_int(logic[127:0] x, logic[127:0] y);
|
||||
// This one is unsigned, but the rest should be signed
|
||||
return x % y;
|
||||
endfunction
|
||||
|
||||
function automatic logic[127:0] sail_pow_int(logic[127:0] x, logic[127:0] y);
|
||||
// These are Sail integers, so operations on them should be signed
|
||||
return signed'(x) ** signed'(y);
|
||||
endfunction
|
||||
|
||||
function automatic logic[127:0] sail_tmod_int(logic[127:0] x, logic[127:0] y);
|
||||
return signed'(x) % signed'(y);
|
||||
endfunction
|
||||
|
||||
function automatic logic[127:0] sail_tdiv_int(logic[127:0] x, logic[127:0] y);
|
||||
return signed'(x) / signed'(y);
|
||||
endfunction
|
||||
|
||||
function automatic sail_bits sail_shift_bits_left(sail_bits x, sail_bits y);
|
||||
return {x.size, x.bits << y.bits};
|
||||
endfunction
|
||||
|
||||
function automatic sail_bits sail_shift_bits_right(sail_bits x, sail_bits y);
|
||||
return {x.size, x.bits >> y.bits};
|
||||
endfunction
|
||||
|
||||
function automatic sail_unit sail_decimal_string_of_bits(logic [11:0] x);
|
||||
return SAIL_UNIT;
|
||||
endfunction
|
||||
function automatic logic sail_elf_tohost(sail_unit u); return 0; endfunction
|
||||
function automatic logic sail_get_config_print_mem(sail_unit u); return 0; endfunction
|
||||
function automatic logic sail_get_config_print_platform(sail_unit u); return 0; endfunction
|
||||
function automatic logic sail_get_config_print_reg(sail_unit u); return 0; endfunction
|
||||
function automatic logic sail_get_config_print_instr(sail_unit u); return 0; endfunction
|
||||
function automatic logic sail_get_config_print_exception(sail_unit u); return 0; endfunction
|
||||
function automatic logic[31:0] sail_plat_clint_base(sail_unit u); return 0; endfunction
|
||||
function automatic logic[31:0] sail_plat_clint_size(sail_unit u); return 0; endfunction
|
||||
function automatic logic sail_plat_enable_dirty_update(sail_unit u); return 0; endfunction
|
||||
function automatic logic sail_plat_enable_misaligned_access(sail_unit u); return 1; endfunction
|
||||
function automatic logic sail_plat_enable_pmp(sail_unit u); return 0; endfunction
|
||||
function automatic sail_unit sail_platform_barrier(t_barrier_kind k); return SAIL_UNIT; endfunction
|
||||
function automatic sail_unit sail_platform_write_mem_ea(
|
||||
t_write_kind a, logic [63:0] b, sail_bits c, logic [127:0] d
|
||||
); return SAIL_UNIT; endfunction
|
||||
function automatic logic[15:0] sail_plat_get_16_random_bits(sail_unit u); return 0; endfunction
|
||||
function automatic logic sail_plat_htif_tohost(sail_unit u); return 0; endfunction
|
||||
function automatic logic sail_plat_mtval_has_illegal_inst_bits(sail_unit u); return 1; endfunction
|
||||
function automatic logic[31:0] sail_plat_ram_base(sail_unit u); return 0; endfunction
|
||||
function automatic logic[31:0] sail_plat_ram_size(sail_unit u); return 0; endfunction
|
||||
function automatic logic[31:0] sail_plat_rom_base(sail_unit u); return 0; endfunction
|
||||
function automatic logic[31:0] sail_plat_rom_size(sail_unit u); return 0; endfunction
|
||||
function automatic sail_unit sail_plat_term_write(logic[7:0] u); return SAIL_UNIT; endfunction
|
||||
function automatic sail_unit sail_print_mem_access(sail_unit u); return SAIL_UNIT; endfunction
|
||||
function automatic sail_unit sail_print_platform(sail_unit u); return SAIL_UNIT; endfunction
|
||||
function automatic sail_unit sail_print_reg(sail_unit u); return SAIL_UNIT; endfunction
|
||||
function automatic sail_unit sail_string_of_int(logic[127:0] u); return SAIL_UNIT; endfunction
|
||||
function automatic logic sail_sys_enable_fdext(sail_unit u); return 0; endfunction
|
||||
function automatic logic sail_sys_enable_rvc(sail_unit u); return 1; endfunction
|
||||
function automatic logic sail_sys_enable_writable_misa(sail_unit u); return 0; endfunction
|
||||
function automatic logic sail_sys_enable_zfinx(sail_unit u); return 0; endfunction
|
||||
function automatic sail_unit sail_cancel_reservation(sail_unit u); return SAIL_UNIT; endfunction
|
||||
function automatic logic[31:0] sail_plat_uart_base(sail_unit u); return 0; endfunction
|
||||
function automatic logic[31:0] sail_plat_uart_size(sail_unit u); return 0; endfunction
|
||||
function automatic logic[6:0] sail_sys_pmp_count(sail_unit u); return 7'd4; endfunction
|
||||
function automatic logic[6:0] sail_sys_pmp_max_count(sail_unit u); return 7'd16; endfunction
|
||||
function automatic sail_unit sail_load_reservation(logic[31:0] u); return SAIL_UNIT; endfunction
|
||||
function automatic logic sail_speculate_conditional(sail_unit u); return 0; endfunction
|
||||
function automatic logic[63:0] sail_sys_pmp_grain(sail_unit u); return 0; endfunction
|
||||
function automatic logic sail_sys_enable_writable_fiom(sail_unit u); return 0; endfunction
|
||||
48
dv/formal/thm/btype.proof
Normal file
48
dv/formal/thm/btype.proof
Normal file
|
|
@ -0,0 +1,48 @@
|
|||
# Copyright lowRISC contributors.
|
||||
# Copyright 2024 University of Oxford, see also CREDITS.md.
|
||||
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
|
||||
# Original author: Louis-Emile Ploix
|
||||
# SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
# This file implements two small graph inductions required by btype and jtype instructions to
|
||||
# deal with the fact that the PC changes at inconvenient times.
|
||||
|
||||
lemma btype
|
||||
in (instr_will_progress & ex_is_pres_btype & ~ex_err)
|
||||
FinishFirstCycle: have (`ID.instr_first_cycle)
|
||||
/
|
||||
BInd:
|
||||
graph_induction +rev
|
||||
cond (`CR.instr_valid_id & ex_is_pres_btype & ~ex_err & ~ex_kill)
|
||||
inv nobranch (~ex_has_branched_d)
|
||||
inv eq (ex_has_branched_d == `CR.branch_decision && post_pc == ex_branch_dst)
|
||||
|
||||
entry (`CR.instr_new_id) -> stall oma progress
|
||||
|
||||
node stall nobranch (`ID.stall_ld_hz) => stall progress
|
||||
node oma eq (`IDG.outstanding_memory_access & ~`ID.stall_ld_hz) => oma progress
|
||||
split_bool (`CR.branch_decision)
|
||||
node progress eq (instr_will_progress)
|
||||
/
|
||||
in (instr_will_progress & ex_is_pres_btype & ~ex_err)
|
||||
NoBranch: have (~`CR.branch_decision |-> spec_post_pc == pre_nextpc)
|
||||
Branch: have (`CR.branch_decision |-> spec_post_pc == `CR.branch_target_ex)
|
||||
|
||||
lemma jump
|
||||
in (instr_will_progress & ex_is_pres_jump & ~ex_err)
|
||||
FinishFirstCycle: have (`ID.instr_first_cycle)
|
||||
/
|
||||
JInd:
|
||||
graph_induction +rev
|
||||
cond (`CR.instr_valid_id & ex_is_pres_jump & ~ex_err & ~ex_kill)
|
||||
inv nobranch (~ex_has_branched_d)
|
||||
inv eq (ex_has_branched_d && post_pc[31:1] == `CR.branch_target_ex[31:1])
|
||||
|
||||
entry (`CR.instr_new_id) -> stall oma progress
|
||||
|
||||
node stall nobranch (`ID.stall_ld_hz) => stall progress
|
||||
node oma eq (`IDG.outstanding_memory_access & ~`ID.stall_ld_hz) => oma progress
|
||||
node progress eq (instr_will_progress)
|
||||
/
|
||||
in (instr_will_progress & ex_is_pres_jump & ~ex_err)
|
||||
Branch: have (spec_post_pc[31:1] == `CR.branch_target_ex[31:1])
|
||||
326
dv/formal/thm/ibex.proof
Normal file
326
dv/formal/thm/ibex.proof
Normal file
|
|
@ -0,0 +1,326 @@
|
|||
# Copyright lowRISC contributors.
|
||||
# Copyright 2024 University of Oxford, see also CREDITS.md.
|
||||
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
|
||||
# Original author: Louis-Emile Ploix
|
||||
# SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
# This file contains mostly just small helper invariants about all sorts. They are all generally easy to prove.
|
||||
# It also contains the first memory graph induction, it's consequences, and liveness.
|
||||
|
||||
lemma ibex
|
||||
NotDataIndTiming: have (~`CSR.data_ind_timing_o)
|
||||
|
||||
PrivMorUMpp: have ((`CSR.mstatus_q.mpp == PRIV_LVL_U) || (`CSR.mstatus_q.mpp == PRIV_LVL_M))
|
||||
PrivMorUCur: have ((`CSR.priv_lvl_q == PRIV_LVL_U) || (`CSR.priv_lvl_q == PRIV_LVL_M))
|
||||
|
||||
PCBit0: have (~`CR.pc_id[0])
|
||||
MtvecLow: have (pre_mtvec[7:0] == 8'h01)
|
||||
NmiMode: have (~`IDC.nmi_mode_q)
|
||||
EBreakIntoDebug: have (~`IDC.ebreak_into_debug)
|
||||
NoEnterDebugMode: have (~`IDC.enter_debug_mode)
|
||||
IfBusErr: have (`IF.if_id_pipe_reg_we |-> ~`IF.if_instr_bus_err)
|
||||
|
||||
WfiKill: have (wbexc_exists & wbexc_is_wfi |-> ex_kill)
|
||||
ErrKill: have (wbexc_exists & wbexc_err |-> ex_kill)
|
||||
|
||||
ReqRequiresInstr: have (data_req_o |-> ex_has_compressed_instr)
|
||||
ReqRequiresNotIllegal: have (data_req_o |-> ~`CR.illegal_insn_id & ~`CR.illegal_c_insn_id)
|
||||
|
||||
AluInstrMatch: have (`CR.instr_rdata_id == `CR.instr_rdata_alu_id)
|
||||
|
||||
IdExNotReq: have (~ex_is_mem_instr -> ~data_req_o)
|
||||
IdExNotMemMuteIncr: have (`CR.instr_valid_id & ~ex_is_mem_instr -> ~`ID.lsu_addr_incr_req_i & ~`ID.lsu_req_done_i)
|
||||
ExecNoSpecialReq: have (`ID.instr_executing & ~instr_will_progress |-> ~`IDC.special_req)
|
||||
StallIdFSM1: have (`ID.instr_executing && `ID.id_fsm_d != 0 |-> ~instr_will_progress)
|
||||
|
||||
WbexcErrMonotonic: have (wbexc_exists & wbexc_err & ~instr_will_progress & ~wbexc_finishing |=> wbexc_err)
|
||||
|
||||
NonCompressedMatch: have (wbexc_finishing && wbexc_instr[1:0] == 2'b11 |-> wbexc_instr == wbexc_decompressed_instr)
|
||||
CompressedMatch: have (ex_has_compressed_instr |-> ex_compressed_instr[15:0] == `CR.instr_rdata_c_id)
|
||||
|
||||
PostFlushNoInstr: have (`IDC.ctrl_fsm_cs == `IDC.FLUSH |=> ~`CR.instr_valid_id)
|
||||
|
||||
DecompressionIllegalIdEx: have (ex_has_compressed_instr |-> decompressed_instr_illegal == `CR.illegal_c_insn_id)
|
||||
DecompressionMatchIdEx: have (ex_has_compressed_instr & ~`CR.illegal_insn_id & ~`CR.illegal_c_insn_id |-> decompressed_instr == `CR.instr_rdata_id)
|
||||
DecompressionIllegalWbexc: have (wbexc_exists |-> decompressed_instr_illegal_2 == wbexc_compressed_illegal)
|
||||
DecompressionMatchWbexc: have (wbexc_exists & ~wbexc_illegal & ~wbexc_compressed_illegal |-> decompressed_instr_2 == wbexc_decompressed_instr)
|
||||
|
||||
HasCompressed: have (`CR.instr_valid_id |-> ex_has_compressed_instr)
|
||||
LSUInstrStable: have (`LSU.ls_fsm_cs != 0 |-> $stable(`CR.instr_rdata_id))
|
||||
|
||||
NoneIdleIsDecode: have (`LSU.ls_fsm_cs != 0 |-> `IDC.ctrl_fsm_cs == 5)
|
||||
LSUFinishWaitRvalidMisGntsDone: have (`LSU.ls_fsm_cs == 4 && data_rvalid_i |-> instr_will_progress)
|
||||
LSUFinishWaitRvalidMis: have (`LSU.ls_fsm_cs == 2 && data_rvalid_i && data_gnt_i |-> instr_will_progress)
|
||||
LSUFinishWaitGnt: have (`LSU.ls_fsm_cs == 3 && data_gnt_i |-> instr_will_progress)
|
||||
LSUFinishFast: have (`LSU.ls_fsm_cs == 0 && data_gnt_i && `LSU.ls_fsm_ns == 0 |-> instr_will_progress)
|
||||
|
||||
SndGntReqFstGnt: have (mem_gnt_snd_d |-> mem_gnt_fst_q)
|
||||
|
||||
WBOutstandingNoReq: have (outstanding_mem & ~`LSU.lsu_resp_valid_o |-> ~data_req_o)
|
||||
|
||||
NotIdleReqDec: have (`LSU.ls_fsm_cs != `LSU.IDLE |-> `ID.lsu_req_dec)
|
||||
NotIdleNoExErr: have (`LSU.ls_fsm_cs != `LSU.IDLE |-> ~ex_err)
|
||||
|
||||
ProgressNoWbStall: have (instr_will_progress |-> ~`IDC.stall_wb_i)
|
||||
|
||||
NoStoreWb: have (`WBG.wb_instr_type_q == WB_INSTR_STORE |-> ~`WB.rf_we_wb_o)
|
||||
WbInstrDefined: have (`WBG.wb_instr_type_q != 2'b11)
|
||||
|
||||
RfWriteWb: have (`CR.rf_write_wb & wbexc_finishing |-> `WB.rf_we_wb_o)
|
||||
|
||||
CtrlWbexc: have (wbexc_exists |-> `IDC.ctrl_fsm_cs == `IDC.DECODE || `IDC.ctrl_fsm_cs == `IDC.FLUSH)
|
||||
ProgressDecode: have (instr_will_progress |-> `IDC.ctrl_fsm_cs == `IDC.DECODE)
|
||||
|
||||
BranchedProg: have (ex_has_branched_d & ~instr_will_progress |=> ex_has_branched_d | `IDC.wb_exception_o)
|
||||
|
||||
IDCFsmAny: have (`IDC.ctrl_fsm_cs inside {`IDC.RESET, `IDC.BOOT_SET, `IDC.WAIT_SLEEP, `IDC.SLEEP, `IDC.FIRST_FETCH, `IDC.DECODE, `IDC.IRQ_TAKEN, `IDC.FLUSH})
|
||||
IDCFsmNotBoot: have (##3 ~(`IDC.ctrl_fsm_cs inside {`IDC.RESET, `IDC.BOOT_SET}))
|
||||
|
||||
MemInstrEx: have (`LSU.ls_fsm_cs != `LSU.IDLE |-> ex_is_mem_instr)
|
||||
MemInstrWbLoad: have (`WB.outstanding_load_wb_o |-> wbexc_is_load_instr)
|
||||
MemInstrWbStore: have (`WB.outstanding_store_wb_o |-> wbexc_is_store_instr)
|
||||
MemClockEn: have (`LSU.ls_fsm_cs != `LSU.IDLE |-> ibex_top_i.core_busy_q)
|
||||
|
||||
ClockEn: have (instr_will_progress |-> ibex_top_i.clock_en)
|
||||
EnWbProgress: have (`WB.en_wb_i |-> instr_will_progress)
|
||||
DoneFin: have (`WBG.wb_done & `WBG.wb_valid_q & ~wbexc_err |-> wbexc_finishing)
|
||||
ValidExists: have (`WBG.wb_valid_q |-> wbexc_exists)
|
||||
|
||||
UnCheckableNoPresent: have (wbexc_exists & `ISS_CSR & ~wbexc_is_checkable_csr |-> ~has_spec_past)
|
||||
|
||||
MemInstrWbWrite: have (
|
||||
wbexc_exists & wbexc_is_store_instr & ~wbexc_err |->
|
||||
~`WBG.rf_we_wb_q & (`WBG.wb_instr_type_q != WB_INSTR_LOAD)
|
||||
)
|
||||
ValidToBranch: have (ex_has_branched_d |-> `CR.instr_valid_id)
|
||||
|
||||
LsuWeq: block
|
||||
Ex: have (`LSU.ls_fsm_cs != `LSU.IDLE && mem_gnt_fst_q |-> ex_is_store_instr == `LSU.data_we_q)
|
||||
/
|
||||
Wb: have (outstanding_mem |-> wbexc_is_store_instr == `LSU.data_we_q)
|
||||
|
||||
block
|
||||
LSUEmpty: have (`LSU.ls_fsm_cs != `LSU.IDLE |-> ~wbexc_exists & ~ex_kill)
|
||||
/
|
||||
LSUEnd: have (`LSU.lsu_req_done_o |-> instr_will_progress)
|
||||
|
||||
block
|
||||
NoFinishingIRQ: have (wbexc_exists |-> ~wbexc_handling_irq)
|
||||
/
|
||||
SpecPastReg: have (wbexc_exists & wbexc_post_wX_en |-> spec_past_regs[wbexc_post_wX_addr] == wbexc_post_wX)
|
||||
SpecPastWbexc:
|
||||
each X Priv:(priv) Mstatus:(mstatus) Mie:(mie) Mcause:(mcause) Mtval:(mtval) Mtvec:(mtvec) \
|
||||
Mscratch:(mscratch) Mepc:(mepc) Mcounteren:(mcounteren) \
|
||||
Pmp_cfg:(pmp_cfg) Pmp_addr:(pmp_addr) Mseccfg:(mseccfg) \
|
||||
Pc:(pc)
|
||||
have (wbexc_exists |-> spec_past_``X == wbexc_post_``X)
|
||||
|
||||
/
|
||||
|
||||
# This graph induction bounds the number of waiting responses,
|
||||
# and establishes conditions for PMP errors, and relates the presence
|
||||
# of waiting responses to the outstanding_mem signal.
|
||||
# It includes all LSU states and a couple of extra states for
|
||||
# once the instruction moves/has moved to writeback.
|
||||
Memory: graph_induction +rev
|
||||
inv idle (
|
||||
~`LSU.handle_misaligned_q &&
|
||||
`CR.lsu_resp_valid == outstanding_mem
|
||||
)
|
||||
inv idle_active (
|
||||
data_mem_assume.outstanding_reqs == data_gnt_i &&
|
||||
~`LSU.pmp_err_q && ~`LSU.lsu_err_d && ~`LSU.handle_misaligned_q &&
|
||||
`CR.lsu_resp_valid == outstanding_mem
|
||||
)
|
||||
inv wait_gnt_mis (
|
||||
$stable(data_addr_o) && ~has_resp_waiting_q && ~`LSU.lsu_err_q &&
|
||||
(data_req_o == ~`LSU.pmp_err_q) && (`LSU.pmp_err_q == `CR.pmp_req_err[2])
|
||||
)
|
||||
inv wait_gnt (
|
||||
$stable(data_addr_o) && ~has_resp_waiting_q &&
|
||||
(data_req_o == ~`LSU.pmp_err_q) && (`LSU.pmp_err_q == `CR.pmp_req_err[2])
|
||||
)
|
||||
inv wait_rvalid_mis (
|
||||
($stable(`LSU.ls_fsm_cs) -> $stable(data_addr_o)) &&
|
||||
~`LSU.lsu_err_q &&
|
||||
((~`LSU.pmp_err_q && has_one_resp_waiting_q) || (`LSU.pmp_err_q && ~has_resp_waiting_q))
|
||||
)
|
||||
inv wait_rvalid_mis_gnts_done (
|
||||
$stable(data_addr_o) &&
|
||||
(`LSU.pmp_err_q == `CR.pmp_req_err[2]) &&
|
||||
(
|
||||
(~`LSU.lsu_err_q && ~`LSU.pmp_err_q && has_two_resp_waiting_q) ||
|
||||
((`LSU.lsu_err_q != `LSU.pmp_err_q) && has_one_resp_waiting_q) ||
|
||||
(`LSU.lsu_err_q && `LSU.pmp_err_q && ~has_resp_waiting_q)
|
||||
)
|
||||
)
|
||||
|
||||
inv step (`LSU.ls_fsm_ns == `LSU.IDLE && `CR.instr_type_wb != WB_INSTR_OTHER && has_one_resp_waiting_d)
|
||||
inv step_fail (`LSU.ls_fsm_ns == `LSU.IDLE && `CR.instr_type_wb != WB_INSTR_OTHER && ~has_resp_waiting_d && `CR.pmp_req_err[2])
|
||||
inv wait (outstanding_mem && has_one_resp_waiting_q && ~`LSU.lsu_req_i && wbexc_exists)
|
||||
inv end (outstanding_mem && has_one_resp_waiting_q && wbexc_exists)
|
||||
inv fail (outstanding_mem && ~has_resp_waiting_q && wbexc_exists)
|
||||
|
||||
entry ($rose(rst_ni)) -> idle
|
||||
|
||||
node idle idle (`LSU.ls_fsm_cs == `LSU.IDLE && data_mem_assume.outstanding_reqs == data_gnt_i)
|
||||
edge idle => idle
|
||||
edge idle -> idle_active
|
||||
|
||||
node idle_active idle_active (`LSU.ls_fsm_cs == `LSU.IDLE && `CR.lsu_req)
|
||||
edge idle_active => wait_rvalid_mis wait_gnt_mis wait_gnt
|
||||
edge idle_active -> step step_fail
|
||||
|
||||
node wait_gnt_mis wait_gnt_mis (`LSU.ls_fsm_cs == `LSU.WAIT_GNT_MIS)
|
||||
edge wait_gnt_mis => wait_gnt_mis wait_rvalid_mis
|
||||
|
||||
node wait_rvalid_mis wait_rvalid_mis (`LSU.ls_fsm_cs == `LSU.WAIT_RVALID_MIS)
|
||||
edge wait_rvalid_mis => wait_rvalid_mis wait_rvalid_mis_gnts_done wait_gnt
|
||||
edge wait_rvalid_mis -> step step_fail
|
||||
|
||||
node wait_gnt wait_gnt (`LSU.ls_fsm_cs == `LSU.WAIT_GNT)
|
||||
edge wait_gnt => wait_gnt
|
||||
edge wait_gnt -> step step_fail
|
||||
|
||||
node wait_rvalid_mis_gnts_done wait_rvalid_mis_gnts_done (`LSU.ls_fsm_cs == `LSU.WAIT_RVALID_MIS_GNTS_DONE)
|
||||
edge wait_rvalid_mis_gnts_done => wait_rvalid_mis_gnts_done
|
||||
edge wait_rvalid_mis_gnts_done -> step step_fail
|
||||
|
||||
node step step (`LSU.lsu_req_done_o && ~`LSU.pmp_err_d)
|
||||
edge step => wait end
|
||||
|
||||
node step_fail step_fail (`LSU.lsu_req_done_o && `LSU.pmp_err_d)
|
||||
edge step_fail => fail
|
||||
|
||||
node wait wait (has_resp_waiting_q && ~`CR.lsu_resp_valid && `LSU.ls_fsm_cs == `LSU.IDLE && ~instr_will_progress)
|
||||
edge wait => wait end
|
||||
|
||||
node end end (`CR.lsu_resp_valid && `LSU.ls_fsm_cs == `LSU.IDLE && data_rvalid_i)
|
||||
edge end -> idle
|
||||
|
||||
node fail fail (`CR.lsu_resp_valid && `LSU.ls_fsm_cs == `LSU.IDLE && ~data_rvalid_i)
|
||||
edge fail -> idle
|
||||
/
|
||||
NoMemAccessNoRValid: have (`LSU.lsu_resp_valid_o -> outstanding_mem)
|
||||
StallNoChangeA: have (`LSU.ls_fsm_cs != `LSU.IDLE && ($past(`LSU.ls_fsm_cs) != `LSU.IDLE || $past(`LSU.lsu_req_i)) |-> $stable(`ID.rf_rdata_a_fwd))
|
||||
StallNoChangeB: have (data_we_o && `LSU.ls_fsm_cs != `LSU.IDLE && ($past(`LSU.ls_fsm_cs) != `LSU.IDLE || $past(`LSU.lsu_req_i)) |-> $stable(`ID.rf_rdata_b_fwd))
|
||||
|
||||
BecameDecodeIsInstrStart: have (`IDC.ctrl_fsm_cs == `IDC.DECODE && !$stable(`IDC.ctrl_fsm_cs) |-> ~`ID.instr_valid_i | `CR.instr_new_id)
|
||||
BecameDecodeIsEmptyWbexc: have (`IDC.ctrl_fsm_cs == `IDC.DECODE && !$stable(`IDC.ctrl_fsm_cs) |-> ~wbexc_exists)
|
||||
FetchErrIsErr: have (wbexc_fetch_err & wbexc_exists |-> wbexc_err & `IDC.instr_fetch_err)
|
||||
|
||||
MemOpRequiresValid: have (`LSU.ls_fsm_cs != `LSU.IDLE || `CR.lsu_req |-> `ID.instr_valid_i)
|
||||
|
||||
MultEndState: have (instr_will_progress |=> `MULTG.mult_state_q == `MULTG.ALBL)
|
||||
|
||||
/
|
||||
|
||||
MemErrKind: have (finishing_executed && wbexc_is_mem_instr && ~wbexc_illegal && wbexc_err |-> `IDC.store_err_q | `IDC.load_err_q)
|
||||
MemErrStructure: have (finishing_executed && wbexc_is_mem_instr && ~wbexc_illegal && wbexc_err |-> $past(instr_will_progress, 2) | $past(data_rvalid_i))
|
||||
MemNoErrStructure: have (finishing_executed && wbexc_is_mem_instr && ~wbexc_illegal && ~wbexc_err |-> data_rvalid_i)
|
||||
|
||||
WbexcMemErrKindLoad: have (`IDC.load_err_q |-> wbexc_exists & wbexc_is_load_instr)
|
||||
WbexcMemErrKindStore: have (`IDC.store_err_q |-> wbexc_exists & wbexc_is_store_instr)
|
||||
|
||||
WbexcNotMemMuteLSU: have (~wbexc_is_mem_instr -> ~`CR.rf_we_lsu & ~`CR.lsu_resp_valid & ~`CR.lsu_load_err & ~`CR.lsu_store_err)
|
||||
WbexcNotMemMuteMemErr: have (~wbexc_is_mem_instr -> ~`IDC.load_err_q & ~`IDC.store_err_q)
|
||||
StallIdFSM2: have (`ID.instr_executing && ~instr_will_progress |=> `ID.instr_executing)
|
||||
NewIdFSM: have (`CR.instr_new_id |-> `ID.id_fsm_q == 0)
|
||||
PreNextPcMatch: have (instr_will_progress & ~ex_has_branched_d & ~`IDC.instr_fetch_err -> pre_nextpc == `CR.pc_if) # Slow!
|
||||
StallNoChangeLsuWData: have ((data_we_o && `LSU.ls_fsm_cs != `LSU.IDLE && ($past(`LSU.ls_fsm_cs) != `LSU.IDLE || $past(`LSU.lsu_req_i)) |-> $stable(`LSU.lsu_wdata_i)))
|
||||
|
||||
# These properties take some time to prove, but do prove with low proof effort. Just run them with individual Hp instances.
|
||||
SpecStableLoad: have (ex_is_pres_load_instr && `LSU.ls_fsm_cs != `LSU.IDLE && ($past(`LSU.ls_fsm_cs) != `LSU.IDLE || $past(`LSU.lsu_req_i)) |-> $stable(spec_mem_read))
|
||||
SpecStableLoadSnd: have (ex_is_pres_load_instr && `LSU.ls_fsm_cs != `LSU.IDLE && ($past(`LSU.ls_fsm_cs) != `LSU.IDLE || $past(`LSU.lsu_req_i)) |-> $stable(spec_mem_read_snd))
|
||||
SpecStableLoadAddr: have (ex_is_pres_load_instr && `LSU.ls_fsm_cs != `LSU.IDLE && ($past(`LSU.ls_fsm_cs) != `LSU.IDLE || $past(`LSU.lsu_req_i)) |-> $stable(spec_mem_read_fst_addr))
|
||||
SpecStableLoadSndAddr: have (ex_is_pres_load_instr && `LSU.ls_fsm_cs != `LSU.IDLE && ($past(`LSU.ls_fsm_cs) != `LSU.IDLE || $past(`LSU.lsu_req_i)) |-> $stable(spec_mem_read_snd_addr))
|
||||
|
||||
SpecStableStore: have (ex_is_pres_store_instr && `LSU.ls_fsm_cs != `LSU.IDLE && ($past(`LSU.ls_fsm_cs) != `LSU.IDLE || $past(`LSU.lsu_req_i)) |-> $stable(spec_mem_write))
|
||||
SpecStableStoreSnd: have (ex_is_pres_store_instr && `LSU.ls_fsm_cs != `LSU.IDLE && ($past(`LSU.ls_fsm_cs) != `LSU.IDLE || $past(`LSU.lsu_req_i)) |-> $stable(spec_mem_write_snd))
|
||||
SpecStableStoreAddr: have (ex_is_pres_store_instr && `LSU.ls_fsm_cs != `LSU.IDLE && ($past(`LSU.ls_fsm_cs) != `LSU.IDLE || $past(`LSU.lsu_req_i)) |-> $stable(spec_mem_write_fst_addr))
|
||||
SpecStableStoreSndAddr: have (ex_is_pres_store_instr && `LSU.ls_fsm_cs != `LSU.IDLE && ($past(`LSU.ls_fsm_cs) != `LSU.IDLE || $past(`LSU.lsu_req_i)) |-> $stable(spec_mem_write_snd_addr))
|
||||
SpecStableStoreData: have (ex_is_pres_store_instr && `LSU.ls_fsm_cs != `LSU.IDLE && ($past(`LSU.ls_fsm_cs) != `LSU.IDLE || $past(`LSU.lsu_req_i)) |-> $stable(spec_mem_write_fst_wdata))
|
||||
SpecStableStoreSndData: have (ex_is_pres_store_instr && `LSU.ls_fsm_cs != `LSU.IDLE && ($past(`LSU.ls_fsm_cs) != `LSU.IDLE || $past(`LSU.lsu_req_i)) |-> $stable(spec_mem_write_snd_wdata))
|
||||
|
||||
LoadNotSpecWrite: have (ex_is_pres_load_instr |-> ~spec_mem_write)
|
||||
StoreNotSpecRead: have (ex_is_pres_store_instr |-> ~spec_mem_read)
|
||||
|
||||
FirstCycleNoGnt: have (`ID.instr_first_cycle |-> ~mem_gnt_fst_q)
|
||||
MemStartFirstCycle: have (`LSU.ls_fsm_cs == `LSU.IDLE && `CR.lsu_req |-> `ID.instr_first_cycle)
|
||||
# The below is slow!
|
||||
DivInstrStable: have (`MULT.md_state_q != `MULT.MD_IDLE |-> $stable(`CR.instr_rdata_id) && `CR.instr_valid_id && (~`ID.stall_multdiv -> `MULT.md_state_q == `MULT.MD_FINISH) && `MULTG.mult_state_q == `MULTG.ALBL && `MULT.div_en_internal && (~wbexc_exists | wbexc_finishing))
|
||||
|
||||
InstrReqCount: have (
|
||||
(instr_mem_assume.outstanding_reqs_q == 2) == (`IFP.rdata_outstanding_q[1] && `IFP.rdata_outstanding_q[0]) &&
|
||||
(instr_mem_assume.outstanding_reqs_q == 1) == (~`IFP.rdata_outstanding_q[1] && `IFP.rdata_outstanding_q[0]) &&
|
||||
(instr_mem_assume.outstanding_reqs_q == 0) == (~`IFP.rdata_outstanding_q[1] && ~`IFP.rdata_outstanding_q[0])
|
||||
)
|
||||
|
||||
# Slow!
|
||||
FetchErrRoot: have (`ID.instr_valid_i && (`IDC.ctrl_fsm_cs == `IDC.FLUSH -> ~$past(`IDC.csr_pipe_flush)) |-> spec_fetch_err == `ID.instr_fetch_err_i)
|
||||
/
|
||||
|
||||
MepcEn: have (`CSR.mepc_en |-> instr_will_progress | wbexc_finishing | wbexc_handling_irq)
|
||||
DivNoKill: have (`MULT.md_state_q != `MULT.MD_IDLE |-> ~ex_kill)
|
||||
|
||||
RTypeFirstCycle: have (`CR.instr_valid_id & ex_is_rtype |-> `ID.instr_first_cycle_id_o)
|
||||
|
||||
DataMemGntMaxDelay: have (data_req_o |-> ##[0:`TIME_LIMIT] data_gnt_i)
|
||||
DataMemRvalidMaxDelay: have (data_gnt_i |=> ##[0:`TIME_LIMIT] data_rvalid_i)
|
||||
InstrMemGntMaxDelay: have (instr_req_o |-> ##[0:`TIME_LIMIT] instr_gnt_i)
|
||||
InstrMemRvalidMaxDelay: have (instr_gnt_i |=> ##[0:`TIME_LIMIT] instr_rvalid_i)
|
||||
|
||||
NormalMainResMatch: have (`ID.instr_valid_i && ~ex_kill && main_mode == MAIN_IDEX |-> spec_api_i.main_result == MAINRES_OK)
|
||||
FetchErrMainResMatch: have (`ID.instr_valid_i && ~ex_kill && main_mode == MAIN_IFERR |-> spec_api_i.main_result == MAINRES_OK)
|
||||
IRQMainResMatch: have (wbexc_handling_irq && main_mode == MAIN_IRQ |-> spec_api_i.main_result == MAINRES_OK)
|
||||
|
||||
/
|
||||
SpecEnUnreach: have (spec_en |-> ~spec_int_err)
|
||||
|
||||
# Liveness proofs, currently only work if TIME_LIMIT = 1 and WFI_BOUND = 20.
|
||||
# They work by adding up worst case bounds to arrive a weak but finite bound between calls to
|
||||
# instr_will_progress.
|
||||
lemma live
|
||||
DivMiddleStep: have (`MULT.md_state_q == `MULT.MD_COMP && $stable(`MULT.md_state_q) |-> `MULT.div_counter_q == $past(`MULT.div_counter_q) - 1)
|
||||
IF: have (always (##[0:10] `IF.if_instr_valid))
|
||||
PCSet: have (`CR.pc_set |-> ##[0:10] ~`CR.pc_set)
|
||||
/
|
||||
|
||||
DivStart: have (`CR.instr_new_id & `CR.instr_valid_id & ex_is_div |-> ##[0:7] (`MULT.div_counter_q == 5'd31 && `MULT.md_state_q == `MULT.MD_COMP) | instr_will_progress | (ex_kill & `CR.instr_valid_id))
|
||||
DivMiddle: have (`MULT.div_counter_q == 5'd31 && `MULT.md_state_q == `MULT.MD_COMP |-> ##30 `MULT.div_counter_q == 5'd1 && `MULT.md_state_q == `MULT.MD_COMP)
|
||||
DivEnd: have (`MULT.div_counter_q == 5'd1 && `MULT.md_state_q == `MULT.MD_COMP |-> ##3 instr_will_progress)
|
||||
|
||||
WFIStart: have (instr_will_progress & ex_is_wfi & ~ex_err |-> ##[0:5] `IDC.ctrl_fsm_cs == `IDC.SLEEP)
|
||||
WFIMiddle: have (`IDC.ctrl_fsm_cs == `IDC.SLEEP |-> ##[0:20] `IDC.ctrl_fsm_cs == `IDC.SLEEP && `IDC.ctrl_fsm_ns == `IDC.FIRST_FETCH)
|
||||
WFIEnd: have (`IDC.ctrl_fsm_cs == `IDC.SLEEP && `IDC.ctrl_fsm_ns == `IDC.FIRST_FETCH |-> ##[0:5] `IF.id_in_ready_i)
|
||||
|
||||
NewProgNormal: have (`CR.instr_new_id & `CR.instr_valid_id & ~ex_is_div & ~ex_is_mem_instr |-> ##[0:5] (instr_will_progress | (ex_kill & `CR.instr_valid_id)))
|
||||
NewProgMem: have (`CR.instr_new_id & `CR.instr_valid_id & ex_is_mem_instr |-> ##[0:10] (instr_will_progress | (ex_kill & `CR.instr_valid_id)))
|
||||
|
||||
ProgReadyNormal: have (instr_will_progress & (~ex_is_wfi | ex_err) |-> ##[0:5] `IF.id_in_ready_i)
|
||||
ProgReadyWFI: have (instr_will_progress & ex_is_wfi & ~ex_err |-> ##[0:30] `IF.id_in_ready_i)
|
||||
KillReady: have (ex_kill & `CR.instr_valid_id |-> ##[1:35] `IF.id_in_ready_i && ~wbexc_exists && ~`CR.instr_valid_id)
|
||||
|
||||
ReadyNew: have (`IF.id_in_ready_i |-> ##[1:11] `CR.instr_new_id & `CR.instr_valid_id)
|
||||
Initial: have ($rose(rst_ni) |-> ##[1:15] `CR.instr_new_id & `CR.instr_valid_id)
|
||||
FlushedNoKill: have (`CR.instr_new_id & `CR.instr_valid_id & ~wbexc_exists |-> ~ex_kill until_with instr_will_progress)
|
||||
/
|
||||
ReadyFlushed: have (`IF.id_in_ready_i && ~wbexc_exists && ~`CR.instr_valid_id |-> ##[1:11] `CR.instr_new_id & `CR.instr_valid_id & ~wbexc_exists)
|
||||
/
|
||||
DivNew1: have (`CR.instr_new_id & `CR.instr_valid_id & ex_is_div |-> ##[0:37] ((`MULT.div_counter_q == 5'd1 && `MULT.md_state_q == `MULT.MD_COMP) | instr_will_progress | (ex_kill & `CR.instr_valid_id)))
|
||||
/
|
||||
NewProgDiv: have (`CR.instr_new_id & `CR.instr_valid_id & ex_is_div |-> ##[0:40] (instr_will_progress | (ex_kill & `CR.instr_valid_id)))
|
||||
ProgReady: have (instr_will_progress |-> ##[0:30] `IF.id_in_ready_i)
|
||||
/
|
||||
NewProg: have (`CR.instr_new_id & `CR.instr_valid_id |-> ##[0:40] (instr_will_progress | (ex_kill & `CR.instr_valid_id)))
|
||||
/
|
||||
FlushedProg: have (`CR.instr_new_id & `CR.instr_valid_id & ~wbexc_exists |-> ##[0:40] instr_will_progress)
|
||||
/
|
||||
KillSpecEn: have (ex_kill & `CR.instr_valid_id |-> ##[0:86] spec_en)
|
||||
/
|
||||
NewReady: have (`CR.instr_new_id & `CR.instr_valid_id |-> ##[0:75] `IF.id_in_ready_i)
|
||||
NewSpecEn: have (`CR.instr_new_id & `CR.instr_valid_id |-> ##[0:40+86] spec_en)
|
||||
/
|
||||
NewLoop: have (`CR.instr_new_id & `CR.instr_valid_id |-> ##[1:86] `CR.instr_new_id & `CR.instr_valid_id)
|
||||
/
|
||||
New: have (always (##[1:86] `CR.instr_new_id & `CR.instr_valid_id))
|
||||
169
dv/formal/thm/mem.proof
Normal file
169
dv/formal/thm/mem.proof
Normal file
|
|
@ -0,0 +1,169 @@
|
|||
# Copyright lowRISC contributors.
|
||||
# Copyright 2024 University of Oxford, see also CREDITS.md.
|
||||
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
|
||||
# Original author: Louis-Emile Ploix
|
||||
# SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
lemma mem
|
||||
MemNotWFI: have (wbexc_exists && wbexc_is_mem_instr |-> ~wbexc_is_wfi)
|
||||
MemFin: have (finishing_executed && wbexc_is_mem_instr && ~wbexc_err |-> data_rvalid_i)
|
||||
|
||||
RespWait: have (wbexc_exists && wbexc_is_mem_instr && ~wbexc_err && ~data_rvalid_i |-> `LSU.ls_fsm_cs == `LSU.IDLE && ~`LSU.lsu_req_i)
|
||||
|
||||
EarlyLSUCtrlMatch: have (
|
||||
`LSU.ls_fsm_cs != `LSU.IDLE & spec_post_wX_en & mem_gnt_fst_q |->
|
||||
`LSU.rdata_offset_q == `LSU.data_offset && `LSU.data_type_q == `LSU.lsu_type_i && `LSU.data_sign_ext_q == `LSU.lsu_sign_ext_i && `LSU.data_we_q == `LSU.lsu_we_i
|
||||
)
|
||||
|
||||
MisStates: have (`LSU.ls_fsm_cs == `LSU.WAIT_GNT_MIS || `LSU.ls_fsm_cs == `LSU.WAIT_RVALID_MIS || `LSU.ls_fsm_cs == `LSU.WAIT_RVALID_MIS_GNTS_DONE |-> `LSU.split_misaligned_access)
|
||||
|
||||
LoadPMPErrorWx: have (`CR.instr_valid_id & ex_is_pres_load_instr |-> spec_post_wX_en == ~spec_has_pmp_err)
|
||||
|
||||
# Another graph induction for LSU states which specifically bind what is
|
||||
# happening to the specification.
|
||||
MemSpec: graph_induction +rev
|
||||
cond (ex_is_pres_mem_instr && (`LSU.ls_fsm_cs != `LSU.IDLE || `CR.lsu_req))
|
||||
|
||||
inv fst_req (
|
||||
(data_req_o -> (mem_req_fst_d && fst_mem_cmp)) &&
|
||||
(~data_req_o -> (~spec_mem_en_snd && spec_has_pmp_err && spec_post_mtval == `LSU.addr_last_d)) &&
|
||||
~mem_gnt_fst_q && addr_last_d_matches
|
||||
)
|
||||
inv fst_req_1 (
|
||||
(data_req_o -> (mem_req_fst_d && fst_mem_cmp && ~spec_has_pmp_err)) &&
|
||||
(~data_req_o -> (~spec_mem_en && spec_has_pmp_err && spec_post_mtval == `LSU.addr_last_d)) &&
|
||||
~mem_gnt_fst_q && ~spec_mem_en_snd && ~`LSU.lsu_err_q && addr_last_d_matches
|
||||
)
|
||||
inv fst_req_2 (
|
||||
(data_req_o -> (mem_req_fst_d && fst_mem_cmp)) &&
|
||||
(~data_req_o -> (~spec_mem_en_snd && spec_has_pmp_err && spec_post_mtval == `LSU.addr_last_d)) &&
|
||||
~mem_gnt_fst_q && ~`LSU.lsu_err_q &&
|
||||
`LSU.split_misaligned_access && addr_last_d_matches
|
||||
)
|
||||
inv snd_req_1 (
|
||||
((`LSU.pmp_err_q && `LSU.data_pmp_err_i) -> (~spec_mem_en & ~mem_gnt_fst_q && ~spec_mem_en_snd && spec_has_pmp_err)) &&
|
||||
((`LSU.pmp_err_q && data_req_o) -> (mem_req_fst_d && fst_mem_cmp && ~spec_mem_en_snd && spec_has_pmp_err)) &&
|
||||
((~`LSU.pmp_err_q && `LSU.data_pmp_err_i) -> (mem_gnt_fst_q && ~spec_mem_en_snd && spec_has_pmp_err)) &&
|
||||
((~`LSU.pmp_err_q && data_req_o) -> (mem_req_snd_d && snd_mem_cmp && ~spec_has_pmp_err)) &&
|
||||
`LSU.split_misaligned_access && addr_last_matches &&
|
||||
(`LSU.pmp_err_q -> (spec_post_mtval == `LSU.addr_last_q)) &&
|
||||
((~`LSU.pmp_err_q && `LSU.data_pmp_err_i) -> (spec_post_mtval == `LSU.addr_last_d))
|
||||
)
|
||||
inv snd_req_2 (
|
||||
((`LSU.lsu_err_q && `LSU.pmp_err_q) -> (~spec_mem_en & ~mem_gnt_fst_q && ~spec_mem_en_snd && spec_has_pmp_err)) &&
|
||||
((`LSU.lsu_err_q && data_req_o) -> (mem_req_fst_d && fst_mem_cmp && ~spec_mem_en_snd && spec_has_pmp_err)) &&
|
||||
((~`LSU.lsu_err_q && `LSU.pmp_err_q) -> (mem_gnt_fst_q && ~spec_mem_en_snd && spec_has_pmp_err)) &&
|
||||
((~`LSU.lsu_err_q && data_req_o) -> (mem_req_snd_d && snd_mem_cmp && ~spec_has_pmp_err)) &&
|
||||
((~`LSU.lsu_err_q && ex_is_load_instr) -> (`LSU.rdata_q == spec_mem_read_fst_rdata[31:8])) &&
|
||||
`LSU.split_misaligned_access && addr_last_matches &&
|
||||
(`LSU.lsu_err_q -> (spec_post_mtval == `LSU.addr_last_q)) &&
|
||||
((~`LSU.lsu_err_q && `LSU.pmp_err_q) -> (spec_post_mtval == `LSU.addr_last_d))
|
||||
)
|
||||
inv req_done (
|
||||
~data_req_o && mem_gnt_snd_q && ~spec_has_pmp_err && spec_mem_en && spec_mem_en_snd &&
|
||||
~`LSU.lsu_err_q && ~`LSU.pmp_err_q && addr_last_matches
|
||||
)
|
||||
|
||||
entry (`LSU.ls_fsm_cs == `LSU.IDLE && `CR.lsu_req) -> idle_active
|
||||
|
||||
node idle_active fst_req (`LSU.ls_fsm_cs == `LSU.IDLE && `CR.lsu_req)
|
||||
edge idle_active => wait_rvalid_mis wait_gnt_mis wait_gnt
|
||||
edge idle_active -> step
|
||||
|
||||
node wait_gnt_mis fst_req_2 (`LSU.ls_fsm_cs == `LSU.WAIT_GNT_MIS)
|
||||
edge wait_gnt_mis => wait_gnt_mis wait_rvalid_mis
|
||||
|
||||
node wait_rvalid_mis snd_req_1 (`LSU.ls_fsm_cs == `LSU.WAIT_RVALID_MIS)
|
||||
edge wait_rvalid_mis => wait_rvalid_mis wait_rvalid_mis_gnts_done wait_gnt_split
|
||||
edge wait_rvalid_mis -> step
|
||||
|
||||
node wait_gnt_split snd_req_2 (`LSU.ls_fsm_cs == `LSU.WAIT_GNT && `LSU.split_misaligned_access)
|
||||
edge wait_gnt_split => wait_gnt_split
|
||||
edge wait_gnt_split -> step
|
||||
|
||||
node wait_gnt fst_req_1 (`LSU.ls_fsm_cs == `LSU.WAIT_GNT && ~`LSU.split_misaligned_access)
|
||||
edge wait_gnt => wait_gnt
|
||||
edge wait_gnt -> step
|
||||
|
||||
node wait_rvalid_mis_gnts_done req_done (`LSU.ls_fsm_cs == `LSU.WAIT_RVALID_MIS_GNTS_DONE)
|
||||
edge wait_rvalid_mis_gnts_done => wait_rvalid_mis_gnts_done
|
||||
edge wait_rvalid_mis_gnts_done -> step
|
||||
|
||||
node step (1) (`LSU.lsu_req_done_o) +exit
|
||||
/
|
||||
LSULateRespFinishing: have (late_resp |-> wbexc_finishing || wbexc_err)
|
||||
LSUEarlyRequestSplit: have (early_resp |-> has_snd_req)
|
||||
LSUHold: have (data_req_o & ~data_gnt_i |=> data_addr_o == $past(data_addr_o) && data_we_o == $past(data_we_o))
|
||||
LSUHoldWrite: have (data_req_o & ~data_gnt_i & data_we_o |=> data_be_o == $past(data_be_o) && data_wdata_o == $past(data_wdata_o))
|
||||
LSUMaxTwoReqs: have (mem_gnt_snd_q |-> ~data_gnt_i)
|
||||
LSU2ndReqStep: have (data_req_o & $past(data_gnt_i) & ~$past(instr_will_progress) |-> data_we_o == $past(data_we_o) && data_addr_o == $past(data_addr_o) + 4)
|
||||
LSUInternalHold: have (`LSU.data_req_o && ~data_gnt_i && ~`LSU.pmp_err_q |=> $stable(data_addr_o))
|
||||
|
||||
NoMem: have (~ex_is_pres_mem_instr & instr_will_progress |-> ~mem_gnt_fst_d) # Top level property! Non memory instructions don't do memory requests!
|
||||
|
||||
PMPErrMatch: have (ex_is_pres_mem_instr & instr_will_progress & ~`CR.illegal_insn_id & ~`CR.instr_fetch_err |-> spec_has_pmp_err == (`LSU.lsu_err_d | `LSU.pmp_err_d))
|
||||
|
||||
PCMaintainEx1: have (`ID.instr_valid_i & ex_is_pres_mem_instr & ~ex_err & ~ex_kill |-> pre_nextpc == post_pc)
|
||||
PCMaintainEx2: have (`ID.instr_valid_i & ex_is_pres_mem_instr & ~ex_err & ~ex_kill & ~spec_has_pmp_err |-> pre_nextpc == spec_post_pc)
|
||||
CSRMaintainEx: have (`ID.instr_valid_i & ex_is_pres_mem_instr & ~ex_err & ~ex_kill & ~spec_has_pmp_err |-> ex_csrs_match)
|
||||
ExcCSRMaintainEx: have (`ID.instr_valid_i & ex_is_pres_mem_instr & ~ex_err & ~ex_kill & spec_has_pmp_err |-> ex_csrs_match_non_exc)
|
||||
AltLSUVeryEarly: have (`LSU.ls_fsm_cs != `LSU.IDLE & spec_post_wX_en & ~lsu_had_first_resp |-> spec_post_wX == alt_lsu_very_early_res)
|
||||
/
|
||||
PCNoChangeNoBranch: have (wbexc_exists & wbexc_is_pres_mem_instr & ~wbexc_err & ~ex_has_branched_d |-> (`ID.instr_valid_i ? pre_pc : `CR.pc_if) == wbexc_dut_post_pc)
|
||||
AltLSUEarly: have (`LSU.ls_fsm_cs != `LSU.IDLE & spec_post_wX_en & lsu_had_first_resp |-> spec_post_wX == alt_lsu_early_res)
|
||||
/
|
||||
AltLSU: have (wbexc_exists & wbexc_is_pres_load_instr & ~wbexc_err & wbexc_post_wX_en |-> wbexc_post_wX == alt_lsu_late_res)
|
||||
PCNoChangeBranch: have (wbexc_exists & wbexc_is_pres_mem_instr & ~wbexc_err & ex_has_branched_d |-> pre_pc == wbexc_dut_post_pc)
|
||||
PCExc: have (wbexc_exists & wbexc_is_pres_mem_instr & `LSU.data_or_pmp_err |-> wbexc_post_pc == { `IF.csr_mtvec_i[31:8], 8'h00 })
|
||||
|
||||
CSRMaintain: have (wbexc_exists & wbexc_is_pres_mem_instr & ~wbexc_err & ~`LSU.data_or_pmp_err |-> csrs_match)
|
||||
CSRNoChange: have (wbexc_exists & wbexc_is_pres_mem_instr & ~wbexc_err |-> csrs_didnt_change)
|
||||
PCMaintainWb: have (wbexc_exists & wbexc_is_pres_mem_instr & ~wbexc_err & ~`LSU.data_or_pmp_err |-> wbexc_post_pc == wbexc_dut_post_pc)
|
||||
LoadAddrMaintain: have (wbexc_exists & wbexc_is_pres_load_instr & ~wbexc_err & ~`LSU.data_or_pmp_err |-> wbexc_post_wX_en && `WBG.rf_waddr_wb_q == wbexc_post_wX_addr && ~`WBG.rf_we_wb_q)
|
||||
StoreAddrMaintain: have (wbexc_exists & wbexc_is_pres_store_instr & ~wbexc_err |-> ~wbexc_post_wX_en && ~`WBG.rf_we_wb_q)
|
||||
ExcAddrMaintain: have (wbexc_exists & wbexc_is_pres_mem_instr & `LSU.data_or_pmp_err |-> ~wbexc_post_wX_en)
|
||||
|
||||
ExcCSRMaintainMCause: have (wbexc_exists & wbexc_is_pres_mem_instr & `LSU.data_or_pmp_err & ~wbexc_fetch_err & ~wbexc_illegal |-> wbexc_post_mcause == (wbexc_is_store_instr ? ExcCauseStoreAccessFault : ExcCauseLoadAccessFault))
|
||||
ExcCSRMaintainMTVal: have (wbexc_exists & wbexc_is_pres_mem_instr & `LSU.data_or_pmp_err & ~wbexc_fetch_err & ~wbexc_illegal |-> wbexc_post_mtval == `LSU.addr_last_o)
|
||||
ExcCSRMaintainMStatus: have (wbexc_exists & wbexc_is_pres_mem_instr & `LSU.data_or_pmp_err & ~wbexc_fetch_err & ~wbexc_illegal |->
|
||||
wbexc_post_mstatus.mie == 1'b0 &&
|
||||
wbexc_post_mstatus.mpie == pre_mstatus.mie &&
|
||||
wbexc_post_mstatus.mpp == (pre_priv == Machine ? PRIV_LVL_M : PRIV_LVL_U)
|
||||
)
|
||||
ExcCSRMaintainMepc: have (wbexc_exists & wbexc_is_pres_mem_instr & `LSU.data_or_pmp_err & ~wbexc_fetch_err & ~wbexc_illegal |-> wbexc_post_mepc == `CR.pc_wb)
|
||||
ExcCSRMaintainPriv: have (wbexc_exists & wbexc_is_pres_mem_instr & `LSU.data_or_pmp_err & ~wbexc_fetch_err & ~wbexc_illegal |-> wbexc_post_priv == Machine)
|
||||
ExcCSRMaintainRest: have (wbexc_exists & wbexc_is_pres_mem_instr & `LSU.data_or_pmp_err & ~wbexc_fetch_err & ~wbexc_illegal |-> csrs_match_non_exc)
|
||||
|
||||
# Top level load properties
|
||||
lemma load
|
||||
cond (ex_is_pres_load_instr)
|
||||
|
||||
NoWe: have (spec_mem_read |-> ~data_we_o)
|
||||
En: have (data_req_o |-> spec_mem_read)
|
||||
/
|
||||
SndEn: have (mem_req_snd_d |-> spec_mem_read_snd)
|
||||
/ # Fixme: Is all of this sequencing actually necessary?
|
||||
FstAddr: have (mem_req_fst_d |-> spec_mem_read_fst_addr == data_addr_o)
|
||||
SndAddr: have (mem_req_snd_d |-> spec_mem_read_snd_addr == data_addr_o)
|
||||
/
|
||||
End: in (instr_will_progress)
|
||||
Fst: have (spec_mem_read |-> mem_gnt_fst_d)
|
||||
Snd: have (spec_mem_read_snd |-> mem_gnt_snd_d)
|
||||
|
||||
# Top level store properties
|
||||
lemma store
|
||||
cond (ex_is_pres_store_instr)
|
||||
|
||||
We: have (spec_mem_write |-> data_we_o)
|
||||
En: have (data_req_o |-> spec_mem_write)
|
||||
/
|
||||
SndEn: have (mem_req_snd_d |-> spec_mem_write_snd)
|
||||
/
|
||||
FstAddr: have (mem_req_fst_d |-> spec_mem_write_fst_addr == data_addr_o)
|
||||
FstWData: have (mem_req_fst_d |-> (spec_mem_write_fst_wdata & fst_mask) == (data_wdata_o & fst_mask))
|
||||
SndAddr: have (mem_req_snd_d |-> spec_mem_write_snd_addr == data_addr_o)
|
||||
SndWData: have (mem_req_snd_d |-> (spec_mem_write_snd_wdata & snd_mask) == (data_wdata_o & snd_mask))
|
||||
/
|
||||
End: in (instr_will_progress)
|
||||
Fst: have (spec_mem_write |-> mem_gnt_fst_d)
|
||||
Snd: have (spec_mem_write_snd |-> mem_gnt_snd_d)
|
||||
194
dv/formal/thm/riscv.proof
Normal file
194
dv/formal/thm/riscv.proof
Normal file
|
|
@ -0,0 +1,194 @@
|
|||
# Copyright lowRISC contributors.
|
||||
# Copyright 2024 University of Oxford, see also CREDITS.md.
|
||||
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
|
||||
# Original author: Louis-Emile Ploix
|
||||
# SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
# This is the 'entry point' of the proofs, it invokes all the other proofs in thm/
|
||||
|
||||
def csr_split
|
||||
each X Priv:(priv) Mstatus:(mstatus) Mie:(mie) Mcause:(mcause) Mtval:(mtval) Mtvec:(mtvec) \
|
||||
Mscratch:(mscratch) Mepc:(mepc) Mcounteren:(mcounteren) \
|
||||
Pmp_cfg:(pmp_cfg) Pmp_addr:(pmp_addr) Mseccfg:(mseccfg)
|
||||
have (wbexc_dut_cmp_post_``X == wbexc_spec_cmp_post_``X)
|
||||
|
||||
def spec_compliant_raw_csr_split
|
||||
Addr: have (addr_match)
|
||||
Data: have (data_match)
|
||||
PC: have (pc_match)
|
||||
use csr_split
|
||||
|
||||
def spec_compliant_raw
|
||||
Addr: have (addr_match)
|
||||
Data: have (data_match)
|
||||
CSR: have (csrs_match)
|
||||
PC: have (pc_match)
|
||||
|
||||
def spec_compliant
|
||||
cond (finishing_executed & ~wbexc_illegal)
|
||||
use spec_compliant_raw
|
||||
|
||||
def spec_compliant_no_err
|
||||
cond (finishing_executed & ~wbexc_illegal)
|
||||
NoErr: have (~wbexc_err)
|
||||
/
|
||||
use spec_compliant_raw
|
||||
|
||||
def structure_fast
|
||||
cond (finishing_executed & ~wbexc_illegal)
|
||||
Fast: have ($past(instr_will_progress))
|
||||
|
||||
def structure_fast_err
|
||||
cond (finishing_executed & ~wbexc_illegal & wbexc_err)
|
||||
Fast: have ($past(instr_will_progress))
|
||||
|
||||
lemma riscv
|
||||
Ibex: lemma ibex
|
||||
/
|
||||
|
||||
Arith:
|
||||
in I:(`ISS_ADDI | `ISS_SLTI | `ISS_SLTIU | `ISS_XORI | `ISS_ORI | `ISS_ANDI) \
|
||||
R:(`ISS_ADD | `ISS_SUB | `ISS_SLL | `ISS_SLT | `ISS_SLTU | `ISS_XOR | `ISS_SRL | `ISS_SRA | `ISS_OR | `ISS_AND) \
|
||||
Shift:(`ISS_SHIFTIOP)
|
||||
use structure_fast
|
||||
/
|
||||
use spec_compliant_no_err
|
||||
|
||||
# Never actually proved, just assumed to be true instead.
|
||||
MType:
|
||||
in Mul:(`ISS_MUL) MulH:(`ISS_MULH) MulHSH:(`ISS_MULHSH) MulHU:(`ISS_MULHU) Div:(`ISS_DIV) DivU:(`ISS_DIVU) Rem:(`ISS_REM) RemU:(`ISS_REMU)
|
||||
use spec_compliant_no_err
|
||||
|
||||
CSR:
|
||||
in (`ISS_CSR & wbexc_is_checkable_csr)
|
||||
use structure_fast
|
||||
/
|
||||
use spec_compliant
|
||||
split_bool Err:(wbexc_err)
|
||||
|
||||
BType:
|
||||
in (`ISS_BTYPE)
|
||||
lemma btype
|
||||
use structure_fast
|
||||
/
|
||||
use spec_compliant
|
||||
|
||||
JType: block
|
||||
lemma jump
|
||||
/
|
||||
in Jal:(`ISS_JAL) Jalr:(`ISS_JALR)
|
||||
use structure_fast
|
||||
/
|
||||
use spec_compliant
|
||||
|
||||
UType:
|
||||
in Lui:(`ISS_LUI) Auipc:(`ISS_AUIPC)
|
||||
use structure_fast
|
||||
/
|
||||
use spec_compliant
|
||||
|
||||
Fence:
|
||||
in Fence:(`ISS_FENCE) FenceI:(`ISS_FENCEI)
|
||||
use structure_fast
|
||||
/
|
||||
use spec_compliant
|
||||
|
||||
Special:
|
||||
in ECall:(`ISS_ECALL) EBreak:(`ISS_EBREAK) MRet:(`ISS_MRET)
|
||||
use structure_fast
|
||||
/
|
||||
use spec_compliant
|
||||
|
||||
WFI:
|
||||
in (`ISS_WFI && finishing_executed && ~wbexc_illegal)
|
||||
use structure_fast
|
||||
/
|
||||
use spec_compliant_raw
|
||||
split_bool Err:(wbexc_err)
|
||||
|
||||
Mem: block
|
||||
lemma mem
|
||||
/
|
||||
Load: lemma load
|
||||
Store: lemma store
|
||||
/
|
||||
in L:(wbexc_is_pres_load_instr) S:(wbexc_is_pres_store_instr)
|
||||
use spec_compliant
|
||||
split_bool Err:(wbexc_err)
|
||||
|
||||
IRQ: in (wbexc_handling_irq)
|
||||
PC: have (pc_match)
|
||||
CSR: have (csrs_match)
|
||||
|
||||
Illegal: in (wbexc_illegal & can_check_illegal & wbexc_finishing & ~wbexc_fetch_err & (`ISS_CSR -> wbexc_is_checkable_csr))
|
||||
Fast: have ($past(instr_will_progress))
|
||||
/
|
||||
use spec_compliant_raw
|
||||
|
||||
FetchErr: in (wbexc_finishing & wbexc_fetch_err)
|
||||
Fast: have ($past(instr_will_progress))
|
||||
/
|
||||
use spec_compliant_raw
|
||||
|
||||
/
|
||||
|
||||
# Uncomment this for liveness proofs, see ibex.proof for a description of when this can be done.
|
||||
# Liveness: lemma live
|
||||
|
||||
Top: in (wbexc_finishing & (`ISS_CSR -> wbexc_is_checkable_csr))
|
||||
use spec_compliant_raw
|
||||
|
||||
/
|
||||
|
||||
RegMatch:
|
||||
each i 1:(1) 2:(2) 3:(3) 4:(4) 5:(5) 6:(6) 7:(7) 8:(8) 9:(9) 10:(10) 11:(11) 12:(12) 13:(13) 14:(14) \
|
||||
15:(15) 16:(16) 17:(17) 18:(18) 19:(19) 20:(20) 21:(21) 22:(22) 23:(23) 24:(24) 25:(25) 26:(26) \
|
||||
27:(27) 28:(28) 29:(29) 30:(30) 31:(31)
|
||||
have ((~`CR.rf_write_wb || `CR.rf_waddr_wb != i) & spec_past_has_reg[i] |-> pre_regs[i] == spec_past_regs[i])
|
||||
|
||||
SpecPastNoWbexc:
|
||||
in (has_spec_past & ~wbexc_exists)
|
||||
each X Priv:(priv) Mstatus:(mstatus) Mie:(mie) Mcause:(mcause) Mtval:(mtval) Mtvec:(mtvec) \
|
||||
Mscratch:(mscratch) Mepc:(mepc) Mcounteren:(mcounteren) \
|
||||
Pmp_cfg:(pmp_cfg) Pmp_addr:(pmp_addr) Mseccfg:(mseccfg)
|
||||
have (spec_past_``X == pre_``X)
|
||||
|
||||
SleepSpecPastPC: have (has_spec_past & (`IDC.ctrl_fsm_cs == `IDC.WAIT_SLEEP || `IDC.ctrl_fsm_cs == `IDC.SLEEP) |-> spec_past_pc == `CR.pc_if)
|
||||
|
||||
/
|
||||
|
||||
# If you find a visualize SST trace for this property of length 5, you will be told none exists.
|
||||
# If you find an SST trace via prove -sst, one will be found, but upon visualizing it JG will report that an
|
||||
# assumption was violated. This leads me to believe that this property is provable by 5-induction, but JG has
|
||||
# a bug preventing it from seeing so. It proves instead via engine D.
|
||||
SpecPastNoWbexcPC: have (has_spec_past & ~wbexc_exists |-> spec_past_pc == (`ID.instr_valid_i ? pre_pc : `CR.pc_if))
|
||||
/
|
||||
|
||||
# Prove these with engine D (apart from Live which needs Oh)
|
||||
Wrap: in (spec_en)
|
||||
each X Priv:(priv) Mstatus:(mstatus) Mie:(mie) Mcause:(mcause) Mtval:(mtval) Mtvec:(mtvec) \
|
||||
Mscratch:(mscratch) Mepc:(mepc) Mcounteren:(mcounteren) \
|
||||
Pmp_cfg:(pmp_cfg) Pmp_addr:(pmp_addr) Mseccfg:(mseccfg) \
|
||||
Pc:(pc)
|
||||
have (has_spec_past |-> pre_``X == spec_past_``X)
|
||||
|
||||
RegA: have (spec_rx_a_en && (spec_rx_a_addr != 0) && spec_past_has_reg[spec_rx_a_addr] |-> spec_rx_a == spec_past_regs[spec_rx_a_addr])
|
||||
RegB: have (spec_rx_b_en && (spec_rx_b_addr != 0) && spec_past_has_reg[spec_rx_b_addr] |-> spec_rx_b == spec_past_regs[spec_rx_b_addr])
|
||||
|
||||
# Live: have (always (##[1:157 + 2*`WFI_BOUND + 17*`TIME_LIMIT] spec_en))
|
||||
|
||||
Mem:
|
||||
block
|
||||
En: have (data_req_o |-> spec_mem_en)
|
||||
SndEn: have (mem_req_snd_d |-> spec_mem_en_snd)
|
||||
|
||||
We: have (data_req_o |-> data_we_o == spec_mem_write && data_we_o == ~spec_mem_read)
|
||||
|
||||
FstAddr: have (mem_req_fst_d |-> spec_mem_fst_addr == data_addr_o)
|
||||
SndAddr: have (mem_req_snd_d |-> spec_mem_snd_addr == data_addr_o)
|
||||
|
||||
FstWData: have (mem_req_fst_d & data_we_o |-> (spec_mem_write_fst_wdata & fst_mask) == (data_wdata_o & fst_mask))
|
||||
SndWData: have (mem_req_snd_d & data_we_o |-> (spec_mem_write_snd_wdata & snd_mask) == (data_wdata_o & snd_mask))
|
||||
|
||||
FstEnd: have (spec_en & spec_mem_en |-> mem_gnt_fst_d)
|
||||
SndEnd: have (spec_en & spec_mem_en_snd |-> mem_gnt_snd_d)
|
||||
271
dv/formal/verify.tcl
Normal file
271
dv/formal/verify.tcl
Normal file
|
|
@ -0,0 +1,271 @@
|
|||
# Copyright lowRISC contributors.
|
||||
# Copyright 2024 University of Oxford, see also CREDITS.md.
|
||||
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
|
||||
# The underlying commands and reports of this script are copyrighted by Cadence.
|
||||
# We thank Cadence for granting permission to share our research to help
|
||||
# promote and foster the next generation of innovators.
|
||||
# Original author: Louis-Emile Ploix
|
||||
# SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
set_prove_cache_path jgproofs
|
||||
set_prove_cache on
|
||||
set_prove_cache_mode coi
|
||||
|
||||
set_prove_per_property_time_limit 10s
|
||||
|
||||
set ibex_root ../../
|
||||
set sail_lib_dir $env(SAIL_DIR)/lib/sv
|
||||
set prim $ibex_root/vendor/lowrisc_ip/ip/prim/rtl/
|
||||
set dv $ibex_root/vendor/lowrisc_ip/dv/sv/dv_utils/
|
||||
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_pkg.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_alu.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_compressed_decoder.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_controller.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_cs_registers.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_decoder.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_ex_block.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_id_stage.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_if_stage.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_wb_stage.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_load_store_unit.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_multdiv_slow.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_counter.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_multdiv_fast.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_prefetch_buffer.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_fetch_fifo.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_pmp.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_core.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_csr.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_register_file_ff.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_pkg.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/vendor/lowrisc_ip/ip/prim/rtl/prim_assert.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/vendor/lowrisc_ip/ip/prim/rtl/prim_ram_1p_pkg.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_generic_buf.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_generic_clock_gating.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/dv/uvm/core_ibex/common/prim/prim_buf.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/dv/uvm/core_ibex/common/prim/prim_pkg.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/dv/uvm/core_ibex/common/prim/prim_clock_gating.sv
|
||||
analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_top.sv
|
||||
|
||||
analyze -sv12 -incdir $sail_lib_dir build/ibexspec.sv
|
||||
analyze -sv12 spec/stub.sv
|
||||
|
||||
analyze -sv12 spec/spec_api.sv
|
||||
|
||||
# analyze -sv12 bound/binder.sv
|
||||
# analyze -sv12 bound/if.sv
|
||||
analyze -sv12 check/peek/alt_lsu.sv
|
||||
|
||||
analyze -sv12 check/top.sv
|
||||
|
||||
elaborate -top top -disable_auto_bbox
|
||||
clock clk_i
|
||||
reset ~rst_ni
|
||||
|
||||
set_proofgrid_max_local_jobs 10
|
||||
set_proofgrid_per_engine_max_local_jobs 8
|
||||
|
||||
# AMcustom1
|
||||
custom_engine -add -code hT3N1rhP11/52HrFRS21ROp2LOjVTgPvT8L8BGXHgLhaIuqtT4nARFjUqrBL+7pLmaTOzBepZW/Jm8SSrHDybSQtoNiO3y43wk+dEoWlsZizu97Fih6O6lPVG/LpWP5SsUPwlGagLNa1FKEFvwVXyX7//8prySbvSxIHXr5er+z4RAEA
|
||||
|
||||
# AMcustom2
|
||||
custom_engine -add -code hT3Ng7hP/feYQOTDZ3qhYOwGAM51eA+J/FjkM5shLioAsqhgLR4Ft+O1BuKG6ilQ83B9tLXSmmqwm7g9AQA
|
||||
|
||||
# Ncustom3
|
||||
custom_engine -add -code hT3OXrhPByJp3TrFSTLhUmMH4KVtJgmTCnNDF46yMXOKY48m4LS5nE7yBzFjA7kDuwO/GhGUpEPiky3p3wmPn3dJZHxFMsafSoObRzSC+tn7sEY0WbTdZ/FV4hL3MYH/b1CIUvXSWR4wqEoVLsmMOD4xIPT4lI1LO6ZCO7PnnWQuLwetnvKlrXx6wCW/A+x+enqslg1YPobi4wEF/EvbzOvcTYdJvl2s4H2yZg2b2ofAVN5WvhWk1HoBAA
|
||||
|
||||
# ADcustom4
|
||||
custom_engine -add -code hT3Nv7hPv1752HrFRa2kROx2f/ECJeZB2AZsLdlO8VwmIuqtT4nIDFXclhg+O+o+DMmQCekbheGk0kK28laA9gaOFDXsQp29J3X615HY1IPHJWd6FUFvCHjO+p1k652b5JJvZlShNpGlGSXAiQe/mEAj6tEBAA
|
||||
|
||||
# Ncustom5
|
||||
custom_engine -add -code hT3Ng7hPPfiYQOTDZ3qhYOwGAM51eA+J/FjkM5shLioAsqhgLR4Ft+O1BuKG6ilQ83B9tLXSl+CwjiTMAQA
|
||||
|
||||
# Mpcustom6
|
||||
custom_engine -add -code hT3NZbhP9fmY2AbBQnsjfOxn6c+6e6yL+/e8fZFmaQrnlgEA
|
||||
|
||||
# prove -bg -all -covers
|
||||
|
||||
proc enter_stopat {} {
|
||||
stopat -reset {*}
|
||||
}
|
||||
|
||||
proc exit_stopat {} {
|
||||
stopat -reset -clear
|
||||
}
|
||||
|
||||
proc assume_mtypes {} {
|
||||
assume -from_assert {Step10::top.MType_*_Data}
|
||||
}
|
||||
|
||||
proc prove_lemmas {} {
|
||||
assume_mtypes
|
||||
|
||||
prove -task Step0
|
||||
report -task Step0
|
||||
|
||||
prove -task Step1
|
||||
report -task Step1
|
||||
|
||||
prove -task Step2
|
||||
report -task Step2
|
||||
|
||||
prove -task Step3
|
||||
report -task Step3
|
||||
|
||||
prove -task Step4
|
||||
report -task Step4
|
||||
|
||||
prove -task Step5
|
||||
report -task Step5
|
||||
|
||||
prove -property Step6::top.Ibex_FetchErrRoot
|
||||
prove -property {Step6::top.Ibex_SpecStableLoad Step6::top.Ibex_SpecStableLoadSnd Step6::top.Ibex_SpecStableLoadAddr Step6::top.Ibex_SpecStableLoadSndAddr Step6::top.Ibex_SpecStableStore Step6::top.Ibex_SpecStableStoreSnd Step6::top.Ibex_SpecStableStoreAddr Step6::top.Ibex_SpecStableStoreSndAddr Step6::top.Ibex_SpecStableStoreData Step6::top.Ibex_SpecStableStoreSndData} -engine_mode Hp
|
||||
prove -task Step6
|
||||
report -task Step6
|
||||
|
||||
prove -task Step7
|
||||
report -task Step7
|
||||
|
||||
prove -task Step8
|
||||
report -task Step8
|
||||
|
||||
prove -property {Step9::top.Arith_I_Fast Step9::top.Arith_R_Fast Step9::top.Arith_Shift_Fast Step9::top.CSR_Fast Step9::top.BType_FinishFirstCycle Step9::top.BType_Fast Step9::top.JType_FinishFirstCycle Step9::top.UType_Lui_Fast Step9::top.UType_Auipc_Fast Step9::top.Fence_Fence_Fast Step9::top.Fence_FenceI_Fast Step9::top.Special_ECall_Fast Step9::top.Special_EBreak_Fast Step9::top.Special_MRet_Fast Step9::top.WFI_Fast}
|
||||
prove -property {Step9::top.Mem_MemSpec_Initial Step9::top.Mem_MemSpec_Initial_IdleActive Step9::top.Mem_MemSpec_WaitRvalidMis_Step Step9::top.Mem_MemSpec_WaitRvalidMis_WaitRvalidMis_Inv Step9::top.Mem_MemSpec_WaitRvalidMis_WaitRvalidMisGntsDone_Inv Step9::top.Mem_MemSpec_WaitRvalidMis_WaitGntSplit_Inv Step9::top.Mem_MemSpec_WaitRvalidMis_Step_Inv Step9::top.Mem_MemSpec_WaitGntSplit_Step Step9::top.Mem_MemSpec_WaitGntSplit_WaitGntSplit_Inv Step9::top.Mem_MemSpec_WaitGntSplit_Step_Inv Step9::top.Mem_MemSpec_WaitGnt_Step Step9::top.Mem_MemSpec_WaitGnt_WaitGnt_Inv Step9::top.Mem_MemSpec_WaitGnt_Step_Inv Step9::top.Mem_MemSpec_WaitRvalidMisGntsDone_Step Step9::top.Mem_MemSpec_WaitRvalidMisGntsDone_WaitRvalidMisGntsDone_Inv Step9::top.Mem_MemSpec_WaitRvalidMisGntsDone_Step_Inv Step9::top.Mem_MemSpec_IdleActive_Step Step9::top.Mem_MemSpec_IdleActive_WaitRvalidMis_Inv Step9::top.Mem_MemSpec_IdleActive_WaitGntMis_Inv Step9::top.Mem_MemSpec_IdleActive_WaitGnt_Inv Step9::top.Mem_MemSpec_IdleActive_Step_Inv Step9::top.Mem_MemSpec_WaitGntMis_Step Step9::top.Mem_MemSpec_WaitGntMis_WaitGntMis_Inv Step9::top.Mem_MemSpec_WaitGntMis_WaitRvalidMis_Inv}
|
||||
prove -property {Step9::top.IRQ_PC Step9::top.IRQ_CSR}
|
||||
prove -property {Step9::top.Illegal_Fast Step9::top.FetchErr_Fast}
|
||||
prove -task Step9
|
||||
report -task Step9
|
||||
|
||||
prove -property {Step10::top.Arith_I_NoErr Step10::top.Arith_R_NoErr Step10::top.Arith_Shift_NoErr Step10::top.CSR_Addr_NotErr Step10::top.CSR_Data_NotErr Step10::top.CSR_CSR_NotErr Step10::top.CSR_PC_NotErr Step10::top.CSR_Addr_Err Step10::top.CSR_Data_Err Step10::top.CSR_CSR_Err Step10::top.CSR_PC_Err}
|
||||
prove -property {Step10::top.BType_BInd_Initial Step10::top.BType_BInd_Initial_Stall Step10::top.BType_BInd_Initial_Oma Step10::top.BType_BInd_Initial_Progress Step10::top.BType_BInd_Stall_Step Step10::top.BType_BInd_Stall_Stall_Inv Step10::top.BType_BInd_Stall_Progress_Inv Step10::top.BType_BInd_Oma_Step_0 Step10::top.BType_BInd_Oma_Oma_Inv_0 Step10::top.BType_BInd_Oma_Progress_Inv_0 Step10::top.BType_BInd_Oma_Step_1 Step10::top.BType_BInd_Oma_Oma_Inv_1 Step10::top.BType_BInd_Oma_Progress_Inv_1}
|
||||
prove -property {Step10::top.JType_JInd_Initial Step10::top.JType_JInd_Initial_Stall Step10::top.JType_JInd_Initial_Oma Step10::top.JType_JInd_Initial_Progress Step10::top.JType_JInd_Stall_Step Step10::top.JType_JInd_Stall_Stall_Inv Step10::top.JType_JInd_Stall_Progress_Inv Step10::top.JType_JInd_Oma_Step Step10::top.JType_JInd_Oma_Oma_Inv Step10::top.JType_JInd_Oma_Progress_Inv}
|
||||
prove -property {Step10::top.UType_Lui_Addr Step10::top.UType_Lui_Data Step10::top.UType_Lui_CSR Step10::top.UType_Lui_PC Step10::top.UType_Auipc_Addr Step10::top.UType_Auipc_Data Step10::top.UType_Auipc_CSR Step10::top.UType_Auipc_PC}
|
||||
prove -property {Step10::top.Fence_Fence_Addr Step10::top.Fence_Fence_Data Step10::top.Fence_Fence_CSR Step10::top.Fence_Fence_PC Step10::top.Fence_FenceI_Addr Step10::top.Fence_FenceI_Data Step10::top.Fence_FenceI_CSR Step10::top.Fence_FenceI_PC}
|
||||
prove -property {Step10::top.Special_ECall_Addr Step10::top.Special_ECall_Data Step10::top.Special_ECall_CSR Step10::top.Special_ECall_PC Step10::top.Special_EBreak_Addr Step10::top.Special_EBreak_Data Step10::top.Special_EBreak_CSR Step10::top.Special_EBreak_PC Step10::top.Special_MRet_Addr Step10::top.Special_MRet_Data Step10::top.Special_MRet_CSR Step10::top.Special_MRet_PC}
|
||||
prove -property {Step10::top.WFI_Addr_NotErr Step10::top.WFI_Data_NotErr Step10::top.WFI_PC_NotErr Step10::top.WFI_CSR_NotErr}
|
||||
prove -property {Step10::top.WFI_Addr_Err Step10::top.WFI_Data_Err Step10::top.WFI_PC_Err Step10::top.WFI_CSR_Err}
|
||||
prove -property {Step10::top.Mem_MemSpec_IdleActive_Rev Step10::top.Mem_MemSpec_WaitGntMis_Rev Step10::top.Mem_MemSpec_WaitRvalidMis_Rev Step10::top.Mem_MemSpec_WaitGntSplit_Rev Step10::top.Mem_MemSpec_WaitGnt_Rev Step10::top.Mem_MemSpec_WaitRvalidMisGntsDone_Rev Step10::top.Mem_MemSpec_Step_Rev}
|
||||
prove -property {Step10::top.Illegal_Addr Step10::top.Illegal_Data Step10::top.Illegal_PC Step10::top.Illegal_CSR}
|
||||
prove -property {Step10::top.FetchErr_Addr Step10::top.FetchErr_Data Step10::top.FetchErr_PC Step10::top.FetchErr_CSR}
|
||||
prove -property {Step10::top.MType_Mul_Addr Step10::top.MType_Mul_CSR Step10::top.MType_Mul_PC Step10::top.MType_MulH_Addr Step10::top.MType_MulH_CSR Step10::top.MType_MulH_PC Step10::top.MType_MulHSH_Addr Step10::top.MType_MulHSH_CSR Step10::top.MType_MulHSH_CSR Step10::top.MType_MulHSH_PC Step10::top.MType_MulHU_Addr Step10::top.MType_MulHU_CSR Step10::top.MType_MulHU_PC}
|
||||
prove -property {Step10::top.MType_Div_Addr Step10::top.MType_Div_CSR Step10::top.MType_Div_PC Step10::top.MType_DivU_Addr Step10::top.MType_DivU_CSR Step10::top.MType_DivU_PC Step10::top.MType_Rem_Addr Step10::top.MType_Rem_CSR Step10::top.MType_Rem_PC Step10::top.MType_RemU_Addr Step10::top.MType_RemU_CSR Step10::top.MType_RemU_PC}
|
||||
prove -task Step10
|
||||
report -task Step10
|
||||
|
||||
prove -property {Step11::top.Arith_I_Addr Step11::top.Arith_I_Data Step11::top.Arith_I_CSR Step11::top.Arith_I_PC}
|
||||
prove -property {Step11::top.Arith_R_Addr Step11::top.Arith_R_Data Step11::top.Arith_R_CSR Step11::top.Arith_R_PC}
|
||||
prove -property {Step11::top.Arith_Shift_Addr Step11::top.Arith_Shift_Data Step11::top.Arith_Shift_CSR Step11::top.Arith_Shift_PC}
|
||||
prove -property {Step11::top.BType_BInd_Stall_Rev Step11::top.BType_BInd_Oma_Rev_0 Step11::top.BType_BInd_Oma_Rev_1 Step11::top.BType_BInd_Progress_Rev Step11::top.JType_JInd_Progress_Rev Step11::top.JType_JInd_Stall_Rev Step11::top.JType_JInd_Oma_Rev}
|
||||
prove -property {Step11::top.Mem_MemSpec_IdleActive Step11::top.Mem_MemSpec_WaitGntMis Step11::top.Mem_MemSpec_WaitRvalidMis Step11::top.Mem_MemSpec_WaitGntSplit Step11::top.Mem_MemSpec_WaitGnt Step11::top.Mem_MemSpec_WaitRvalidMisGntsDone Step11::top.Mem_MemSpec_Step}
|
||||
prove -task Step11
|
||||
report -task Step11
|
||||
|
||||
prove -task Step12
|
||||
report -task Step12
|
||||
|
||||
prove -task Step13
|
||||
report -task Step13
|
||||
|
||||
prove -task Step14
|
||||
report -task Step14
|
||||
|
||||
prove -task Step15
|
||||
report -task Step15
|
||||
|
||||
prove -task Step16
|
||||
report -task Step16
|
||||
|
||||
prove -task Step17
|
||||
report -task Step17
|
||||
|
||||
prove -task Step18
|
||||
report -task Step18
|
||||
|
||||
prove -property {Step19::top.Mem_L_*_Err}
|
||||
prove -property {Step19::top.Mem_L_*_NoErr}
|
||||
prove -property {Step19::top.Mem_L_*}
|
||||
prove -property {Step19::top.Mem_S_*_Err}
|
||||
prove -property {Step19::top.Mem_S_*_NoErr}
|
||||
prove -property {Step19::top.Mem_S_*}
|
||||
prove -task Step19
|
||||
report -task Step19
|
||||
}
|
||||
|
||||
proc prove_no_liveness {} {
|
||||
prove_lemmas
|
||||
|
||||
prove -task Step20
|
||||
report -task Step20
|
||||
|
||||
prove -task Step21 -engine_mode D
|
||||
report -task Step21
|
||||
|
||||
prove -task Step22
|
||||
report -task Step22
|
||||
|
||||
prove -task Step23
|
||||
report -task Step23
|
||||
}
|
||||
|
||||
# TODO fix step numbers in here
|
||||
proc prove_liveness {} {
|
||||
prove_lemmas
|
||||
|
||||
prove -property {Step18::top.Liveness_*}
|
||||
prove -task Step18
|
||||
report -task Step18
|
||||
|
||||
prove -property Step19::top.Liveness_DivStart
|
||||
prove -property Step19::top.Liveness_DivMiddle
|
||||
prove -property Step19::top.Liveness_DivEnd
|
||||
prove -property Step19::top.Liveness_WFIStart
|
||||
prove -property Step19::top.Liveness_WFIMiddle
|
||||
prove -property Step19::top.Liveness_WFIEnd
|
||||
prove -property Step19::top.Liveness_NewProgNormal
|
||||
prove -property Step19::top.Liveness_NewProgMem
|
||||
prove -property Step19::top.Liveness_ProgReadyNormal
|
||||
prove -property Step19::top.Liveness_ProgReadyWFI
|
||||
prove -property Step19::top.Liveness_KillReady
|
||||
prove -property Step19::top.Liveness_ReadyNew
|
||||
prove -property Step19::top.Liveness_Initial
|
||||
prove -property Step19::top.Liveness_FlushedNoKill
|
||||
prove -task Step19
|
||||
report -task Step19
|
||||
|
||||
prove -task Step20
|
||||
report -task Step20
|
||||
|
||||
prove -task Step21
|
||||
report -task Step21
|
||||
|
||||
prove -task Step22
|
||||
report -task Step22
|
||||
|
||||
prove -task Step23
|
||||
report -task Step23
|
||||
|
||||
prove -task Step24
|
||||
report -task Step24
|
||||
|
||||
prove -task Step25
|
||||
report -task Step25
|
||||
|
||||
prove -task Step26
|
||||
report -task Step26
|
||||
|
||||
prove -task Step27
|
||||
report -task Step27
|
||||
|
||||
prove -task Step28
|
||||
report -task Step28
|
||||
|
||||
prove -task Step29
|
||||
report -task Step29
|
||||
|
||||
prove -property Step30::top.Live
|
||||
prove -task Step30 -engine_mode D
|
||||
report -task Step30
|
||||
}
|
||||
|
||||
source build/psgen.tcl
|
||||
Loading…
Add table
Add a link
Reference in a new issue