[otbn,dv] Add a check for the INSN_CNT register
Since we want a cycle-by-cycle check that the dut and model match, it
seemed easiest just to use an assertion in an interface. This also
makes it easy to wire up a cover property to check we've seen the
counter saturate.
Signed-off-by: Rupert Swarbrick <rswarbrick@lowrisc.org>
diff --git a/hw/ip/otbn/doc/dv/index.md b/hw/ip/otbn/doc/dv/index.md
index 6303f70..95f6bc3 100644
--- a/hw/ip/otbn/doc/dv/index.md
+++ b/hw/ip/otbn/doc/dv/index.md
@@ -159,6 +159,12 @@
> The covergroup contains eight coverpoints (for each flag set and cleared).
> These are then crossed with the flag group.
+#### Instruction counter
+
+See the instruction counter saturate.
+
+> This is tracked in the `insn_cnt_if` interface with the `InsnCntSaturated_C` cover property.
+
### Instruction-based coverage
As a processor, much of OTBN's coverage points are described in terms of instructions being executed.
diff --git a/hw/ip/otbn/dv/uvm/env/otbn_env.core b/hw/ip/otbn/dv/uvm/env/otbn_env.core
index af06087..f23c345 100644
--- a/hw/ip/otbn/dv/uvm/env/otbn_env.core
+++ b/hw/ip/otbn/dv/uvm/env/otbn_env.core
@@ -20,6 +20,7 @@
- otbn_alu_bignum_if.sv
- otbn_mac_bignum_if.sv
- otbn_rf_base_if.sv
+ - otbn_insn_cnt_if.sv
- otbn_trace_item.sv: {is_include_file: true}
- otbn_trace_monitor.sv: {is_include_file: true}
- otbn_env_cfg.sv: {is_include_file: true}
diff --git a/hw/ip/otbn/dv/uvm/env/otbn_insn_cnt_if.sv b/hw/ip/otbn/dv/uvm/env/otbn_insn_cnt_if.sv
new file mode 100644
index 0000000..da0db16
--- /dev/null
+++ b/hw/ip/otbn/dv/uvm/env/otbn_insn_cnt_if.sv
@@ -0,0 +1,47 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+//
+// Used to track instruction counts
+
+`include "prim_assert.sv"
+
+interface otbn_insn_cnt_if (
+ input clk_i,
+ input rst_ni,
+
+ input logic [31:0] insn_cnt_i,
+ input logic insn_executing_i,
+ input logic stall_i,
+
+ input bit [31:0] model_insn_cnt_i
+);
+
+ // Check that the model and OTBN have matching instruction counters
+ `ASSERT(InsnCntMatches_A, model_insn_cnt_i == insn_cnt_i)
+
+ // As well as exposing the count itself, we've also exposed the "increment me" signal
+ // (insn_executing_i && !stall_i). This means we can see when an instruction counter of all ones
+ // would have incremented but saturated instead. Make sure we've exposed it properly by asserting
+ // that the count works as we expect the rest of the time.
+ logic [31:0] insn_cnt_r;
+ logic increment_me_r;
+ always_ff @(posedge clk_i or negedge rst_ni) begin
+ if (!rst_ni) begin
+ insn_cnt_r <= 0;
+ increment_me_r <= 1'b0;
+ end else begin
+ insn_cnt_r <= insn_cnt_i;
+ increment_me_r <= insn_executing_i & ~stall_i;
+ end
+ end
+ `ASSERT(IncWhenTold_A,
+ (increment_me_r && (insn_cnt_r < '1)) |-> (insn_cnt_i == insn_cnt_r + 32'd1))
+
+ // Now we know that the insn_executing_i and stall_i signals have the behaviour we expect, check
+ // for insn_cnt saturating by expecting to see a cycle where increment_me_r is true but insn_cnt_r
+ // and insn_cnt both equal '1.
+ `COVER(InsnCntSaturated_C,
+ increment_me_r && (insn_cnt_i == '1) && (insn_cnt_r == '1))
+
+endinterface
diff --git a/hw/ip/otbn/dv/uvm/tb.sv b/hw/ip/otbn/dv/uvm/tb.sv
index ccff183..06fde1f 100644
--- a/hw/ip/otbn/dv/uvm/tb.sv
+++ b/hw/ip/otbn/dv/uvm/tb.sv
@@ -129,6 +129,8 @@
assign edn_rnd_data_valid = dut.edn_rnd_req & dut.edn_rnd_ack;
assign edn_urnd_data_valid = dut.edn_urnd_req & dut.edn_urnd_ack;
+ bit [31:0] model_insn_cnt;
+
otbn_core_model #(
.DmemSizeByte (otbn_reg_pkg::OTBN_DMEM_SIZE),
.ImemSizeByte (otbn_reg_pkg::OTBN_IMEM_SIZE),
@@ -141,16 +143,29 @@
.start_i (model_if.start),
.done_o (model_if.done),
.start_addr_i (model_if.start_addr),
- .err_o (model_if.err),
.edn_rnd_data_valid_i (edn_rnd_data_valid),
.edn_rnd_data_i (dut.edn_rnd_data),
- .edn_urnd_data_valid_i (edn_urnd_data_valid)
+ .edn_urnd_data_valid_i (edn_urnd_data_valid),
+
+ .insn_cnt_o (model_insn_cnt),
+ .err_o (model_if.err)
);
// Pull the final PC out of the DUT
assign model_if.stop_pc = u_model.stop_pc_q;
+ otbn_insn_cnt_if insn_cnt_if (
+ .clk_i (clk),
+ .rst_ni (rst_n),
+
+ .insn_cnt_i (dut.insn_cnt),
+ .insn_executing_i (dut.u_otbn_core.u_otbn_controller.insn_executing),
+ .stall_i (dut.u_otbn_core.u_otbn_controller.stall),
+
+ .model_insn_cnt_i (model_insn_cnt)
+ );
+
initial begin
// drive clk and rst_n from clk_if
clk_rst_if.set_active();
