On a hunch, do some CSR experiments with IRQs to find failing traces …

…(and create assumptions/masks to fix them).

tests/formal/checks.cfg

@@ -6,8 +6,10 @@ isa rv32i
 # to check assumptions), probably for little gain. Neverless, allow the
 # possibility for running long tests.
 full
-# Group for experimenting with IRQ line. Not currently used (in particular,
-# my intended use-case of "irq_cover" creates a BMC, not a cover check.)
+# Group for experimenting with IRQ line. Used for any group where I've
+# determined that IRQs make a difference when extending depth.
+# TODO: "irq_cover", one of my intended use-cases, creates a BMC, not a cover
+# check.
 irq
 
 [depth]
@@ -19,6 +21,7 @@ full_insn_sll        80
 full_insn_srl        80
 full_insn_sra        80
 reg       15    25
+# reg       5    32  # Takes a long time!
 pc_fwd    10    30
 pc_bwd    10    30
 liveness  1  12 39
@@ -34,12 +37,19 @@ csrc_any  1     20
 csrc_zero  1     20
 csrc_const  1     20
 
+irq_csrw            27
+irq_csr_ill         27
+irq_csrw_misa       27
+irq_csrc_any  1     27
+irq_csrc_zero  1     27
+irq_csrc_const  1     27
+
 [csrs]
 mscratch any
 mcause
 mip zero_mask="32'h0000F7FF"
 mie zero_mask="32'h0000F7FF"
-mstatus const="32'h0001800"_mask="32'hFFFFFFF7"
+mstatus const="32'h0001800"_mask="32'hFFFFFF77"  # mret sets MPIE to 1!
 mtvec zero_mask="32'h00000003"
 mepc zero_mask="32'h00000003"
 # Read-only zero registers
@@ -84,6 +94,13 @@ eff     m       rw
 // external ints are disabled for checking MIP.
 always @* assume((rvfi_csr_mip_rdata & 32'h00000800) == 0);
 
+[assume !irq_csrw]
+// RV formal cannot presently handle external/async interrupts, so repeat
+// the logic here. When this can be removed, the !csrw_mip line should remain.
+// Default csrw tests don't need this because 20 cycles isn't enough to
+// start the interrupt handler.
+always @* assume((rvfi_csr_mip_rdata & 32'h00000800) == 0);
+
 [defines]
 `define RISCV_FORMAL_ALIGNED_MEM