Add SV assertions to icache <-> core interface in UVM testbench

This adds SVA properties for the cache <-> core interface. Rather than
pollute the actual interfaces, these are wrapped in their own
interface ("ibex_icache_core_protocol_checker").

dv/uvm/icache/dv/ibex_icache_core_agent/ibex_icache_core_agent.core

@@ -11,6 +11,7 @@ filesets:
       - lowrisc:dv:dv_lib
     files:
       - ibex_icache_core_if.sv
+      - ibex_icache_core_protocol_checker.sv
       - ibex_icache_core_agent_pkg.sv
       - ibex_icache_core_item.sv: {is_include_file: true}
       - ibex_icache_core_agent_cfg.sv: {is_include_file: true}

dv/uvm/icache/dv/ibex_icache_core_agent/ibex_icache_core_if.sv

@@ -2,7 +2,7 @@
 // Licensed under the Apache License, Version 2.0, see LICENSE for details.
 // SPDX-License-Identifier: Apache-2.0
 
-interface ibex_icache_core_if (input clk);
+interface ibex_icache_core_if (input clk, input rst_n);
 
   // Set when core is enabled (and might request instructions soon)
   logic         req;
@@ -63,6 +63,11 @@ interface ibex_icache_core_if (input clk);
     input  busy;
   endclocking
 
+
+  // SVA module
+  ibex_icache_core_protocol_checker checker_i (.*);
+
+
   // Drive the branch pin for a single cycle, redirecting the cache to the given instruction
   // address.
   task automatic branch_to(logic [31:0] addr);

dv/uvm/icache/dv/ibex_icache_core_agent/ibex_icache_core_protocol_checker.sv

@@ -0,0 +1,142 @@
+// 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 <-> core interface is being
+// driven correctly.
+//
+// This should be instantiated inside ibex_icache_core_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_core_protocol_checker (
+   input        clk,
+   input        rst_n,
+
+   input        req,
+
+   input        branch,
+   input [31:0] branch_addr,
+
+   input        ready,
+   input        valid,
+   input [31:0] rdata,
+   input [31:0] addr,
+   input        err,
+   input        err_plus2,
+
+   input        enable,
+   input        invalidate,
+
+   input        busy
+);
+
+  // The 'req' port
+  //
+  // The core may not assert 'ready' when 'req' is low. This is because 'req' means "core is not
+  // asleep"; the exact behaviour of instruction fetches in this mode is hard to characterise and we
+  // don't care about it because the core should never do it.
+  `ASSERT(NoReadyWithoutReq, !req |-> !ready, clk, !rst_n)
+
+  // The 'branch' and 'branch_addr' ports
+  //
+  // The branch signal tells the cache to redirect. There's no real requirement on when it can be
+  // asserted, but the address must be 16-bit aligned (i.e. the bottom bit must be zero).
+  `ASSERT(BranchAddrAligned, branch |-> !branch_addr[0], clk, !rst_n)
+
+  // The main instruction interface
+  //
+  // This uses a form of ready/valid handshaking, with a special rule that asserting branch_i
+  // cancels a transaction (so the cache can assert valid, but de-assert it if the core asserts
+  // branch_i).
+  //
+  // Note that the lower 16 bits of rdata must be stable, but the upper bits may change if this is a
+  // compressed instruction (which is the case if the bottom 2 bits are not 2'b11): the upper bits
+  // are then ignored by the core.
+  //
+  // There's no requirement on the core to hold ready until valid.
+  `ASSERT(ValidUntilReady, valid & ~(ready | branch) |=> valid,              clk, !rst_n);
+  `ASSERT(AddrStable,      valid & ~(ready | branch) |=> $stable(addr),      clk, !rst_n);
+  `ASSERT(ErrStable,       valid & ~(ready | branch) |=> $stable(err),       clk, !rst_n);
+  `ASSERT(Err2Stable,      valid & ~(ready | branch) |=> $stable(err_plus2), clk, !rst_n);
+
+  `ASSERT(LoRDataStable,
+          valid & ~(ready | branch) |=> $stable(rdata[15:0]),
+          clk, !rst_n);
+  `ASSERT(HiRDataStable,
+          valid & ~(ready | branch) & (rdata[1:0] == 2'b11) |=> $stable(rdata[15:0]),
+          clk, !rst_n);
+
+  // The core is never allowed to make a fetch from the cache when the PC is not known. To set the
+  // PC, it must issue a branch. Obviously, that means the core must branch before the first fetch
+  // after reset. Less obviously, it also means the core must branch immediately after an error
+  // (because the next PC depends on the fetched data).
+  //
+  // Rather than encoding this with a complicated SVA sequence, we define a has_addr signal that is
+  // set on branches and cleared when the core receives an error.
+  logic has_addr;
+  always @(posedge clk or negedge rst_n) begin
+    if (! rst_n) begin
+      has_addr <= 1'b0;
+    end else begin
+      if (branch) begin
+        has_addr <= 1'b1;
+      end else if (err & ready & valid) begin
+        has_addr <= 1'b0;
+      end
+    end
+  end
+
+  `ASSERT(NoFetchWithoutAddr, req |-> (branch | has_addr), clk, !rst_n)
+
+  // The err_plus2 signal means "this error was caused by the upper two bytes" and is only read when
+  // both valid and err are true. It should never be set for compressed instructions (for them, the
+  // contents of the upper two bytes are ignored).
+  `ASSERT(ErrPlus2ImpliesUncompressed,
+          valid & err & err_plus2 |-> rdata[1:0] == 2'b11,
+          clk, !rst_n)
+
+  // KNOWN assertions:
+
+  // Control lines from the core (req, branch, ready, enable, invalidate) must always have a known
+  // value
+  `ASSERT_KNOWN(ReqKnown,        req,        clk, !rst_n)
+  `ASSERT_KNOWN(BranchKnown,     branch,     clk, !rst_n)
+  `ASSERT_KNOWN(ReadyKnown,      ready,      clk, !rst_n)
+  `ASSERT_KNOWN(EnableKnown,     enable,     clk, !rst_n)
+  `ASSERT_KNOWN(InvalidateKnown, invalidate, clk, !rst_n)
+
+  // The branch_addr value must be known if branch is high
+  `ASSERT_KNOWN_IF(BranchAddrKnown, branch_addr, branch, clk, !rst_n)
+
+  // The valid line usually has a known value. The only exception is after an error (when the
+  // cache's skid buffer doesn't know whether it contains valid data; there's data iff the previous
+  // instruction was compressed, but the instruction data was 'X, so we can't check the bottom two
+  // bits).
+  //
+  // To model this, we require that valid is known whenever has_addr is true. The NoFetchWithoutAddr
+  // assertion checks that the core will never actually take any data when !has_addr.
+  `ASSERT_KNOWN_IF(ValidKnown, valid, has_addr, clk, !rst_n)
+
+  // The address of a response and its error flag must be known if valid is high (these checks are
+  // also gated by has_addr because otherwise the assertion would trigger even if valid was allowed
+  // to be 'X). The err_plus2 flag must be known if err is set.
+  `ASSERT_KNOWN_IF(RespAddrKnown, addr,      has_addr & valid,       clk, !rst_n)
+  `ASSERT_KNOWN_IF(ErrKnown,      err,       has_addr & valid,       clk, !rst_n)
+  `ASSERT_KNOWN_IF(ErrPlus2Known, err_plus2, has_addr & valid & err, clk, !rst_n)
+
+  // The lower 16 bits of a response must be known if valid is high and err is not
+  `ASSERT_KNOWN_IF(LowRDataKnown, rdata[15:0], has_addr & valid & ~err, clk, !rst_n)
+
+  // The upper 16 bits of a response must be known if valid is high, err is not and the instruction
+  // is not compressed.
+  `ASSERT_KNOWN_IF(HiRDataKnown,
+                   rdata[31:16],
+                   has_addr & valid & ~err & (rdata[1:0] == 2'b11),
+                   clk, !rst_n)
+
+  // The busy signal must always have a known value
+  `ASSERT_KNOWN(BusyKnown, busy, clk, !rst_n)
+
+endinterface

dv/uvm/icache/dv/tb/tb.sv

@@ -18,7 +18,7 @@ module tb;
   // interfaces
   clk_rst_if clk_rst_if(.clk(clk), .rst_n(rst_n));
 
-  ibex_icache_core_if core_if (.clk(clk));
+  ibex_icache_core_if core_if (.clk(clk), .rst_n(rst_n));
   ibex_icache_mem_if  mem_if  (.clk(clk));
 
   // dut