[dv/formal] Memory protocol rearranged

This commit has no functional changes, but it just rewrites the
mem_assume_t interface to improve clarity.
It also puts the error assumption inside the interface instead of
outside.

dv/formal/check/protocol/mem.sv

@@ -11,39 +11,47 @@ In this case all responses must be within bounded time (`TIME_BOUND cycles). Rem
 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 clk_i,
+    input logic rst_ni,
+
     input logic req_o,
     input logic gnt_i,
-    input logic rvalid_i
+    input logic rvalid_i,
+    input logic err_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;
+        if (~rst_ni) begin
+            outstanding_reqs_q <= 0;
+        end else begin
+            outstanding_reqs_q <= outstanding_reqs;
+        end
     end
 
+    // Sail does not specify what happens on bus errors.
+    NoErr: assume property (@(posedge clk_i) ~err_i);
+
     // 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);
+    MemValidBounded: assume property (@(posedge clk_i) outstanding_reqs_q == 8'b0 |-> ~rvalid_i);
     // 2. Grants can only be sent when they are requested
-    MemGntOnRequest: assume property (~req_o |-> ~gnt_i);
+    MemGntOnRequest: assume property (@(posedge clk_i) ~req_o |-> ~gnt_i);
 
     // Grants must respond within TIME_LIMIT cycles
-    GntBound: assume property (req_o |-> ##[0:`TIME_LIMIT] gnt_i);
+    GntBound: assume property (@(posedge clk_i) 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);
+    MemValidTimer: assume property (
+      @(posedge clk_i)
+      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);
+    // MemGntEventually: assume property (@(posedge clk_i) 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);

dv/formal/check/top.sv

@@ -15,6 +15,8 @@ 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"
+// Abstract memory interface definition.
+`include "protocol/mem.sv"
 
 `define CR ibex_top_i.u_ibex_core
 `define CSR `CR.cs_registers_i
@@ -471,7 +473,23 @@ ibex_compressed_decoder decompression_assertion_decoder_2(
 
 ////////////////////// IRQ + Memory Protocols //////////////////////
 `include "protocol/irqs.sv"
-`include "protocol/mem.sv"
+
+mem_assume_t instr_mem_assume(
+    .clk_i    (clk_i),
+    .rst_ni   (rst_ni),
+    .req_o    (instr_req_o),
+    .gnt_i    (instr_gnt_i),
+    .rvalid_i (instr_rvalid_i),
+    .err_i    (instr_err_i)
+);
+mem_assume_t data_mem_assume(
+    .clk_i    (clk_i),
+    .rst_ni   (rst_ni),
+    .req_o    (data_req_o),
+    .gnt_i    (data_gnt_i),
+    .rvalid_i (data_rvalid_i),
+    .err_i    (data_err_i)
+);
 
 ////////////////////// Following //////////////////////
 `include "peek/abs.sv" // Abstract state