[dv/formal] Remove -fun2wires 2:rX

Previously we used -fun2wires 2:rX so that we could track which registers
were being used. This was leading to combinational loops, and so had
already been removed from CHERIoT-Ibex. We can still 'track' them using
Ibex's own interpretation of which registers are relevant, and marking
the rest as x.

Author: mndstrmr

dv/formal/Makefile

@@ -11,12 +11,19 @@ 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 \
+# -sv, use the SystemVerilog backend
+# --sv-comb, generate a always_comb instead of an initial block
+# --sv-inregs --sv-outregs, produce inputs and outputs for every Sail register
+# --sv-nostrings, --sv-nopacked, --sv-nomem, avoid generating some things Jasper doesn't like (FIXME: --sv-nopacked might be better removed?)
+# -Oconstrant_fold, do basic optimisation
+# -memo-z3, resolving types requires a sat solver, this helps speed up those queries
+# --sv-unreachable, remove the implementations of functions to either make the design smaller or avoid recursion loops (FIXME: Still necessary?)
+# --sv-fun2wires (n:)?f, transform a function into ports, with n (or 1) slots
+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 
 
 # 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.

dv/formal/check/spec_instance.sv

@@ -19,20 +19,33 @@ always_comb begin
     else main_mode = MAIN_IDEX;
 end
 
+// Some registers are not driven. Only those that have reg_driven[i] high are
+// given real values, the rest are left free (i.e. the spec cannot depend on
+// them). For wraparound purposes it does not matter what reg_driven[i] is:
+// - If too many registers are driven they all must pass checks anyway (since
+// they are checked as inputs)
+// - If too few registers are driven instructions will fail to be spec
+// conformant
+// Note that while it again does not matter how they are defined, but only
+// registers matching one of `CR.rf_raddr_{a, b} can be driven.
+
+logic [31:0] reg_driven;
+assign reg_driven[0] = 1'b0;
+
+for (genvar i = 1; i < 32; i++) begin: g_regs_cut
+    logic [31:0] free; // Undriven
+    assign reg_driven[i] = (`CR.rf_raddr_a == i && `CR.rf_ren_a) || (`CR.rf_raddr_b == i && `CR.rf_ren_b);
+    assign pre_regs_cut[i] = reg_driven[i] ? pre_regs[i] : free;
+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),
+    .regs_i(pre_regs_cut),
 
     .wx_o(spec_post_wX),
     .wx_addr_o(spec_post_wX_addr),

dv/formal/check/top.sv

@@ -179,6 +179,7 @@ WFIStart: assume property (`IDC.ctrl_fsm_cs == SLEEP |-> (
 
 // Pre state is the architectural state of Ibex at the start of the cycle
 logic [31:0] pre_regs[32];
+logic [31:0] pre_regs_cut[31:1];
 logic [31:0] pre_nextpc;
 logic [31:0] pre_mip;
 
@@ -313,17 +314,6 @@ logic wbexc_handling_irq; // Check the results of handling an IRQ
 
 ////////////////////// 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;

dv/formal/spec/spec_api.sv

@@ -23,12 +23,7 @@ module spec_api #(
 ) (
     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,
+    input [31:0] regs_i [31:1],
 
     output logic wx_en_o,
     output logic [31:0] wx_o,
@@ -99,16 +94,6 @@ module spec_api #(
     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];
@@ -272,78 +257,77 @@ sail_ibexspec spec_i(
     .stvec_out(),
     .tselect_in(),
     .tselect_out(),
-    .x1_in(),
+    .mtime_in(),
+    .mtime_out(),
+
+    .x1_in(regs_i[1]),
     .x1_out(),
-    .x2_in(),
+    .x2_in(regs_i[2]),
     .x2_out(),
-    .x3_in(),
+    .x3_in(regs_i[3]),
     .x3_out(),
-    .x4_in(),
+    .x4_in(regs_i[4]),
     .x4_out(),
-    .x5_in(),
+    .x5_in(regs_i[5]),
     .x5_out(),
-    .x6_in(),
+    .x6_in(regs_i[6]),
     .x6_out(),
-    .x7_in(),
+    .x7_in(regs_i[7]),
     .x7_out(),
-    .x8_in(),
+    .x8_in(regs_i[8]),
     .x8_out(),
-    .x9_in(),
+    .x9_in(regs_i[9]),
     .x9_out(),
-    .x10_in(),
+    .x10_in(regs_i[10]),
     .x10_out(),
-    .x11_in(),
+    .x11_in(regs_i[11]),
     .x11_out(),
-    .x12_in(),
+    .x12_in(regs_i[12]),
     .x12_out(),
-    .x13_in(),
+    .x13_in(regs_i[13]),
     .x13_out(),
-    .x14_in(),
+    .x14_in(regs_i[14]),
     .x14_out(),
-    .x15_in(),
+    .x15_in(regs_i[15]),
     .x15_out(),
-    .x16_in(),
+    .x16_in(regs_i[16]),
     .x16_out(),
-    .x17_in(),
+    .x17_in(regs_i[17]),
     .x17_out(),
-    .x18_in(),
+    .x18_in(regs_i[18]),
     .x18_out(),
-    .x19_in(),
+    .x19_in(regs_i[19]),
     .x19_out(),
-    .x20_in(),
+    .x20_in(regs_i[20]),
     .x20_out(),
-    .x21_in(),
+    .x21_in(regs_i[21]),
     .x21_out(),
-    .x22_in(),
+    .x22_in(regs_i[22]),
     .x22_out(),
-    .x23_in(),
+    .x23_in(regs_i[23]),
     .x23_out(),
-    .x24_in(),
+    .x24_in(regs_i[24]),
     .x24_out(),
-    .x25_in(),
+    .x25_in(regs_i[25]),
     .x25_out(),
-    .x26_in(),
+    .x26_in(regs_i[26]),
     .x26_out(),
-    .x27_in(),
+    .x27_in(regs_i[27]),
     .x27_out(),
-    .x28_in(),
+    .x28_in(regs_i[28]),
     .x28_out(),
-    .x29_in(),
+    .x29_in(regs_i[29]),
     .x29_out(),
-    .x30_in(),
+    .x30_in(regs_i[30]),
     .x30_out(),
-    .x31_in(),
+    .x31_in(regs_i[31]),
     .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(),

dv/formal/thm/riscv.proof

@@ -172,8 +172,8 @@ lemma riscv
          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])
+    RegA: have (reg_driven[`CR.rf_raddr_a] && spec_past_has_reg[`CR.rf_raddr_a] |-> spec_past_regs[`CR.rf_raddr_a] == pre_regs_cut[`CR.rf_raddr_a])
+    RegB: have (reg_driven[`CR.rf_raddr_b] && spec_past_has_reg[`CR.rf_raddr_b] |-> spec_past_regs[`CR.rf_raddr_b] == pre_regs_cut[`CR.rf_raddr_b])
 
   # Live: have (always (##[1:157 + 2*`WFI_BOUND + 17*`TIME_LIMIT] spec_en))