diff --git a/dv/uvm/icache/dv/ibex_icache_ecc_agent/ibex_icache_ecc_agent.core b/dv/uvm/icache/dv/ibex_icache_ecc_agent/ibex_icache_ecc_agent.core
index e1f685e5..ea28be97 100644
--- a/dv/uvm/icache/dv/ibex_icache_ecc_agent/ibex_icache_ecc_agent.core
+++ b/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}
diff --git a/dv/uvm/icache/dv/ibex_icache_ecc_agent/ibex_icache_ecc_if.sv b/dv/uvm/icache/dv/ibex_icache_ecc_agent/ibex_icache_ecc_if.sv
index 85c4f322..60e671ca 100644
--- a/dv/uvm/icache/dv/ibex_icache_ecc_agent/ibex_icache_ecc_if.sv
+++ b/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;
 
diff --git a/dv/uvm/icache/dv/ibex_icache_ecc_agent/ibex_icache_ecc_protocol_checker.sv b/dv/uvm/icache/dv/ibex_icache_ecc_agent/ibex_icache_ecc_protocol_checker.sv
new file mode 100644
index 00000000..9dff1465
--- /dev/null
+++ b/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
diff --git a/dv/uvm/icache/dv/prim_badbit/prim_badbit_ram_1p.sv b/dv/uvm/icache/dv/prim_badbit/prim_badbit_ram_1p.sv
index c464b274..f7201f0b 100644
--- a/dv/uvm/icache/dv/prim_badbit/prim_badbit_ram_1p.sv
+++ b/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
diff --git a/rtl/ibex_icache.sv b/rtl/ibex_icache.sv
index 376baafd..e606a41e 100644
--- a/rtl/ibex_icache.sv
+++ b/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