diff --git a/dv/uvm/icache/dv/ibex_icache_core_agent/ibex_icache_core_agent.core b/dv/uvm/icache/dv/ibex_icache_core_agent/ibex_icache_core_agent.core index 43b3e1f2..1d0f19a0 100644 --- a/dv/uvm/icache/dv/ibex_icache_core_agent/ibex_icache_core_agent.core +++ b/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} diff --git a/dv/uvm/icache/dv/ibex_icache_core_agent/ibex_icache_core_if.sv b/dv/uvm/icache/dv/ibex_icache_core_agent/ibex_icache_core_if.sv index 0e9d4e2f..d9546024 100644 --- a/dv/uvm/icache/dv/ibex_icache_core_agent/ibex_icache_core_if.sv +++ b/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); diff --git a/dv/uvm/icache/dv/ibex_icache_core_agent/ibex_icache_core_protocol_checker.sv b/dv/uvm/icache/dv/ibex_icache_core_agent/ibex_icache_core_protocol_checker.sv new file mode 100644 index 00000000..f47e05ce --- /dev/null +++ b/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 diff --git a/dv/uvm/icache/dv/tb/tb.sv b/dv/uvm/icache/dv/tb/tb.sv index c85bcd2b..f0562387 100644 --- a/dv/uvm/icache/dv/tb/tb.sv +++ b/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