[adc_ctrl,dv] Expand comments a bit and tidy up adc_ctrl_fsm_sva_if

There is no functional change, but dropping the ASSERT macro makes
things a little easier to read.

The hardware reset assertions should now be a little more
efficient. I don't think we really need to bother asserting that the
signals don't magically start changing somewhere in the middle of a
reset(!), so I've restructured them slightly to check the first clock
after the start of a reset.

The first syntax I used for this (which is equivalent to the previous
version, but without noise from the macro) uses two "clocks" and is of
the form

  @(negedge rst_aon_ni) 1 |=> @(posedge clk_aon_i) XYZ

Here, the |=> waits for the event on the right hand side, so it means
"On the first clock edge after reset is asserted, XYZ". Very nice!

Unfortunately, this isn't actually supported by Verible's
SystemVerilog front-end. Grr! I was very annoyed at first, but
realised that there's actually an even cleaner way to do it. Because
this is a bound-in interface, we can easily define a helper signal.

This commit defines a "start_of_reset" flag, which set when reset is
asserted and then cleared on the first clock. Now, the properties can
be very simple, looking like:

  start_of_reset -> XYZ

(checked on the positive edge of clk_aon_i because of the default
clocking statement).

That's even shorter! Yippee!

When I initially wrote this, I worried about the scheduling because we
clear start_of_reset on the clock edge and look at the value at the
same time. Fortunately, this is ok: the value tested in the expression
is its value from the preponed region (see IEEE 1800, 16.5.1), so
we'll get the value that hasn't yet been cleared.

Signed-off-by: Rupert Swarbrick <[email protected]>

Author: rswarbrick

hw/ip/adc_ctrl/dv/sva/adc_ctrl_fsm_sva_if.sv

@@ -2,44 +2,62 @@
 // Licensed under the Apache License, Version 2.0, see LICENSE for details.
 // SPDX-License-Identifier: Apache-2.0
 // System verilog assertions for the adc_ctrl_fsm module
+
+// An interface that is bound into adc_ctrl_fsm, capturing ports with .* (so the input ports are
+// named to match signals inside that module).
+
 interface adc_ctrl_fsm_sva_if
   import adc_ctrl_pkg::*;
-  (
+(
   // adc_ctrl_fsm ports
   input logic clk_aon_i,
   input logic rst_aon_ni,
   input logic cfg_fsm_rst_i,
+
   // adc_ctrl_fsm signals
-  input fsm_state_e fsm_state_q,
-  input logic [3:0] pwrup_timer_cnt_q,
+  input fsm_state_e  fsm_state_q,
+  input logic [3:0]  pwrup_timer_cnt_q,
   input logic [23:0] wakeup_timer_cnt_q,
   input logic [15:0] np_sample_cnt_q,
-  input logic [7:0] lp_sample_cnt_q
+  input logic [7:0]  lp_sample_cnt_q
 );
 
   localparam fsm_state_e FsmResetState = PWRDN;
 
-  // FSM software reset
-  `ASSERT(FsmStateSwReset_A, cfg_fsm_rst_i |=> fsm_state_q == FsmResetState, clk_aon_i, !rst_aon_ni)
-  `ASSERT(PwrupTimerCntSwReset_A, cfg_fsm_rst_i |=> pwrup_timer_cnt_q == 0, clk_aon_i, !rst_aon_ni)
-  `ASSERT(WakeupTimerCntSwReset_A, cfg_fsm_rst_i |=> wakeup_timer_cnt_q == 0, clk_aon_i,
-          !rst_aon_ni)
-  `ASSERT(NpSampleCntSwReset_A, cfg_fsm_rst_i |=> np_sample_cnt_q == 0, clk_aon_i, !rst_aon_ni)
-  `ASSERT(LpSampleCntSwReset_A, cfg_fsm_rst_i |=> lp_sample_cnt_q == 0, clk_aon_i, !rst_aon_ni)
-
-
-  // FSM hardware reset - checks first clk_aon_i after every hardware reset
-  `ASSERT(FsmStateHwReset_A, 1 |=> (@(posedge clk_aon_i) fsm_state_q == FsmResetState), !rst_aon_ni,
-          0)
-  `ASSERT(PwrupTimerCntHwReset_A, 1 |=> (@(posedge clk_aon_i) pwrup_timer_cnt_q == 0), !rst_aon_ni,
-          0)
-  `ASSERT(WakeupTimerCntHwReset_A, 1 |=> (@(posedge clk_aon_i) wakeup_timer_cnt_q == 0),
-          !rst_aon_ni, 0)
-  `ASSERT(NpSampleCntHwReset_A, 1 |=> (@(posedge clk_aon_i) np_sample_cnt_q == 0), !rst_aon_ni, 0)
-  `ASSERT(LpSampleCntHwReset_A, 1 |=> (@(posedge clk_aon_i) lp_sample_cnt_q == 0), !rst_aon_ni, 0)
-
-  // Check connectivity of the state output register (this is used for debug only).
-  `ASSERT(FsmDebugOut_A, fsm_state_q === tb.dut.u_reg.hw2reg.adc_fsm_state.d,
-      clk_aon_i, !rst_aon_ni)
+  default clocking @(posedge clk_aon_i); endclocking
+
+  if (1) begin : gen_aon_assertions
+    default disable iff !rst_aon_ni;
+
+    // FSM software reset
+    FsmStateSwReset_A: assert property (cfg_fsm_rst_i |=> fsm_state_q == FsmResetState);
+    PwrupTimerCntSwReset_A: assert property (cfg_fsm_rst_i |=> pwrup_timer_cnt_q == 0);
+    WakeupTimerCntSwReset_A: assert property (cfg_fsm_rst_i |=> wakeup_timer_cnt_q == 0);
+    NpSampleCntSwReset_A: assert property (cfg_fsm_rst_i |=> np_sample_cnt_q == 0);
+    LpSampleCntSwReset_A: assert property (cfg_fsm_rst_i |=> lp_sample_cnt_q == 0);
+
+    // Check connectivity of the state output register (this is used for debug only).
+    FsmDebugOut_A: assert property (fsm_state_q === tb.dut.u_reg.hw2reg.adc_fsm_state.d);
+  end
+
+  // FSM hardware reset
+  //
+  // These assertions contain properties that have a check on the first posedge of clk_aon_i after
+  // the hardware reset is applied. Note that this clock edge may happen during or after the reset
+  // (and the assertions are expected to be true either way).
+
+  bit start_of_reset;
+  always @(negedge rst_aon_ni) begin
+    start_of_reset <= 1;
+  end
+  always @(posedge clk_aon_i) begin
+    start_of_reset <= 0;
+  end
+
+  FsmStateHwReset_A: assert property (start_of_reset -> fsm_state_q == FsmResetState);
+  PwrupTimerCntHwReset_A: assert property (start_of_reset -> pwrup_timer_cnt_q == 0);
+  WakeupTimerCntHwReset_A: assert property (start_of_reset -> wakeup_timer_cnt_q == 0);
+  NpSampleCntHwReset_A: assert property (start_of_reset -> np_sample_cnt_q == 0);
+  LpSampleCntHwReset_A: assert property (start_of_reset -> lp_sample_cnt_q == 0);
 
 endinterface