[dv/formal] Remove buildspec.py

buildspec.py previously allowed us to cut out specific instructions from
the specification, this allowed for faster build times and so a tighter
feedback loop.

Now, building and elaborating the Sail specification is fast enough that
this is no longer necessary.

We can therefore remove `ISS_instr and {ex,wbexc}_is_pres_instr, as
weel as instrs.json.

Also renames Sources.mk to sail-sources.mk for clarity.

Author: mndstrmr

dv/formal/Makefile

@@ -4,7 +4,7 @@ SAIL=sail
 
 SAIL_RISCV_MODEL_DIR=${LOWRISC_SAIL_RISCV_SRC}/model
 
-include Sources.mk
+include sail-sources.mk
 
 PSGEN_SRCS=thm/btype.proof thm/ibex.proof thm/mem.proof thm/riscv.proof
 PSGEN_FLAGS=-root riscv -task

dv/formal/buildspec.py

@@ -4,8 +4,6 @@
 // Original author: Louis-Emile Ploix
 // SPDX-License-Identifier: Apache-2.0
 
-`include "../build/ibexspec_instrs.sv"
-
 `ifndef CMP_INSNS
 `define CMP_INSNS
 
@@ -21,25 +19,12 @@
     `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) \
@@ -55,54 +40,27 @@
 `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)
@@ -114,38 +72,14 @@
 `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

dv/formal/check/encodings.sv

@@ -11,10 +11,6 @@ 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;
 
@@ -29,15 +25,12 @@ 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_btype = `IS_BTYPE;
+assign ex_is_jump = `IS_JAL | `IS_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;
+assign ex_is_mtype = ex_is_div | `IS_MUL | `IS_MULH | `IS_MULHSH | `IS_MULHU;
 `undef INSTR
 
 // real_write checks that there is a write and the dest reg is not x0
@@ -59,8 +52,6 @@ Select CSRs based on the current state of the follower, in particular:
 - 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;

dv/formal/check/peek/compare_helper.sv

@@ -196,10 +196,9 @@ logic [31:0] pre_mip;
 //  - 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_wfi, ex_is_rtype, ex_is_div, ex_is_mtype;
+logic ex_is_btype, ex_is_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;
@@ -221,9 +220,7 @@ 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_load_instr, wbexc_is_store_instr, wbexc_is_mem_instr;
 logic wbexc_is_wfi;
 
 logic [31:0] ex_compressed_instr;
@@ -233,7 +230,7 @@ logic ex_has_compressed_instr;
 logic wbexc_post_int_err; // Spec had an internal error
 
 logic [31:0] wbexc_post_wX;
-logic [5:0] wbexc_post_wX_addr;
+logic [4:0] wbexc_post_wX_addr;
 logic wbexc_post_wX_en;
 
 `define X(n) wbexc_post_``n
@@ -432,13 +429,6 @@ assign ex_is_checkable_csr = ~(
   (`CSR_ADDR == CSR_MCOUNTINHIBIT)
 );
 
-`undef INSTR
-`define INSTR wbexc_decompressed_instr
-
-// Illegal instructions aren't 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 //////////////////////