github-mirrors/ibex
1
0
Fork 0
mirror of https://github.com/lowRISC/ibex.git synced 2025-04-20 11:57:12 -04:00
Code Issues Projects Releases Packages Wiki Activity Actions

Merge d50fe2585a into 594ea976c9

Browse source
This commit is contained in:
Marno van der Maas 2025-04-03 12:10:29 +00:00 • committed by GitHub
commit c3d0503790
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
37 changed files with 4810 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
.github/workflows/pr_lint.yml vendored
View file

@ -36,3 +36,4 @@ jobs:
reviewdog_reporter: github-pr-check
suggest_fixes: "false"
config_file: ${{ env.verible_config }}
extra_args: "--waiver_files lint/verible_waiver.vbw"

5
CREDITS.md
View file

@ -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

3
dv/formal/.gitignore vendored Normal file
View file

@ -0,0 +1,3 @@
build
jgproject
jgproofs

68
dv/formal/Makefile Normal file
View file

@ -0,0 +1,68 @@
IBEX_ROOT=../..
SAIL=sail
SAIL_RISCV_MODEL_DIR=${LOWRISC_SAIL_RISCV_SRC}/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 \
# Use fusesoc to resolve the tree of components, copy all resolved source files into the build/ directory,
# and then generate a filelist for jasper to ingest.
# Finally, apply a number of small RTL patches necessary to make the formal flow work. (see files in patches/)
# (Only patch the duplicated source files that fusesoc has copied into build/fusesoc/src, not the version-controlled originals)
# - Note. we use the 'vcs' fusesoc backend flow to generate the filelist. This is because fusesoc does not currently implement a
# JasperGold backend, but this is not an issue as the file-format generated by the vcs flow is compatible with jasper.
.PHONY: fusesoc
fusesoc:
mkdir -p build/fusesoc
fusesoc \
--cores-root $(IBEX_ROOT) \
run \
--build-root build/fusesoc \
--tool vcs \
--setup \
lowrisc:ibex:ibex_formal:0.1
patch -p0 < patches/ibex_top.diff
patch -p0 < patches/ibex_id_stage.diff
.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: psgen
psgen:
mkdir -p build
psgen $(addprefix -path ,$(PSGEN_SRCS)) $(PSGEN_FLAGS) -sv-out build/psgen.sv -tcl-out build/psgen.tcl
.PHONY: jg
jg: fusesoc psgen sv
jg verify.tcl -allow_unsupported_OS -acquire_proj
# The following default target is intended for regressions / unattended runs.
.PHONY: all
all: fusesoc psgen sv
jg verify.tcl -allow_unsupported_OS -acquire_proj -no_gui --- "prove_no_liveness"
################################################################################
.PHONY: clean
clean:
rm -rf build/
rm -rf jgproject/
rm -rf jgproofs/

239
dv/formal/README.md Normal file
View file

@ -0,0 +1,239 @@
# End-to-End Formal Verification against the Sail
Prerequisites:
- Nix (`https://zero-to-nix.com/start/install`)
- Jasper (available on your PATH):
If Jasper is not found, `nix develop` will refuse to enter the development shell.
Build instructions:
- Clone this repository
- `cd dv/formal`
- `nix develop .#formal`
- `make` invokes Jasper in batch-mode, and attempts to prove everything, which is meant for regressions.
- `make jg` invokes Jasper interactively, halting after sourcing the contents of `verify.tcl`.
Building as above invokes the following steps, which can also be done manually during development:
- `git submodule update --init --recursive`
- `make fusesoc` fetches the necessary RTL using the FuseSoC tool and makes a local copy inside `build/`.
This also creates a filelist (`.scr`) that Jasper knows how to ingest.
This step also patches the Ibex RTL with the changes described [in the section below](#rtl-changes).
- `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.
- `jg verify.tcl` invokes Jasper interactively, sourcing the configuration & run script.
Requires the above two steps to be executed first.
After this command, Jasper should start up and should execute the commands in the TCL file.
You can see the different steps of the proof in the `Task Tree` tab.
Then, you can prove each step in order by right clicking on them and clicking `Prove Task`.
Some tasks may take longer than others and you can select specific properties in the `Property Table` and prove them individually by right clicking and selecting `Prove Property`.
Some steps require a lot of RAM and CPU so we recommend closing any other resource-heavy programs running on your computer.
We've had the proof complete using a machine with 128 GiB of RAM and 32 cores.
To avoid manually running each step you can also use the `prove_lemmas` command inside the TCL command interface located below your session window.
## Development
Identical to the above, but use `nix develop .#formal-dev`.
Local versions of psgen or Sail can be used once the formal-dev shell is open by prepending to `PATH`:
- psgen: (`https://github.com/mndstrmr/psgen`)
- Clone the repository to \<psgen-dir\> : `git clone https://github.com/mndstrmr/psgen`
- Make local changes...
- Build with `nix develop --command bash -c "go build"`
- In the formal-dev shell:
- Add to path with `export PATH=<psgen-dir>:$PATH`
- lowRISC Sail: (`https://github.com/lowrisc/sail` on the `lowrisc` branch).
- Clone the repository to \<sail-dir\> `git clone --branch lowrisc https://github.com/lowrisc/sail`
- Make local changes...
- Build with `nix develop github:lowrisc/ibex-formal-embargoed#lowrisc_sail --command bash -c "dune build --release && dune install --prefix ."`
- In the formal-dev shell:
- Add to path with `export PATH=<sail-dir>/bin:$PATH`
- Update `LOWRISC_SAIL_SRC` to point to the source root with `export LOWRISC_SAIL_SRC=<sail-dir>`.
- sail-riscv: (`https://github.com/lowrisc/sail-riscv`) Can be swapped out by changing `LOWRISC_SAIL_RISCV_SRC`.
- Clone the repository to \<sail-riscv-dir\> (`git clone https://github.com/lowrisc/sail-riscv`).
- Checkout local version / make local changes...
- In the formal-dev shell:
- Update `LOWRISC_SAIL_RISCV_SRC` to point to the source root with `export LOWRISC_SAIL_RISCV_SRC=<sail-riscv-dir>`.
## 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 proven 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`.
These changes are made automatically by `make` and `make jg`.
## 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 (ignoring 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 `riscv.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 accidentally 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 handle an interrupt, it does so correctly.
7. I haven't proved security, I have proved correctness, or more specifically 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 entered if they couldn't ever be exited in `protocol/irqs.sv`.
This probably should be legal behaviour, but without it liveness is false.
There could probably instead be a specific carve-out for this case, since it's also legal behaviour.
3. If a WFI is entered 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 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
View 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
View 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
View 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
View 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
View 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
View 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;

134
dv/formal/check/peek/follower.sv Normal file
View file

@ -0,0 +1,134 @@
// 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
View 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
View 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
View 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
View 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)
);

486
dv/formal/check/top.sv Normal file
View file

@ -0,0 +1,486 @@
// 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[32];
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[32];
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

31
dv/formal/ibex_formal.core Normal file
View file

@ -0,0 +1,31 @@
CAPI=2:
# Copyright lowRISC contributors.
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
# SPDX-License-Identifier: Apache-2.0
name: "lowrisc:ibex:ibex_formal:0.1"
description: "Ibex formal module used to prove equivalence with Sail"
filesets:
files_rtl:
depend:
- lowrisc:ibex:ibex_pkg
- lowrisc:ibex:ibex_core
- lowrisc:prim:buf
- lowrisc:prim:clock_gating
- lowrisc:prim:secded
- lowrisc:prim:assert
- lowrisc:prim:ram_1p_pkg
- lowrisc:prim_generic:buf
- lowrisc:prim_generic:clock_gating
files:
- ../../rtl/ibex_register_file_ff.sv # generic FF-based
- ../../rtl/ibex_register_file_fpga.sv # FPGA
- ../../rtl/ibex_register_file_latch.sv # ASIC
- ../../rtl/ibex_top.sv
file_type: systemVerilogSource
targets:
default:
filesets:
- files_rtl
toplevel: ibex_top

58
dv/formal/instrs.json Normal file
View 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"
]

11
dv/formal/patches/ibex_id_stage.diff Normal file
View file

@ -0,0 +1,11 @@
--- build/fusesoc/src/lowrisc_ibex_ibex_core_0.1/rtl/ibex_id_stage.sv 2024-08-25 12:37:56.787684672 +0100
+++ build/fusesoc/src/lowrisc_ibex_ibex_core_0.1/rtl/ibex_id_stage.sv 2024-08-25 12:39:23.606231887 +0100
@@ -522,7 +522,7 @@
// - 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 ||

31
dv/formal/patches/ibex_top.diff Normal file
View file

@ -0,0 +1,31 @@
--- build/fusesoc/rtl/ibex_top.sv 2024-08-25 12:49:31.975238123 +0100
+++ build/fusesoc/rtl/ibex_top.sv 2024-08-25 12:51:45.786743599 +0100
@@ -142,7 +142,7 @@
);
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 @@
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 //

520
dv/formal/poetry.lock generated Normal file
View file

@ -0,0 +1,520 @@
# This file is automatically @generated by Poetry 1.8.3 and should not be changed by hand.
[[package]]
name = "anytree"
version = "2.8.0"
description = "Powerful and Lightweight Python Tree Data Structure.."
optional = false
python-versions = "*"
files = [
{file = "anytree-2.8.0-py2.py3-none-any.whl", hash = "sha256:14c55ac77492b11532395049a03b773d14c7e30b22aa012e337b1e983de31521"},
{file = "anytree-2.8.0.tar.gz", hash = "sha256:3f0f93f355a91bc3e6245319bf4c1d50e3416cc7a35cc1133c1ff38306bbccab"},
]
[package.dependencies]
six = ">=1.9.0"
[package.extras]
dev = ["check-manifest"]
test = ["coverage"]
[[package]]
name = "attrs"
version = "24.2.0"
description = "Classes Without Boilerplate"
optional = false
python-versions = ">=3.7"
files = [
{file = "attrs-24.2.0-py3-none-any.whl", hash = "sha256:81921eb96de3191c8258c199618104dd27ac608d9366f5e35d011eae1867ede2"},
{file = "attrs-24.2.0.tar.gz", hash = "sha256:5cfb1b9148b5b086569baec03f20d7b6bf3bcacc9a42bebf87ffaaca362f6346"},
]
[package.extras]
benchmark = ["cloudpickle", "hypothesis", "mypy (>=1.11.1)", "pympler", "pytest (>=4.3.0)", "pytest-codspeed", "pytest-mypy-plugins", "pytest-xdist[psutil]"]
cov = ["cloudpickle", "coverage[toml] (>=5.3)", "hypothesis", "mypy (>=1.11.1)", "pympler", "pytest (>=4.3.0)", "pytest-mypy-plugins", "pytest-xdist[psutil]"]
dev = ["cloudpickle", "hypothesis", "mypy (>=1.11.1)", "pre-commit", "pympler", "pytest (>=4.3.0)", "pytest-mypy-plugins", "pytest-xdist[psutil]"]
docs = ["cogapp", "furo", "myst-parser", "sphinx", "sphinx-notfound-page", "sphinxcontrib-towncrier", "towncrier (<24.7)"]
tests = ["cloudpickle", "hypothesis", "mypy (>=1.11.1)", "pympler", "pytest (>=4.3.0)", "pytest-mypy-plugins", "pytest-xdist[psutil]"]
tests-mypy = ["mypy (>=1.11.1)", "pytest-mypy-plugins"]
[[package]]
name = "distro"
version = "1.9.0"
description = "Distro - an OS platform information API"
optional = false
python-versions = ">=3.6"
files = [
{file = "distro-1.9.0-py3-none-any.whl", hash = "sha256:7bffd925d65168f85027d8da9af6bddab658135b840670a223589bc0c8ef02b2"},
{file = "distro-1.9.0.tar.gz", hash = "sha256:2fa77c6fd8940f116ee1d6b94a2f90b13b5ea8d019b98bc8bafdcabcdd9bdbed"},
]
[[package]]
name = "edalize"
version = "0.4.0"
description = "Library for interfacing EDA tools such as simulators, linters or synthesis tools, using a common interface"
optional = false
python-versions = ">=3.6, <4"
files = []
develop = false
[package.dependencies]
Jinja2 = ">=3"
[package.extras]
reporting = ["pandas", "pyparsing"]
[package.source]
type = "git"
url = "https://github.com/lowRISC/edalize.git"
reference = "v0.4.0"
resolved_reference = "2a70c4421db186b4ec91c770addc89ec83f3818b"
[[package]]
name = "fusesoc"
version = "0.4"
description = "FuseSoC is a package manager and a set of build tools for HDL (Hardware Description Language) code."
optional = false
python-versions = ">=3.6, <4"
files = []
develop = false
[package.dependencies]
edalize = ">=0.2.3"
pyparsing = "*"
pyyaml = "*"
simplesat = ">=0.8.0"
[package.source]
type = "git"
url = "https://github.com/lowRISC/fusesoc.git"
reference = "ot-0.4"
resolved_reference = "e20b92898f6d14574cca8d636a841845b0817585"
[[package]]
name = "hjson"
version = "3.1.0"
description = "Hjson, a user interface for JSON."
optional = false
python-versions = "*"
files = [
{file = "hjson-3.1.0-py3-none-any.whl", hash = "sha256:65713cdcf13214fb554eb8b4ef803419733f4f5e551047c9b711098ab7186b89"},
{file = "hjson-3.1.0.tar.gz", hash = "sha256:55af475a27cf83a7969c808399d7bccdec8fb836a07ddbd574587593b9cdcf75"},
]
[[package]]
name = "jinja2"
version = "3.1.4"
description = "A very fast and expressive template engine."
optional = false
python-versions = ">=3.7"
files = [
{file = "jinja2-3.1.4-py3-none-any.whl", hash = "sha256:bc5dd2abb727a5319567b7a813e6a2e7318c39f4f487cfe6c89c6f9c7d25197d"},
{file = "jinja2-3.1.4.tar.gz", hash = "sha256:4a3aee7acbbe7303aede8e9648d13b8bf88a429282aa6122a993f0ac800cb369"},
]
[package.dependencies]
MarkupSafe = ">=2.0"
[package.extras]
i18n = ["Babel (>=2.7)"]
[[package]]
name = "jsonschema"
version = "4.23.0"
description = "An implementation of JSON Schema validation for Python"
optional = false
python-versions = ">=3.8"
files = [
{file = "jsonschema-4.23.0-py3-none-any.whl", hash = "sha256:fbadb6f8b144a8f8cf9f0b89ba94501d143e50411a1278633f56a7acf7fd5566"},
{file = "jsonschema-4.23.0.tar.gz", hash = "sha256:d71497fef26351a33265337fa77ffeb82423f3ea21283cd9467bb03999266bc4"},
]
[package.dependencies]
attrs = ">=22.2.0"
jsonschema-specifications = ">=2023.03.6"
referencing = ">=0.28.4"
rpds-py = ">=0.7.1"
[package.extras]
format = ["fqdn", "idna", "isoduration", "jsonpointer (>1.13)", "rfc3339-validator", "rfc3987", "uri-template", "webcolors (>=1.11)"]
format-nongpl = ["fqdn", "idna", "isoduration", "jsonpointer (>1.13)", "rfc3339-validator", "rfc3986-validator (>0.1.0)", "uri-template", "webcolors (>=24.6.0)"]
[[package]]
name = "jsonschema-specifications"
version = "2023.12.1"
description = "The JSON Schema meta-schemas and vocabularies, exposed as a Registry"
optional = false
python-versions = ">=3.8"
files = [
{file = "jsonschema_specifications-2023.12.1-py3-none-any.whl", hash = "sha256:87e4fdf3a94858b8a2ba2778d9ba57d8a9cafca7c7489c46ba0d30a8bc6a9c3c"},
{file = "jsonschema_specifications-2023.12.1.tar.gz", hash = "sha256:48a76787b3e70f5ed53f1160d2b81f586e4ca6d1548c5de7085d1682674764cc"},
]
[package.dependencies]
referencing = ">=0.31.0"
[[package]]
name = "mako"
version = "1.1.6"
description = "A super-fast templating language that borrows the best ideas from the existing templating languages."
optional = false
python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*"
files = [
{file = "Mako-1.1.6-py2.py3-none-any.whl", hash = "sha256:afaf8e515d075b22fad7d7b8b30e4a1c90624ff2f3733a06ec125f5a5f043a57"},
{file = "Mako-1.1.6.tar.gz", hash = "sha256:4e9e345a41924a954251b95b4b28e14a301145b544901332e658907a7464b6b2"},
]
[package.dependencies]
MarkupSafe = ">=0.9.2"
[package.extras]
babel = ["Babel"]
lingua = ["lingua"]
[[package]]
name = "markupsafe"
version = "2.1.5"
description = "Safely add untrusted strings to HTML/XML markup."
optional = false
python-versions = ">=3.7"
files = [
{file = "MarkupSafe-2.1.5-cp310-cp310-macosx_10_9_universal2.whl", hash = "sha256:a17a92de5231666cfbe003f0e4b9b3a7ae3afb1ec2845aadc2bacc93ff85febc"},
{file = "MarkupSafe-2.1.5-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:72b6be590cc35924b02c78ef34b467da4ba07e4e0f0454a2c5907f473fc50ce5"},
{file = "MarkupSafe-2.1.5-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:e61659ba32cf2cf1481e575d0462554625196a1f2fc06a1c777d3f48e8865d46"},
{file = "MarkupSafe-2.1.5-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:2174c595a0d73a3080ca3257b40096db99799265e1c27cc5a610743acd86d62f"},
{file = "MarkupSafe-2.1.5-cp310-cp310-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:ae2ad8ae6ebee9d2d94b17fb62763125f3f374c25618198f40cbb8b525411900"},
{file = "MarkupSafe-2.1.5-cp310-cp310-musllinux_1_1_aarch64.whl", hash = "sha256:075202fa5b72c86ad32dc7d0b56024ebdbcf2048c0ba09f1cde31bfdd57bcfff"},
{file = "MarkupSafe-2.1.5-cp310-cp310-musllinux_1_1_i686.whl", hash = "sha256:598e3276b64aff0e7b3451b72e94fa3c238d452e7ddcd893c3ab324717456bad"},
{file = "MarkupSafe-2.1.5-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:fce659a462a1be54d2ffcacea5e3ba2d74daa74f30f5f143fe0c58636e355fdd"},
{file = "MarkupSafe-2.1.5-cp310-cp310-win32.whl", hash = "sha256:d9fad5155d72433c921b782e58892377c44bd6252b5af2f67f16b194987338a4"},
{file = "MarkupSafe-2.1.5-cp310-cp310-win_amd64.whl", hash = "sha256:bf50cd79a75d181c9181df03572cdce0fbb75cc353bc350712073108cba98de5"},
{file = "MarkupSafe-2.1.5-cp311-cp311-macosx_10_9_universal2.whl", hash = "sha256:629ddd2ca402ae6dbedfceeba9c46d5f7b2a61d9749597d4307f943ef198fc1f"},
{file = "MarkupSafe-2.1.5-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:5b7b716f97b52c5a14bffdf688f971b2d5ef4029127f1ad7a513973cfd818df2"},
{file = "MarkupSafe-2.1.5-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:6ec585f69cec0aa07d945b20805be741395e28ac1627333b1c5b0105962ffced"},
{file = "MarkupSafe-2.1.5-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:b91c037585eba9095565a3556f611e3cbfaa42ca1e865f7b8015fe5c7336d5a5"},
{file = "MarkupSafe-2.1.5-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:7502934a33b54030eaf1194c21c692a534196063db72176b0c4028e140f8f32c"},
{file = "MarkupSafe-2.1.5-cp311-cp311-musllinux_1_1_aarch64.whl", hash = "sha256:0e397ac966fdf721b2c528cf028494e86172b4feba51d65f81ffd65c63798f3f"},
{file = "MarkupSafe-2.1.5-cp311-cp311-musllinux_1_1_i686.whl", hash = "sha256:c061bb86a71b42465156a3ee7bd58c8c2ceacdbeb95d05a99893e08b8467359a"},
{file = "MarkupSafe-2.1.5-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:3a57fdd7ce31c7ff06cdfbf31dafa96cc533c21e443d57f5b1ecc6cdc668ec7f"},
{file = "MarkupSafe-2.1.5-cp311-cp311-win32.whl", hash = "sha256:397081c1a0bfb5124355710fe79478cdbeb39626492b15d399526ae53422b906"},
{file = "MarkupSafe-2.1.5-cp311-cp311-win_amd64.whl", hash = "sha256:2b7c57a4dfc4f16f7142221afe5ba4e093e09e728ca65c51f5620c9aaeb9a617"},
{file = "MarkupSafe-2.1.5-cp312-cp312-macosx_10_9_universal2.whl", hash = "sha256:8dec4936e9c3100156f8a2dc89c4b88d5c435175ff03413b443469c7c8c5f4d1"},
{file = "MarkupSafe-2.1.5-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:3c6b973f22eb18a789b1460b4b91bf04ae3f0c4234a0a6aa6b0a92f6f7b951d4"},
{file = "MarkupSafe-2.1.5-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:ac07bad82163452a6884fe8fa0963fb98c2346ba78d779ec06bd7a6262132aee"},
{file = "MarkupSafe-2.1.5-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:f5dfb42c4604dddc8e4305050aa6deb084540643ed5804d7455b5df8fe16f5e5"},
{file = "MarkupSafe-2.1.5-cp312-cp312-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:ea3d8a3d18833cf4304cd2fc9cbb1efe188ca9b5efef2bdac7adc20594a0e46b"},
{file = "MarkupSafe-2.1.5-cp312-cp312-musllinux_1_1_aarch64.whl", hash = "sha256:d050b3361367a06d752db6ead6e7edeb0009be66bc3bae0ee9d97fb326badc2a"},
{file = "MarkupSafe-2.1.5-cp312-cp312-musllinux_1_1_i686.whl", hash = "sha256:bec0a414d016ac1a18862a519e54b2fd0fc8bbfd6890376898a6c0891dd82e9f"},
{file = "MarkupSafe-2.1.5-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:58c98fee265677f63a4385256a6d7683ab1832f3ddd1e66fe948d5880c21a169"},
{file = "MarkupSafe-2.1.5-cp312-cp312-win32.whl", hash = "sha256:8590b4ae07a35970728874632fed7bd57b26b0102df2d2b233b6d9d82f6c62ad"},
{file = "MarkupSafe-2.1.5-cp312-cp312-win_amd64.whl", hash = "sha256:823b65d8706e32ad2df51ed89496147a42a2a6e01c13cfb6ffb8b1e92bc910bb"},
{file = "MarkupSafe-2.1.5-cp37-cp37m-macosx_10_9_x86_64.whl", hash = "sha256:c8b29db45f8fe46ad280a7294f5c3ec36dbac9491f2d1c17345be8e69cc5928f"},
{file = "MarkupSafe-2.1.5-cp37-cp37m-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:ec6a563cff360b50eed26f13adc43e61bc0c04d94b8be985e6fb24b81f6dcfdf"},
{file = "MarkupSafe-2.1.5-cp37-cp37m-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:a549b9c31bec33820e885335b451286e2969a2d9e24879f83fe904a5ce59d70a"},
{file = "MarkupSafe-2.1.5-cp37-cp37m-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:4f11aa001c540f62c6166c7726f71f7573b52c68c31f014c25cc7901deea0b52"},
{file = "MarkupSafe-2.1.5-cp37-cp37m-musllinux_1_1_aarch64.whl", hash = "sha256:7b2e5a267c855eea6b4283940daa6e88a285f5f2a67f2220203786dfa59b37e9"},
{file = "MarkupSafe-2.1.5-cp37-cp37m-musllinux_1_1_i686.whl", hash = "sha256:2d2d793e36e230fd32babe143b04cec8a8b3eb8a3122d2aceb4a371e6b09b8df"},
{file = "MarkupSafe-2.1.5-cp37-cp37m-musllinux_1_1_x86_64.whl", hash = "sha256:ce409136744f6521e39fd8e2a24c53fa18ad67aa5bc7c2cf83645cce5b5c4e50"},
{file = "MarkupSafe-2.1.5-cp37-cp37m-win32.whl", hash = "sha256:4096e9de5c6fdf43fb4f04c26fb114f61ef0bf2e5604b6ee3019d51b69e8c371"},
{file = "MarkupSafe-2.1.5-cp37-cp37m-win_amd64.whl", hash = "sha256:4275d846e41ecefa46e2015117a9f491e57a71ddd59bbead77e904dc02b1bed2"},
{file = "MarkupSafe-2.1.5-cp38-cp38-macosx_10_9_universal2.whl", hash = "sha256:656f7526c69fac7f600bd1f400991cc282b417d17539a1b228617081106feb4a"},
{file = "MarkupSafe-2.1.5-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:97cafb1f3cbcd3fd2b6fbfb99ae11cdb14deea0736fc2b0952ee177f2b813a46"},
{file = "MarkupSafe-2.1.5-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:1f3fbcb7ef1f16e48246f704ab79d79da8a46891e2da03f8783a5b6fa41a9532"},
{file = "MarkupSafe-2.1.5-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:fa9db3f79de01457b03d4f01b34cf91bc0048eb2c3846ff26f66687c2f6d16ab"},
{file = "MarkupSafe-2.1.5-cp38-cp38-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:ffee1f21e5ef0d712f9033568f8344d5da8cc2869dbd08d87c84656e6a2d2f68"},
{file = "MarkupSafe-2.1.5-cp38-cp38-musllinux_1_1_aarch64.whl", hash = "sha256:5dedb4db619ba5a2787a94d877bc8ffc0566f92a01c0ef214865e54ecc9ee5e0"},
{file = "MarkupSafe-2.1.5-cp38-cp38-musllinux_1_1_i686.whl", hash = "sha256:30b600cf0a7ac9234b2638fbc0fb6158ba5bdcdf46aeb631ead21248b9affbc4"},
{file = "MarkupSafe-2.1.5-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:8dd717634f5a044f860435c1d8c16a270ddf0ef8588d4887037c5028b859b0c3"},
{file = "MarkupSafe-2.1.5-cp38-cp38-win32.whl", hash = "sha256:daa4ee5a243f0f20d528d939d06670a298dd39b1ad5f8a72a4275124a7819eff"},
{file = "MarkupSafe-2.1.5-cp38-cp38-win_amd64.whl", hash = "sha256:619bc166c4f2de5caa5a633b8b7326fbe98e0ccbfacabd87268a2b15ff73a029"},
{file = "MarkupSafe-2.1.5-cp39-cp39-macosx_10_9_universal2.whl", hash = "sha256:7a68b554d356a91cce1236aa7682dc01df0edba8d043fd1ce607c49dd3c1edcf"},
{file = "MarkupSafe-2.1.5-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:db0b55e0f3cc0be60c1f19efdde9a637c32740486004f20d1cff53c3c0ece4d2"},
{file = "MarkupSafe-2.1.5-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:3e53af139f8579a6d5f7b76549125f0d94d7e630761a2111bc431fd820e163b8"},
{file = "MarkupSafe-2.1.5-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:17b950fccb810b3293638215058e432159d2b71005c74371d784862b7e4683f3"},
{file = "MarkupSafe-2.1.5-cp39-cp39-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:4c31f53cdae6ecfa91a77820e8b151dba54ab528ba65dfd235c80b086d68a465"},
{file = "MarkupSafe-2.1.5-cp39-cp39-musllinux_1_1_aarch64.whl", hash = "sha256:bff1b4290a66b490a2f4719358c0cdcd9bafb6b8f061e45c7a2460866bf50c2e"},
{file = "MarkupSafe-2.1.5-cp39-cp39-musllinux_1_1_i686.whl", hash = "sha256:bc1667f8b83f48511b94671e0e441401371dfd0f0a795c7daa4a3cd1dde55bea"},
{file = "MarkupSafe-2.1.5-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:5049256f536511ee3f7e1b3f87d1d1209d327e818e6ae1365e8653d7e3abb6a6"},
{file = "MarkupSafe-2.1.5-cp39-cp39-win32.whl", hash = "sha256:00e046b6dd71aa03a41079792f8473dc494d564611a8f89bbbd7cb93295ebdcf"},
{file = "MarkupSafe-2.1.5-cp39-cp39-win_amd64.whl", hash = "sha256:fa173ec60341d6bb97a89f5ea19c85c5643c1e7dedebc22f5181eb73573142c5"},
{file = "MarkupSafe-2.1.5.tar.gz", hash = "sha256:d283d37a890ba4c1ae73ffadf8046435c76e7bc2247bbb63c00bd1a709c6544b"},
]
[[package]]
name = "okonomiyaki"
version = "1.4.0"
description = "Self-contained library to deal with metadata in Enthought-specific egg and runtime archives"
optional = false
python-versions = ">=2.7"
files = [
{file = "okonomiyaki-1.4.0-py2.py3-none-any.whl", hash = "sha256:174af185f866fc42fdb58b2d6c7107d870f795e3f404b9c6278f8e62f87f0f83"},
{file = "okonomiyaki-1.4.0.tar.gz", hash = "sha256:508008004a12e09f565d8b4e4145bd7500787fdd6810d898fdc8e5c61a3f41e5"},
]
[package.dependencies]
attrs = ">=16.1.0"
distro = {version = "*", markers = "sys_platform == \"linux\" or sys_platform == \"linux2\""}
jsonschema = ">=2.5.1"
six = ">=1.9.0"
zipfile2 = ">=0.0.12"
[package.extras]
test = ["distro", "haas", "hypothesis", "mock", "packaging (>=20.0)", "testfixtures"]
[[package]]
name = "packaging"
version = "23.1"
description = "Core utilities for Python packages"
optional = false
python-versions = ">=3.7"
files = [
{file = "packaging-23.1-py3-none-any.whl", hash = "sha256:994793af429502c4ea2ebf6bf664629d07c1a9fe974af92966e4b8d2df7edc61"},
{file = "packaging-23.1.tar.gz", hash = "sha256:a392980d2b6cffa644431898be54b0045151319d1e7ec34f0cfed48767dd334f"},
]
[[package]]
name = "pyparsing"
version = "3.1.2"
description = "pyparsing module - Classes and methods to define and execute parsing grammars"
optional = false
python-versions = ">=3.6.8"
files = [
{file = "pyparsing-3.1.2-py3-none-any.whl", hash = "sha256:f9db75911801ed778fe61bb643079ff86601aca99fcae6345aa67292038fb742"},
{file = "pyparsing-3.1.2.tar.gz", hash = "sha256:a1bac0ce561155ecc3ed78ca94d3c9378656ad4c94c1270de543f621420f94ad"},
]
[package.extras]
diagrams = ["jinja2", "railroad-diagrams"]
[[package]]
name = "pyyaml"
version = "6.0"
description = "YAML parser and emitter for Python"
optional = false
python-versions = ">=3.6"
files = [
{file = "PyYAML-6.0-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:d4db7c7aef085872ef65a8fd7d6d09a14ae91f691dec3e87ee5ee0539d516f53"},
{file = "PyYAML-6.0-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:9df7ed3b3d2e0ecfe09e14741b857df43adb5a3ddadc919a2d94fbdf78fea53c"},
{file = "PyYAML-6.0-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:77f396e6ef4c73fdc33a9157446466f1cff553d979bd00ecb64385760c6babdc"},
{file = "PyYAML-6.0-cp310-cp310-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:a80a78046a72361de73f8f395f1f1e49f956c6be882eed58505a15f3e430962b"},
{file = "PyYAML-6.0-cp310-cp310-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_12_x86_64.manylinux2010_x86_64.whl", hash = "sha256:f84fbc98b019fef2ee9a1cb3ce93e3187a6df0b2538a651bfb890254ba9f90b5"},
{file = "PyYAML-6.0-cp310-cp310-win32.whl", hash = "sha256:2cd5df3de48857ed0544b34e2d40e9fac445930039f3cfe4bcc592a1f836d513"},
{file = "PyYAML-6.0-cp310-cp310-win_amd64.whl", hash = "sha256:daf496c58a8c52083df09b80c860005194014c3698698d1a57cbcfa182142a3a"},
{file = "PyYAML-6.0-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:d4b0ba9512519522b118090257be113b9468d804b19d63c71dbcf4a48fa32358"},
{file = "PyYAML-6.0-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:81957921f441d50af23654aa6c5e5eaf9b06aba7f0a19c18a538dc7ef291c5a1"},
{file = "PyYAML-6.0-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:afa17f5bc4d1b10afd4466fd3a44dc0e245382deca5b3c353d8b757f9e3ecb8d"},
{file = "PyYAML-6.0-cp311-cp311-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:dbad0e9d368bb989f4515da330b88a057617d16b6a8245084f1b05400f24609f"},
{file = "PyYAML-6.0-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:432557aa2c09802be39460360ddffd48156e30721f5e8d917f01d31694216782"},
{file = "PyYAML-6.0-cp311-cp311-win32.whl", hash = "sha256:bfaef573a63ba8923503d27530362590ff4f576c626d86a9fed95822a8255fd7"},
{file = "PyYAML-6.0-cp311-cp311-win_amd64.whl", hash = "sha256:01b45c0191e6d66c470b6cf1b9531a771a83c1c4208272ead47a3ae4f2f603bf"},
{file = "PyYAML-6.0-cp36-cp36m-macosx_10_9_x86_64.whl", hash = "sha256:897b80890765f037df3403d22bab41627ca8811ae55e9a722fd0392850ec4d86"},
{file = "PyYAML-6.0-cp36-cp36m-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:50602afada6d6cbfad699b0c7bb50d5ccffa7e46a3d738092afddc1f9758427f"},
{file = "PyYAML-6.0-cp36-cp36m-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:48c346915c114f5fdb3ead70312bd042a953a8ce5c7106d5bfb1a5254e47da92"},
{file = "PyYAML-6.0-cp36-cp36m-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_12_x86_64.manylinux2010_x86_64.whl", hash = "sha256:98c4d36e99714e55cfbaaee6dd5badbc9a1ec339ebfc3b1f52e293aee6bb71a4"},
{file = "PyYAML-6.0-cp36-cp36m-win32.whl", hash = "sha256:0283c35a6a9fbf047493e3a0ce8d79ef5030852c51e9d911a27badfde0605293"},
{file = "PyYAML-6.0-cp36-cp36m-win_amd64.whl", hash = "sha256:07751360502caac1c067a8132d150cf3d61339af5691fe9e87803040dbc5db57"},
{file = "PyYAML-6.0-cp37-cp37m-macosx_10_9_x86_64.whl", hash = "sha256:819b3830a1543db06c4d4b865e70ded25be52a2e0631ccd2f6a47a2822f2fd7c"},
{file = "PyYAML-6.0-cp37-cp37m-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:473f9edb243cb1935ab5a084eb238d842fb8f404ed2193a915d1784b5a6b5fc0"},
{file = "PyYAML-6.0-cp37-cp37m-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:0ce82d761c532fe4ec3f87fc45688bdd3a4c1dc5e0b4a19814b9009a29baefd4"},
{file = "PyYAML-6.0-cp37-cp37m-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_12_x86_64.manylinux2010_x86_64.whl", hash = "sha256:231710d57adfd809ef5d34183b8ed1eeae3f76459c18fb4a0b373ad56bedcdd9"},
{file = "PyYAML-6.0-cp37-cp37m-win32.whl", hash = "sha256:c5687b8d43cf58545ade1fe3e055f70eac7a5a1a0bf42824308d868289a95737"},
{file = "PyYAML-6.0-cp37-cp37m-win_amd64.whl", hash = "sha256:d15a181d1ecd0d4270dc32edb46f7cb7733c7c508857278d3d378d14d606db2d"},
{file = "PyYAML-6.0-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:0b4624f379dab24d3725ffde76559cff63d9ec94e1736b556dacdfebe5ab6d4b"},
{file = "PyYAML-6.0-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:213c60cd50106436cc818accf5baa1aba61c0189ff610f64f4a3e8c6726218ba"},
{file = "PyYAML-6.0-cp38-cp38-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:9fa600030013c4de8165339db93d182b9431076eb98eb40ee068700c9c813e34"},
{file = "PyYAML-6.0-cp38-cp38-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_12_x86_64.manylinux2010_x86_64.whl", hash = "sha256:277a0ef2981ca40581a47093e9e2d13b3f1fbbeffae064c1d21bfceba2030287"},
{file = "PyYAML-6.0-cp38-cp38-win32.whl", hash = "sha256:d4eccecf9adf6fbcc6861a38015c2a64f38b9d94838ac1810a9023a0609e1b78"},
{file = "PyYAML-6.0-cp38-cp38-win_amd64.whl", hash = "sha256:1e4747bc279b4f613a09eb64bba2ba602d8a6664c6ce6396a4d0cd413a50ce07"},
{file = "PyYAML-6.0-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:055d937d65826939cb044fc8c9b08889e8c743fdc6a32b33e2390f66013e449b"},
{file = "PyYAML-6.0-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:e61ceaab6f49fb8bdfaa0f92c4b57bcfbea54c09277b1b4f7ac376bfb7a7c174"},
{file = "PyYAML-6.0-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:d67d839ede4ed1b28a4e8909735fc992a923cdb84e618544973d7dfc71540803"},
{file = "PyYAML-6.0-cp39-cp39-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:cba8c411ef271aa037d7357a2bc8f9ee8b58b9965831d9e51baf703280dc73d3"},
{file = "PyYAML-6.0-cp39-cp39-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_12_x86_64.manylinux2010_x86_64.whl", hash = "sha256:40527857252b61eacd1d9af500c3337ba8deb8fc298940291486c465c8b46ec0"},
{file = "PyYAML-6.0-cp39-cp39-win32.whl", hash = "sha256:b5b9eccad747aabaaffbc6064800670f0c297e52c12754eb1d976c57e4f74dcb"},
{file = "PyYAML-6.0-cp39-cp39-win_amd64.whl", hash = "sha256:b3d267842bf12586ba6c734f89d1f5b871df0273157918b0ccefa29deb05c21c"},
{file = "PyYAML-6.0.tar.gz", hash = "sha256:68fb519c14306fec9720a2a5b45bc9f0c8d1b9c72adf45c37baedfcd949c35a2"},
]
[[package]]
name = "referencing"
version = "0.35.1"
description = "JSON Referencing + Python"
optional = false
python-versions = ">=3.8"
files = [
{file = "referencing-0.35.1-py3-none-any.whl", hash = "sha256:eda6d3234d62814d1c64e305c1331c9a3a6132da475ab6382eaa997b21ee75de"},
{file = "referencing-0.35.1.tar.gz", hash = "sha256:25b42124a6c8b632a425174f24087783efb348a6f1e0008e63cd4466fedf703c"},
]
[package.dependencies]
attrs = ">=22.2.0"
rpds-py = ">=0.7.0"
[[package]]
name = "rpds-py"
version = "0.20.0"
description = "Python bindings to Rust's persistent data structures (rpds)"
optional = false
python-versions = ">=3.8"
files = [
{file = "rpds_py-0.20.0-cp310-cp310-macosx_10_12_x86_64.whl", hash = "sha256:3ad0fda1635f8439cde85c700f964b23ed5fc2d28016b32b9ee5fe30da5c84e2"},
{file = "rpds_py-0.20.0-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:9bb4a0d90fdb03437c109a17eade42dfbf6190408f29b2744114d11586611d6f"},
{file = "rpds_py-0.20.0-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:c6377e647bbfd0a0b159fe557f2c6c602c159fc752fa316572f012fc0bf67150"},
{file = "rpds_py-0.20.0-cp310-cp310-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:eb851b7df9dda52dc1415ebee12362047ce771fc36914586b2e9fcbd7d293b3e"},
{file = "rpds_py-0.20.0-cp310-cp310-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:1e0f80b739e5a8f54837be5d5c924483996b603d5502bfff79bf33da06164ee2"},
{file = "rpds_py-0.20.0-cp310-cp310-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:5a8c94dad2e45324fc74dce25e1645d4d14df9a4e54a30fa0ae8bad9a63928e3"},
{file = "rpds_py-0.20.0-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:f8e604fe73ba048c06085beaf51147eaec7df856824bfe7b98657cf436623daf"},
{file = "rpds_py-0.20.0-cp310-cp310-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:df3de6b7726b52966edf29663e57306b23ef775faf0ac01a3e9f4012a24a4140"},
{file = "rpds_py-0.20.0-cp310-cp310-musllinux_1_2_aarch64.whl", hash = "sha256:cf258ede5bc22a45c8e726b29835b9303c285ab46fc7c3a4cc770736b5304c9f"},
{file = "rpds_py-0.20.0-cp310-cp310-musllinux_1_2_i686.whl", hash = "sha256:55fea87029cded5df854ca7e192ec7bdb7ecd1d9a3f63d5c4eb09148acf4a7ce"},
{file = "rpds_py-0.20.0-cp310-cp310-musllinux_1_2_x86_64.whl", hash = "sha256:ae94bd0b2f02c28e199e9bc51485d0c5601f58780636185660f86bf80c89af94"},
{file = "rpds_py-0.20.0-cp310-none-win32.whl", hash = "sha256:28527c685f237c05445efec62426d285e47a58fb05ba0090a4340b73ecda6dee"},
{file = "rpds_py-0.20.0-cp310-none-win_amd64.whl", hash = "sha256:238a2d5b1cad28cdc6ed15faf93a998336eb041c4e440dd7f902528b8891b399"},
{file = "rpds_py-0.20.0-cp311-cp311-macosx_10_12_x86_64.whl", hash = "sha256:ac2f4f7a98934c2ed6505aead07b979e6f999389f16b714448fb39bbaa86a489"},
{file = "rpds_py-0.20.0-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:220002c1b846db9afd83371d08d239fdc865e8f8c5795bbaec20916a76db3318"},
{file = "rpds_py-0.20.0-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:8d7919548df3f25374a1f5d01fbcd38dacab338ef5f33e044744b5c36729c8db"},
{file = "rpds_py-0.20.0-cp311-cp311-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:758406267907b3781beee0f0edfe4a179fbd97c0be2e9b1154d7f0a1279cf8e5"},
{file = "rpds_py-0.20.0-cp311-cp311-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:3d61339e9f84a3f0767b1995adfb171a0d00a1185192718a17af6e124728e0f5"},
{file = "rpds_py-0.20.0-cp311-cp311-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:1259c7b3705ac0a0bd38197565a5d603218591d3f6cee6e614e380b6ba61c6f6"},
{file = "rpds_py-0.20.0-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:5c1dc0f53856b9cc9a0ccca0a7cc61d3d20a7088201c0937f3f4048c1718a209"},
{file = "rpds_py-0.20.0-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:7e60cb630f674a31f0368ed32b2a6b4331b8350d67de53c0359992444b116dd3"},
{file = "rpds_py-0.20.0-cp311-cp311-musllinux_1_2_aarch64.whl", hash = "sha256:dbe982f38565bb50cb7fb061ebf762c2f254ca3d8c20d4006878766e84266272"},
{file = "rpds_py-0.20.0-cp311-cp311-musllinux_1_2_i686.whl", hash = "sha256:514b3293b64187172bc77c8fb0cdae26981618021053b30d8371c3a902d4d5ad"},
{file = "rpds_py-0.20.0-cp311-cp311-musllinux_1_2_x86_64.whl", hash = "sha256:d0a26ffe9d4dd35e4dfdd1e71f46401cff0181c75ac174711ccff0459135fa58"},
{file = "rpds_py-0.20.0-cp311-none-win32.whl", hash = "sha256:89c19a494bf3ad08c1da49445cc5d13d8fefc265f48ee7e7556839acdacf69d0"},
{file = "rpds_py-0.20.0-cp311-none-win_amd64.whl", hash = "sha256:c638144ce971df84650d3ed0096e2ae7af8e62ecbbb7b201c8935c370df00a2c"},
{file = "rpds_py-0.20.0-cp312-cp312-macosx_10_12_x86_64.whl", hash = "sha256:a84ab91cbe7aab97f7446652d0ed37d35b68a465aeef8fc41932a9d7eee2c1a6"},
{file = "rpds_py-0.20.0-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:56e27147a5a4c2c21633ff8475d185734c0e4befd1c989b5b95a5d0db699b21b"},
{file = "rpds_py-0.20.0-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:2580b0c34583b85efec8c5c5ec9edf2dfe817330cc882ee972ae650e7b5ef739"},
{file = "rpds_py-0.20.0-cp312-cp312-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:b80d4a7900cf6b66bb9cee5c352b2d708e29e5a37fe9bf784fa97fc11504bf6c"},
{file = "rpds_py-0.20.0-cp312-cp312-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:50eccbf054e62a7b2209b28dc7a22d6254860209d6753e6b78cfaeb0075d7bee"},
{file = "rpds_py-0.20.0-cp312-cp312-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:49a8063ea4296b3a7e81a5dfb8f7b2d73f0b1c20c2af401fb0cdf22e14711a96"},
{file = "rpds_py-0.20.0-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:ea438162a9fcbee3ecf36c23e6c68237479f89f962f82dae83dc15feeceb37e4"},
{file = "rpds_py-0.20.0-cp312-cp312-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:18d7585c463087bddcfa74c2ba267339f14f2515158ac4db30b1f9cbdb62c8ef"},
{file = "rpds_py-0.20.0-cp312-cp312-musllinux_1_2_aarch64.whl", hash = "sha256:d4c7d1a051eeb39f5c9547e82ea27cbcc28338482242e3e0b7768033cb083821"},
{file = "rpds_py-0.20.0-cp312-cp312-musllinux_1_2_i686.whl", hash = "sha256:e4df1e3b3bec320790f699890d41c59d250f6beda159ea3c44c3f5bac1976940"},
{file = "rpds_py-0.20.0-cp312-cp312-musllinux_1_2_x86_64.whl", hash = "sha256:2cf126d33a91ee6eedc7f3197b53e87a2acdac63602c0f03a02dd69e4b138174"},
{file = "rpds_py-0.20.0-cp312-none-win32.whl", hash = "sha256:8bc7690f7caee50b04a79bf017a8d020c1f48c2a1077ffe172abec59870f1139"},
{file = "rpds_py-0.20.0-cp312-none-win_amd64.whl", hash = "sha256:0e13e6952ef264c40587d510ad676a988df19adea20444c2b295e536457bc585"},
{file = "rpds_py-0.20.0-cp313-cp313-macosx_10_12_x86_64.whl", hash = "sha256:aa9a0521aeca7d4941499a73ad7d4f8ffa3d1affc50b9ea11d992cd7eff18a29"},
{file = "rpds_py-0.20.0-cp313-cp313-macosx_11_0_arm64.whl", hash = "sha256:4a1f1d51eccb7e6c32ae89243cb352389228ea62f89cd80823ea7dd1b98e0b91"},
{file = "rpds_py-0.20.0-cp313-cp313-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:8a86a9b96070674fc88b6f9f71a97d2c1d3e5165574615d1f9168ecba4cecb24"},
{file = "rpds_py-0.20.0-cp313-cp313-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:6c8ef2ebf76df43f5750b46851ed1cdf8f109d7787ca40035fe19fbdc1acc5a7"},
{file = "rpds_py-0.20.0-cp313-cp313-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:b74b25f024b421d5859d156750ea9a65651793d51b76a2e9238c05c9d5f203a9"},
{file = "rpds_py-0.20.0-cp313-cp313-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:57eb94a8c16ab08fef6404301c38318e2c5a32216bf5de453e2714c964c125c8"},
{file = "rpds_py-0.20.0-cp313-cp313-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:e1940dae14e715e2e02dfd5b0f64a52e8374a517a1e531ad9412319dc3ac7879"},
{file = "rpds_py-0.20.0-cp313-cp313-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:d20277fd62e1b992a50c43f13fbe13277a31f8c9f70d59759c88f644d66c619f"},
{file = "rpds_py-0.20.0-cp313-cp313-musllinux_1_2_aarch64.whl", hash = "sha256:06db23d43f26478303e954c34c75182356ca9aa7797d22c5345b16871ab9c45c"},
{file = "rpds_py-0.20.0-cp313-cp313-musllinux_1_2_i686.whl", hash = "sha256:b2a5db5397d82fa847e4c624b0c98fe59d2d9b7cf0ce6de09e4d2e80f8f5b3f2"},
{file = "rpds_py-0.20.0-cp313-cp313-musllinux_1_2_x86_64.whl", hash = "sha256:5a35df9f5548fd79cb2f52d27182108c3e6641a4feb0f39067911bf2adaa3e57"},
{file = "rpds_py-0.20.0-cp313-none-win32.whl", hash = "sha256:fd2d84f40633bc475ef2d5490b9c19543fbf18596dcb1b291e3a12ea5d722f7a"},
{file = "rpds_py-0.20.0-cp313-none-win_amd64.whl", hash = "sha256:9bc2d153989e3216b0559251b0c260cfd168ec78b1fac33dd485750a228db5a2"},
{file = "rpds_py-0.20.0-cp38-cp38-macosx_10_12_x86_64.whl", hash = "sha256:f2fbf7db2012d4876fb0d66b5b9ba6591197b0f165db8d99371d976546472a24"},
{file = "rpds_py-0.20.0-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:1e5f3cd7397c8f86c8cc72d5a791071431c108edd79872cdd96e00abd8497d29"},
{file = "rpds_py-0.20.0-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:ce9845054c13696f7af7f2b353e6b4f676dab1b4b215d7fe5e05c6f8bb06f965"},
{file = "rpds_py-0.20.0-cp38-cp38-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:c3e130fd0ec56cb76eb49ef52faead8ff09d13f4527e9b0c400307ff72b408e1"},
{file = "rpds_py-0.20.0-cp38-cp38-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:4b16aa0107ecb512b568244ef461f27697164d9a68d8b35090e9b0c1c8b27752"},
{file = "rpds_py-0.20.0-cp38-cp38-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:aa7f429242aae2947246587d2964fad750b79e8c233a2367f71b554e9447949c"},
{file = "rpds_py-0.20.0-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:af0fc424a5842a11e28956e69395fbbeab2c97c42253169d87e90aac2886d751"},
{file = "rpds_py-0.20.0-cp38-cp38-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:b8c00a3b1e70c1d3891f0db1b05292747f0dbcfb49c43f9244d04c70fbc40eb8"},
{file = "rpds_py-0.20.0-cp38-cp38-musllinux_1_2_aarch64.whl", hash = "sha256:40ce74fc86ee4645d0a225498d091d8bc61f39b709ebef8204cb8b5a464d3c0e"},
{file = "rpds_py-0.20.0-cp38-cp38-musllinux_1_2_i686.whl", hash = "sha256:4fe84294c7019456e56d93e8ababdad5a329cd25975be749c3f5f558abb48253"},
{file = "rpds_py-0.20.0-cp38-cp38-musllinux_1_2_x86_64.whl", hash = "sha256:338ca4539aad4ce70a656e5187a3a31c5204f261aef9f6ab50e50bcdffaf050a"},
{file = "rpds_py-0.20.0-cp38-none-win32.whl", hash = "sha256:54b43a2b07db18314669092bb2de584524d1ef414588780261e31e85846c26a5"},
{file = "rpds_py-0.20.0-cp38-none-win_amd64.whl", hash = "sha256:a1862d2d7ce1674cffa6d186d53ca95c6e17ed2b06b3f4c476173565c862d232"},
{file = "rpds_py-0.20.0-cp39-cp39-macosx_10_12_x86_64.whl", hash = "sha256:3fde368e9140312b6e8b6c09fb9f8c8c2f00999d1823403ae90cc00480221b22"},
{file = "rpds_py-0.20.0-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:9824fb430c9cf9af743cf7aaf6707bf14323fb51ee74425c380f4c846ea70789"},
{file = "rpds_py-0.20.0-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:11ef6ce74616342888b69878d45e9f779b95d4bd48b382a229fe624a409b72c5"},
{file = "rpds_py-0.20.0-cp39-cp39-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:c52d3f2f82b763a24ef52f5d24358553e8403ce05f893b5347098014f2d9eff2"},
{file = "rpds_py-0.20.0-cp39-cp39-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:9d35cef91e59ebbeaa45214861874bc6f19eb35de96db73e467a8358d701a96c"},
{file = "rpds_py-0.20.0-cp39-cp39-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:d72278a30111e5b5525c1dd96120d9e958464316f55adb030433ea905866f4de"},
{file = "rpds_py-0.20.0-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:b4c29cbbba378759ac5786730d1c3cb4ec6f8ababf5c42a9ce303dc4b3d08cda"},
{file = "rpds_py-0.20.0-cp39-cp39-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:6632f2d04f15d1bd6fe0eedd3b86d9061b836ddca4c03d5cf5c7e9e6b7c14580"},
{file = "rpds_py-0.20.0-cp39-cp39-musllinux_1_2_aarch64.whl", hash = "sha256:d0b67d87bb45ed1cd020e8fbf2307d449b68abc45402fe1a4ac9e46c3c8b192b"},
{file = "rpds_py-0.20.0-cp39-cp39-musllinux_1_2_i686.whl", hash = "sha256:ec31a99ca63bf3cd7f1a5ac9fe95c5e2d060d3c768a09bc1d16e235840861420"},
{file = "rpds_py-0.20.0-cp39-cp39-musllinux_1_2_x86_64.whl", hash = "sha256:22e6c9976e38f4d8c4a63bd8a8edac5307dffd3ee7e6026d97f3cc3a2dc02a0b"},
{file = "rpds_py-0.20.0-cp39-none-win32.whl", hash = "sha256:569b3ea770c2717b730b61998b6c54996adee3cef69fc28d444f3e7920313cf7"},
{file = "rpds_py-0.20.0-cp39-none-win_amd64.whl", hash = "sha256:e6900ecdd50ce0facf703f7a00df12374b74bbc8ad9fe0f6559947fb20f82364"},
{file = "rpds_py-0.20.0-pp310-pypy310_pp73-macosx_10_12_x86_64.whl", hash = "sha256:617c7357272c67696fd052811e352ac54ed1d9b49ab370261a80d3b6ce385045"},
{file = "rpds_py-0.20.0-pp310-pypy310_pp73-macosx_11_0_arm64.whl", hash = "sha256:9426133526f69fcaba6e42146b4e12d6bc6c839b8b555097020e2b78ce908dcc"},
{file = "rpds_py-0.20.0-pp310-pypy310_pp73-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:deb62214c42a261cb3eb04d474f7155279c1a8a8c30ac89b7dcb1721d92c3c02"},
{file = "rpds_py-0.20.0-pp310-pypy310_pp73-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:fcaeb7b57f1a1e071ebd748984359fef83ecb026325b9d4ca847c95bc7311c92"},
{file = "rpds_py-0.20.0-pp310-pypy310_pp73-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:d454b8749b4bd70dd0a79f428731ee263fa6995f83ccb8bada706e8d1d3ff89d"},
{file = "rpds_py-0.20.0-pp310-pypy310_pp73-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:d807dc2051abe041b6649681dce568f8e10668e3c1c6543ebae58f2d7e617855"},
{file = "rpds_py-0.20.0-pp310-pypy310_pp73-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:c3c20f0ddeb6e29126d45f89206b8291352b8c5b44384e78a6499d68b52ae511"},
{file = "rpds_py-0.20.0-pp310-pypy310_pp73-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:b7f19250ceef892adf27f0399b9e5afad019288e9be756d6919cb58892129f51"},
{file = "rpds_py-0.20.0-pp310-pypy310_pp73-musllinux_1_2_aarch64.whl", hash = "sha256:4f1ed4749a08379555cebf4650453f14452eaa9c43d0a95c49db50c18b7da075"},
{file = "rpds_py-0.20.0-pp310-pypy310_pp73-musllinux_1_2_i686.whl", hash = "sha256:dcedf0b42bcb4cfff4101d7771a10532415a6106062f005ab97d1d0ab5681c60"},
{file = "rpds_py-0.20.0-pp310-pypy310_pp73-musllinux_1_2_x86_64.whl", hash = "sha256:39ed0d010457a78f54090fafb5d108501b5aa5604cc22408fc1c0c77eac14344"},
{file = "rpds_py-0.20.0-pp310-pypy310_pp73-win_amd64.whl", hash = "sha256:bb273176be34a746bdac0b0d7e4e2c467323d13640b736c4c477881a3220a989"},
{file = "rpds_py-0.20.0-pp39-pypy39_pp73-macosx_10_12_x86_64.whl", hash = "sha256:f918a1a130a6dfe1d7fe0f105064141342e7dd1611f2e6a21cd2f5c8cb1cfb3e"},
{file = "rpds_py-0.20.0-pp39-pypy39_pp73-macosx_11_0_arm64.whl", hash = "sha256:f60012a73aa396be721558caa3a6fd49b3dd0033d1675c6d59c4502e870fcf0c"},
{file = "rpds_py-0.20.0-pp39-pypy39_pp73-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:3d2b1ad682a3dfda2a4e8ad8572f3100f95fad98cb99faf37ff0ddfe9cbf9d03"},
{file = "rpds_py-0.20.0-pp39-pypy39_pp73-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:614fdafe9f5f19c63ea02817fa4861c606a59a604a77c8cdef5aa01d28b97921"},
{file = "rpds_py-0.20.0-pp39-pypy39_pp73-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:fa518bcd7600c584bf42e6617ee8132869e877db2f76bcdc281ec6a4113a53ab"},
{file = "rpds_py-0.20.0-pp39-pypy39_pp73-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:f0475242f447cc6cb8a9dd486d68b2ef7fbee84427124c232bff5f63b1fe11e5"},
{file = "rpds_py-0.20.0-pp39-pypy39_pp73-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:f90a4cd061914a60bd51c68bcb4357086991bd0bb93d8aa66a6da7701370708f"},
{file = "rpds_py-0.20.0-pp39-pypy39_pp73-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:def7400461c3a3f26e49078302e1c1b38f6752342c77e3cf72ce91ca69fb1bc1"},
{file = "rpds_py-0.20.0-pp39-pypy39_pp73-musllinux_1_2_aarch64.whl", hash = "sha256:65794e4048ee837494aea3c21a28ad5fc080994dfba5b036cf84de37f7ad5074"},
{file = "rpds_py-0.20.0-pp39-pypy39_pp73-musllinux_1_2_i686.whl", hash = "sha256:faefcc78f53a88f3076b7f8be0a8f8d35133a3ecf7f3770895c25f8813460f08"},
{file = "rpds_py-0.20.0-pp39-pypy39_pp73-musllinux_1_2_x86_64.whl", hash = "sha256:5b4f105deeffa28bbcdff6c49b34e74903139afa690e35d2d9e3c2c2fba18cec"},
{file = "rpds_py-0.20.0-pp39-pypy39_pp73-win_amd64.whl", hash = "sha256:fdfc3a892927458d98f3d55428ae46b921d1f7543b89382fdb483f5640daaec8"},
{file = "rpds_py-0.20.0.tar.gz", hash = "sha256:d72a210824facfdaf8768cf2d7ca25a042c30320b3020de2fa04640920d4e121"},
]
[[package]]
name = "simplesat"
version = "0.8.2"
description = "Simple SAT solvers for use in Enstaller"
optional = false
python-versions = "*"
files = [
{file = "simplesat-0.8.2-py2.py3-none-any.whl", hash = "sha256:76dd637db54c998badb988baafbc2bd4cc6689364580588487bc2634a6ab55fd"},
{file = "simplesat-0.8.2.tar.gz", hash = "sha256:1943f32735b03b048e20953a0145b2b61d2eb7a9dcc471a74f214afe9fa8d858"},
]
[package.dependencies]
attrs = ">=17.4.0"
okonomiyaki = ">=0.16.6"
six = ">=1.10.0"
[[package]]
name = "six"
version = "1.16.0"
description = "Python 2 and 3 compatibility utilities"
optional = false
python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*"
files = [
{file = "six-1.16.0-py2.py3-none-any.whl", hash = "sha256:8abb2f1d86890a2dfb989f9a77cfcfd3e47c2a354b01111771326f8aa26e0254"},
{file = "six-1.16.0.tar.gz", hash = "sha256:1e61c37477a1626458e36f7b1d82aa5c9b094fa4802892072e49de9c60c4c926"},
]
[[package]]
name = "wheel"
version = "0.41.2"
description = "A built-package format for Python"
optional = false
python-versions = ">=3.7"
files = [
{file = "wheel-0.41.2-py3-none-any.whl", hash = "sha256:75909db2664838d015e3d9139004ee16711748a52c8f336b52882266540215d8"},
{file = "wheel-0.41.2.tar.gz", hash = "sha256:0c5ac5ff2afb79ac23ab82bab027a0be7b5dbcf2e54dc50efe4bf507de1f7985"},
]
[package.extras]
test = ["pytest (>=6.0.0)", "setuptools (>=65)"]
[[package]]
name = "zipfile2"
version = "0.0.12"
description = "An improved ZipFile class."
optional = false
python-versions = "*"
files = [
{file = "zipfile2-0.0.12-py2.py3-none-any.whl", hash = "sha256:b9adf577d825461480e485027116c035f666b72ac3911af71aa93da6e0579eb8"},
{file = "zipfile2-0.0.12.tar.gz", hash = "sha256:7376f7c968717ac895ef862da913e790cf1b518caf56c4822c04684c46a8a608"},
]
[metadata]
lock-version = "2.0"
python-versions = "^3.10"
content-hash = "77df0bf8de469f836b38ed006e00b9e70ed430601f2561999dd41b83ea5a22d6"

26
dv/formal/pyproject.toml Normal file
View file

@ -0,0 +1,26 @@
# Copyright lowRISC contributors.
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
# SPDX-License-Identifier: Apache-2.0
[tool.poetry]
name = "ibex"
version = "0.0.0"
description = "Ibex"
authors = []
license = "Apache 2.0"
readme = "README.md"
[tool.poetry.dependencies]
python = "^3.10"
packaging = "23.1"
anytree = "2.8.0"
hjson = "3.1.0"
mako = "1.1.6"
pyyaml = "6.0"
wheel = "0.41.2"
edalize = { git = "https://github.com/lowRISC/edalize.git", tag = "v0.4.0"}
fusesoc = { git = "https://github.com/lowRISC/fusesoc.git", tag = "ot-0.4" }
[build-system]
requires = ["poetry-core"]
build-backend = "poetry.core.masonry.api"

28
dv/formal/spec/fix_pmp_bug.py Normal file
View 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
View 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
View 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[2];
logic [31:0] rX_sail_invoke_ret[2];
logic [63:0] rX_sail_invoke_arg_0[2];
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[1];
logic [63:0] wX_sail_invoke_arg_0[1];
logic [31:0] wX_sail_invoke_arg_1[1];
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[2];
logic [31:0] write_ram_sail_invoke_arg_1[2];
logic [31:0] write_ram_sail_invoke_arg_2[2];
logic [3:0] write_ram_sail_invoke_arg_3[2];
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[2];
logic [31:0] read_ram_sail_invoke_ret[2];
logic [31:0] read_ram_sail_invoke_arg_1[2];
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[64];
logic [31:0] pmpaddr_n_in[64];
t_Pmpcfg_ent pmpcfg_n_out[64];
logic [31:0] pmpaddr_n_out[64];
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
View 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
View 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
View 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
View 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
View 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)

241
dv/formal/verify.tcl Normal file
View file

@ -0,0 +1,241 @@
# 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
# Load all Ibex RTL, using the filelist generated by fusesoc
analyze -sv12 +define+SYNTHESIS -f_relative_to_file_location build/fusesoc/default-vcs/lowrisc_ibex_ibex_formal_0.1.scr
set sail_lib_dir $env(LOWRISC_SAIL_SRC)/lib/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

378
flake.lock generated Normal file
View file

@ -0,0 +1,378 @@
{
"nodes": {
"flake-utils": {
"inputs": {
"systems": "systems"
},
"locked": {
"lastModified": 1710146030,
"narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
"owner": "numtide",
"repo": "flake-utils",
"rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
"type": "github"
},
"original": {
"owner": "numtide",
"repo": "flake-utils",
"type": "github"
}
},
"gomod2nix": {
"inputs": {
"flake-utils": [
"psgen",
"flake-utils"
],
"nixpkgs": [
"psgen",
"nixpkgs"
]
},
"locked": {
"lastModified": 1717050755,
"narHash": "sha256-C9IEHABulv2zEDFA+Bf0E1nmfN4y6MIUe5eM2RCrDC0=",
"owner": "tweag",
"repo": "gomod2nix",
"rev": "31b6d2e40b36456e792cd6cf50d5a8ddd2fa59a1",
"type": "github"
},
"original": {
"owner": "tweag",
"repo": "gomod2nix",
"type": "github"
}
},
"lowrisc-nix": {
"inputs": {
"flake-utils": [
"flake-utils"
],
"nixpkgs": [
"nixpkgs"
],
"poetry2nix": "poetry2nix",
"rust-overlay": "rust-overlay"
},
"locked": {
"lastModified": 1724163813,
"narHash": "sha256-jdVhaKwR39AqQcSIe2euQkZwsu88qRcjsehO57tchVA=",
"owner": "lowrisc",
"repo": "lowrisc-nix",
"rev": "7412a5a201df3e5837b42a9b831bdf5bb9105a3b",
"type": "github"
},
"original": {
"owner": "lowrisc",
"repo": "lowrisc-nix",
"type": "github"
}
},
"lowrisc_sail": {
"flake": false,
"locked": {
"lastModified": 1719847350,
"narHash": "sha256-KOjNg6Av//KLp4/aQEIVCe157ac90lyZ6CZArPIWL8o=",
"owner": "lowrisc",
"repo": "sail",
"rev": "3f317060d2800c88432cc1309255a7c674bcab41",
"type": "github"
},
"original": {
"owner": "lowrisc",
"ref": "lowrisc",
"repo": "sail",
"type": "github"
}
},
"lowrisc_sail_riscv": {
"flake": false,
"locked": {
"lastModified": 1722338144,
"narHash": "sha256-ALWgTa/AxCnHJlK/RSZ6856xK2lwHc6CzHGtf4d8C0s=",
"owner": "lowrisc",
"repo": "sail-riscv",
"rev": "81a266b6f65365b34180af7b91708265da653878",
"type": "github"
},
"original": {
"owner": "lowrisc",
"ref": "81a266b6f65365b34180af7b91708265da653878",
"repo": "sail-riscv",
"type": "github"
}
},
"mkshell-minimal": {
"locked": {
"lastModified": 1700988624,
"narHash": "sha256-KJyiF67zVYOBkNltKhJATfSj+gfRFX9dSFIWDEBy2nQ=",
"owner": "viperML",
"repo": "mkshell-minimal",
"rev": "6b0868be06da900b5fe6ece05616b84e3cbd7944",
"type": "github"
},
"original": {
"owner": "viperML",
"repo": "mkshell-minimal",
"type": "github"
}
},
"nix-github-actions": {
"inputs": {
"nixpkgs": [
"lowrisc-nix",
"poetry2nix",
"nixpkgs"
]
},
"locked": {
"lastModified": 1703863825,
"narHash": "sha256-rXwqjtwiGKJheXB43ybM8NwWB8rO2dSRrEqes0S7F5Y=",
"owner": "nix-community",
"repo": "nix-github-actions",
"rev": "5163432afc817cf8bd1f031418d1869e4c9d5547",
"type": "github"
},
"original": {
"owner": "nix-community",
"repo": "nix-github-actions",
"type": "github"
}
},
"nix-github-actions_2": {
"inputs": {
"nixpkgs": [
"poetry2nix",
"nixpkgs"
]
},
"locked": {
"lastModified": 1703863825,
"narHash": "sha256-rXwqjtwiGKJheXB43ybM8NwWB8rO2dSRrEqes0S7F5Y=",
"owner": "nix-community",
"repo": "nix-github-actions",
"rev": "5163432afc817cf8bd1f031418d1869e4c9d5547",
"type": "github"
},
"original": {
"owner": "nix-community",
"repo": "nix-github-actions",
"type": "github"
}
},
"nixpkgs": {
"locked": {
"lastModified": 1724316499,
"narHash": "sha256-Qb9MhKBUTCfWg/wqqaxt89Xfi6qTD3XpTzQ9eXi3JmE=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "797f7dc49e0bc7fab4b57c021cdf68f595e47841",
"type": "github"
},
"original": {
"id": "nixpkgs",
"ref": "nixos-24.05",
"type": "indirect"
}
},
"poetry2nix": {
"inputs": {
"flake-utils": [
"lowrisc-nix",
"flake-utils"
],
"nix-github-actions": "nix-github-actions",
"nixpkgs": [
"lowrisc-nix",
"nixpkgs"
],
"systems": "systems_2",
"treefmt-nix": "treefmt-nix"
},
"locked": {
"lastModified": 1723854676,
"narHash": "sha256-+BrHfNuXrqeE7PoV6xDaoh0joYiJkvTTCIV0fFR3THw=",
"owner": "nix-community",
"repo": "poetry2nix",
"rev": "d650118bce34c0238b9b54f23f7f173f9e4db867",
"type": "github"
},
"original": {
"owner": "nix-community",
"repo": "poetry2nix",
"type": "github"
}
},
"poetry2nix_2": {
"inputs": {
"flake-utils": [
"flake-utils"
],
"nix-github-actions": "nix-github-actions_2",
"nixpkgs": [
"nixpkgs"
],
"systems": "systems_3",
"treefmt-nix": "treefmt-nix_2"
},
"locked": {
"lastModified": 1724417163,
"narHash": "sha256-gD0N0pnKxWJcKtbetlkKOIumS0Zovgxx/nMfOIJIzoI=",
"owner": "nix-community",
"repo": "poetry2nix",
"rev": "7619e43c2b48c29e24b88a415256f09df96ec276",
"type": "github"
},
"original": {
"owner": "nix-community",
"repo": "poetry2nix",
"type": "github"
}
},
"psgen": {
"inputs": {
"flake-utils": [
"flake-utils"
],
"gomod2nix": "gomod2nix",
"nixpkgs": [
"nixpkgs"
]
},
"locked": {
"lastModified": 1723038779,
"narHash": "sha256-L/toJC6lyeVJy2Uswse8aCrhdt0mTxDfn8t0NpNVn/I=",
"owner": "mndstrmr",
"repo": "psgen",
"rev": "2d0c1e0690cf6c3b9b1bf4f51bccab4698f4e21f",
"type": "github"
},
"original": {
"owner": "mndstrmr",
"repo": "psgen",
"type": "github"
}
},
"root": {
"inputs": {
"flake-utils": "flake-utils",
"lowrisc-nix": "lowrisc-nix",
"lowrisc_sail": "lowrisc_sail",
"lowrisc_sail_riscv": "lowrisc_sail_riscv",
"mkshell-minimal": "mkshell-minimal",
"nixpkgs": "nixpkgs",
"poetry2nix": "poetry2nix_2",
"psgen": "psgen"
}
},
"rust-overlay": {
"inputs": {
"nixpkgs": [
"lowrisc-nix",
"nixpkgs"
]
},
"locked": {
"lastModified": 1724034091,
"narHash": "sha256-b1g7w0sw+MDAhUAeCoX1vlTghsqcDZkxr+k9OZmxPa8=",
"owner": "oxalica",
"repo": "rust-overlay",
"rev": "c7d36e0947826e0751a5214ffe82533fbc909bc0",
"type": "github"
},
"original": {
"owner": "oxalica",
"repo": "rust-overlay",
"type": "github"
}
},
"systems": {
"locked": {
"lastModified": 1681028828,
"narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
"owner": "nix-systems",
"repo": "default",
"rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
"type": "github"
},
"original": {
"owner": "nix-systems",
"repo": "default",
"type": "github"
}
},
"systems_2": {
"locked": {
"lastModified": 1681028828,
"narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
"owner": "nix-systems",
"repo": "default",
"rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
"type": "github"
},
"original": {
"id": "systems",
"type": "indirect"
}
},
"systems_3": {
"locked": {
"lastModified": 1681028828,
"narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
"owner": "nix-systems",
"repo": "default",
"rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
"type": "github"
},
"original": {
"id": "systems",
"type": "indirect"
}
},
"treefmt-nix": {
"inputs": {
"nixpkgs": [
"lowrisc-nix",
"poetry2nix",
"nixpkgs"
]
},
"locked": {
"lastModified": 1719749022,
"narHash": "sha256-ddPKHcqaKCIFSFc/cvxS14goUhCOAwsM1PbMr0ZtHMg=",
"owner": "numtide",
"repo": "treefmt-nix",
"rev": "8df5ff62195d4e67e2264df0b7f5e8c9995fd0bd",
"type": "github"
},
"original": {
"owner": "numtide",
"repo": "treefmt-nix",
"type": "github"
}
},
"treefmt-nix_2": {
"inputs": {
"nixpkgs": [
"poetry2nix",
"nixpkgs"
]
},
"locked": {
"lastModified": 1719749022,
"narHash": "sha256-ddPKHcqaKCIFSFc/cvxS14goUhCOAwsM1PbMr0ZtHMg=",
"owner": "numtide",
"repo": "treefmt-nix",
"rev": "8df5ff62195d4e67e2264df0b7f5e8c9995fd0bd",
"type": "github"
},
"original": {
"owner": "numtide",
"repo": "treefmt-nix",
"type": "github"
}
}
},
"root": "root",
"version": 7
}

159
flake.nix Normal file
View file

@ -0,0 +1,159 @@
# Copyright lowRISC contributors.
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
# SPDX-License-Identifier: Apache-2.0
{
description = "Nix Flake for Ibex development and testing.";
inputs = {
nixpkgs.url = "nixpkgs/nixos-24.05";
flake-utils.url = "github:numtide/flake-utils";
poetry2nix = {
url = "github:nix-community/poetry2nix";
inputs.nixpkgs.follows = "nixpkgs";
inputs.flake-utils.follows = "flake-utils";
};
mkshell-minimal.url = "github:viperML/mkshell-minimal";
lowrisc-nix = {
url = "github:lowrisc/lowrisc-nix";
inputs.nixpkgs.follows = "nixpkgs";
inputs.flake-utils.follows = "flake-utils";
};
psgen = {
url = "github:mndstrmr/psgen";
inputs.nixpkgs.follows = "nixpkgs";
inputs.flake-utils.follows = "flake-utils";
};
lowrisc_sail = {
url = "github:lowrisc/sail?ref=lowrisc";
flake = false;
};
lowrisc_sail_riscv = {
url = "github:lowrisc/sail-riscv?ref=81a266b6f65365b34180af7b91708265da653878";
flake = false;
};
};
# The lowRISC public nix-cache contains builds of nix packages used by lowRISC, primarily coming from github:lowRISC/lowrisc-nix.
nixConfig = {
extra-substituters = ["https://nix-cache.lowrisc.org/public/"];
extra-trusted-public-keys = ["nix-cache.lowrisc.org-public-1:O6JLD0yXzaJDPiQW1meVu32JIDViuaPtGDfjlOopU7o="];
};
outputs = inputs@{self, ...}:
let
# System types to support.
supportedSystems = with inputs.flake-utils.lib.system; [
x86_64-linux
];
# The .#formal shellHook always checks for jg on the path.
# Should we check for a given version of the tool as well?
check_jg_version = false;
expected_jaspergold_version = "2021.12 FCS 64 bits";
in inputs.flake-utils.lib.eachSystem supportedSystems (system:
let
pkgs = import inputs.nixpkgs {
inherit system;
};
inherit (pkgs) lib;
mkshell-minimal = inputs.mkshell-minimal pkgs;
# lowRISC fork of the Sail repository. The SAIL -> SV flow is used to generate the reference model.
lowrisc_sail = import ./nix/lowrisc_sail.nix {
inherit pkgs;
src = inputs.lowrisc_sail;
};
# RISCV Sail model with changes for Ibex
lowrisc_sail_riscv.src = (import ./nix/lowrisc_sail_riscv.nix {
inherit pkgs;
src = inputs.lowrisc_sail_riscv;
}).src;
# Create a python package set suitable for the formal flow
# - The file dv/formal/pyproject.toml defines the package set for this environment
# - Using the fusesoc .core files in this repo requires a lowrisc-fork of fusesoc, so this
# file specifies the forked repository. Most other python package dependencies are in
# support of fusesoc.
formal_python_env = let
poetry2nix = inputs.poetry2nix.lib.mkPoetry2Nix {inherit pkgs;};
lowriscPoetryOverrides = inputs.lowrisc-nix.lib.poetryOverrides {inherit pkgs;};
in
poetry2nix.mkPoetryEnv {
projectDir = ./dv/formal;
overrides = [
lowriscPoetryOverrides
poetry2nix.defaultPoetryOverrides
];
};
in {
packages = {
# Export the package for the lowrisc fork of the sail compiler. This allows us
# to re-use its build environment.
inherit lowrisc_sail;
};
devShells = rec {
formal = mkshell-minimal {
packages = [
inputs.psgen.packages.${system}.default
lowrisc_sail
formal_python_env
] ++ (with pkgs; [
gnumake
patch
]);
shellHook = let
# The formal environment has an untracked external requirement on Cadence JasperGold.
# Add a check here which will prevent launching the devShell if JasperGold is not found on the user's path.
# TODO: Is this robust? Do we want to check available features?
check_jg = ''
if ! command -v jg &>/dev/null; then
echo "JasperGold not found on path. Not launching devShell."
exit 1
fi
'' + lib.optionalString check_jg_version ''
jg_version=$(jg -version -allow_unsupported_OS)
if [[ $jg_version != "${expected_jaspergold_version}" ]]; then
echo "Incorrect JasperGold version found on path."
echo "Expected \"${expected_jaspergold_version}\", Got \"$jg_version\"."
echo "Not launching devShell."
exit 1
fi
'';
in ''
${check_jg}
# The following environment variables are used by the formal build scripts to pick up the locations
# of the external source-file dependencies.
# The can be re-exported manually for development (see .#formal-dev)
export LOWRISC_SAIL_SRC=${lowrisc_sail.src}
export LOWRISC_SAIL_RISCV_SRC=${lowrisc_sail_riscv.src}
'';
};
formal-dev = formal.overrideAttrs (prev: {
shellHook = prev.shellHook + ''
cat << EOF
======================================================================================
This is a development shell, by default it is identical to the full formal shell.
In order to use a local version of psgen or Sail, just prepend to the current path now:
export PATH=<dirname>:\$PATH
For updates to Sail also update LOWRISC_SAIL_SRC:
export LOWRISC_SAIL_SRC=<dirname>
In order to use a local version of sail-riscv update LOWRISC_SAIL_RISCV_SRC:
export LOWRISC_SAIL_RISCV_SRC=<dirname>
======================================================================================
EOF
'';
});
};
}
);
}

1
lint/verible_waiver.vbw Normal file
View file

@ -0,0 +1 @@
waive --rule=module-port --location="spec_instance.sv"

23
nix/lowrisc_sail.nix Normal file
View file

@ -0,0 +1,23 @@
# Copyright lowRISC contributors.
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
# SPDX-License-Identifier: Apache-2.0
# Override the upstream sail package definition to use the lowRISC fork
{
pkgs,
src,
}:
pkgs.ocamlPackages.sail.overrideAttrs (prev: {
pname = "lowrisc_sail";
inherit src;
# The lowRISC fork is older than upstream, and requires additional dependencies
# from those specified upsteam to build. Add them here.
propagatedBuildInputs =
prev.propagatedBuildInputs ++ (with pkgs.ocamlPackages; [
menhirLib
]) ++ (with pkgs; [
z3
]);
})

18
nix/lowrisc_sail_riscv.nix Normal file
View file

@ -0,0 +1,18 @@
# Copyright lowRISC contributors.
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
# SPDX-License-Identifier: Apache-2.0
# RISCV Sail model with changes for Ibex
{
pkgs,
src,
}:
pkgs.sail-riscv-rv32.overrideAttrs {
pname = "lowrisc_sail_riscv";
inherit src;
# The upstream patches does not apply to our older version of riscv_sail.
patches = [ ];
}