Reset sequences are only as good as their checkers. A test that asserts reset mid-transfer but never checks the outputs during reset proves nothing. Three properties cover most reset behaviour: outputs stay safe while reset is asserted, nothing starts before release is complete, and no stale state survives the reset.

The three properties

Concurrent assertions, where the simulator supports them

The properties below are written as concurrent assertions for simulators with assertion support. They state the contract independently of any one test, so every reset sequence in the regression checks them automatically.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

// not-run: concurrent assertions need a simulator with SVA support
// Properties for the buffer of the previous lesson.
// Bind the signals clk, rst_n, s_valid, s_ready and m_valid at the point of use.
property safe_while_in_reset;
  @(posedge clk) !rst_n |-> !m_valid;
endproperty
assert property (safe_while_in_reset);

property no_accept_while_in_reset;
  @(posedge clk) !rst_n |-> !(s_valid && s_ready);
endproperty
assert property (no_accept_while_in_reset);

property empty_after_release;
  @(posedge clk) $rose(rst_n) |-> ##1 !m_valid;
endproperty
assert property (empty_after_release);

The equivalent plain checker, runnable anywhere

Where concurrent assertions are unavailable, the same three properties become plain checkers sampled on the falling edge, when all signals are settled. The buffer is repeated here so this example runs on its own.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32

`timescale 1ns/1ps

// One-entry valid/ready buffer, repeated so this example runs on its own.
module xfer_buf_mon (
  input  logic clk,
  input  logic rst_n,
  input  logic s_valid,
  output logic s_ready,
  input  logic [7:0] s_data,
  output logic m_valid,
  input  logic m_ready,
  output logic [7:0] m_data
);
  logic full_q;
  logic [7:0] data_q;

  assign s_ready = ~full_q & rst_n;   // not ready while in reset: a source holding valid must see no accept
  assign m_valid = full_q;
  assign m_data = data_q;

  always @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      full_q <= 1'b0;
      data_q <= 8'h00;
    end else if (s_valid && s_ready) begin
      full_q <= 1'b1;
      data_q <= s_data;
    end else if (m_valid && m_ready) begin
      full_q <= 1'b0;
    end
  end
endmodule

What the checks and the review look for

The review checks that every reset sequence in the regression is covered by at least the safe-outputs property, either as a concurrent assertion or as a plain checker, and that the properties are bound in every configuration, not just the default one. An assertion that never fires because it was never bound is worse than no assertion: it looks like coverage.

Related topics

• Reset sequences and random resets

• Reset coverage

• RTL: CDC verification