Add some basic protocol checking to the icache's RAM interface

Since we are binding in an interface anyway, we can add some SV
assertions to make sure nothing too strange is happening.

Note that they aren't as strong as you might expect: we don't check
that rdata isn't X, for example. This is because the cache makes
speculative reads, which it (hopefully) ignores if the data is
invalid.

dv/uvm/icache/dv/ibex_icache_ecc_agent/ibex_icache_ecc_agent.core

@@ -9,8 +9,10 @@ filesets:
     depend:
       - lowrisc:dv:dv_utils
       - lowrisc:dv:dv_lib
+      - lowrisc:prim:assert
     files:
       - ibex_icache_ecc_if.sv
+      - ibex_icache_ecc_protocol_checker.sv
       - ibex_icache_ecc_agent_pkg.sv
       - ibex_icache_ecc_item.sv: {is_include_file: true}
       - ibex_icache_ecc_bus_item.sv: {is_include_file: true}

dv/uvm/icache/dv/ibex_icache_ecc_agent/ibex_icache_ecc_if.sv

@@ -10,9 +10,15 @@ interface ibex_icache_ecc_if
    input logic          write_i,
    input logic [31:0]   width,
    input logic [31:0]   addr,
+   input logic [127:0]  wdata,
+   input logic [127:0]  wmask,
    input logic [127:0]  rdata,
+
    output logic [127:0] bad_bit_mask);
 
+  // SVA module
+  ibex_icache_ecc_protocol_checker checker_i (.*);
+
   // The address for the last monitored req transaction
   logic [31:0]  last_addr = 'x;
 

dv/uvm/icache/dv/ibex_icache_ecc_agent/ibex_icache_ecc_protocol_checker.sv

@@ -0,0 +1,37 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+// An interface that contains SV assertions to check that the icache <-> SRAM interface is being
+// driven correctly.
+//
+// This should be instantiated inside ibex_icache_ecc_if. The input names are the same as the
+// signals in the interface (no _i suffix), so that this can be instantiated with .*
+
+`include "prim_assert.sv"
+
+interface ibex_icache_ecc_protocol_checker
+  (input logic         clk_i,
+   input logic         req_i,
+   input logic         write_i,
+   input logic [31:0]  width,
+   input logic [31:0]  addr,
+   input logic [127:0] wdata,
+   input logic [127:0] wmask,
+   input logic [127:0] rdata);
+
+  // The req line should never be unknown. Note that we have no reset signal here, so we assert this
+  // is true at all times (fortunately, it seems that the DUT holds req low when in reset).
+  `ASSERT_KNOWN(ReqKnown, req_i, clk_i, 0)
+
+  // If there is a request, the write signal should be known
+  `ASSERT_KNOWN_IF(WriteKnown, write_i, req_i, clk_i, 0)
+
+  // If there is a request with write_i high, the address and write mask should be known, and so
+  // should any data to be written. We don't require the address to be known for reads: reading
+  // rubbish is fine, so long as we ignore it later.
+  `ASSERT_KNOWN_IF(AddrKnown,  addr,          req_i & write_i, clk_i, 0)
+  `ASSERT_KNOWN_IF(WMaskKnown, wmask,         req_i & write_i, clk_i, 0)
+  `ASSERT_KNOWN_IF(WDataKnown, wdata & wmask, req_i & write_i, clk_i, 0)
+
+endinterface

dv/uvm/icache/dv/prim_badbit/prim_badbit_ram_1p.sv

@@ -63,10 +63,12 @@ module prim_badbit_ram_1p #(
   logic [31:0] width;
   assign width = Width;
 
-  // Similarly, extend addr and sram_rdata (the un-fiddled value)
+  // Similarly, extend addr, wdata, wmask and sram_rdata (the un-fiddled value)
   logic [31:0]  addr;
-  logic [127:0] rdata;
+  logic [127:0] wdata, wmask, rdata;
   assign addr  = {{32-Aw{1'b0}}, addr_i};
+  assign wdata = {{128-Width{1'b0}}, wdata_i};
+  assign wmask = {{128-Width{1'b0}}, wmask_i};
   assign rdata = {{128-Width{1'b0}}, sram_rdata};
 
   // To inject errors, bind in an interface with bad_bit_mask as an output and assign one of the

rtl/ibex_icache.sv

@@ -1015,4 +1015,8 @@ module ibex_icache #(
   `ASSERT_INIT(ecc_tag_param_legal, (TAG_SIZE <= 27))
   `ASSERT_INIT(ecc_data_param_legal, (LineSize <= 121))
 
+  // Lookups in the tag ram should always give a known result
+  `ASSERT_KNOWN(TagHitKnown,     lookup_valid_ic1 & tag_hit_ic1)
+  `ASSERT_KNOWN(TagInvalidKnown, lookup_valid_ic1 & tag_invalid_ic1)
+
 endmodule