Formal cleanup

.github/workflows/pr_lint.yml

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

CREDITS.md

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

dv/formal/.gitignore

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

dv/formal/Makefile

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

dv/formal/Sources.mk

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

dv/formal/buildspec.py

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

dv/formal/check/encodings.sv

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