Built-in methods in assertions

Built-in methods in assertions are designed to simplify complex logic and make verification more efficient and comprehensible. These methods are implemented in hardware description languages (HDLs) and assertion libraries like SystemVerilog Assertions (SVA) to analyze and validate temporal properties of a design.

Let’s delve into some commonly used built-in methods such as $rose, $fell, $stable, $past, $onehot, $onehot0, $countones, $isunknown, and others. We’ll explore their purposes, use cases, and examples.

1. $rose

The $rose function checks if least significant bit (LSB) of a signal or expression transitions from 0 or x or z (previous clocking value) to 1 in a given clock cycle. This is useful for detecting rising edges.

Syntax:

$rose(signal)

Example:

This example monitors a start signal and ensures that whenever there is a rising edge on start, a done signal is asserted within 5 clock cycles.

module rose_assertion_example (
    input  logic clk,
    input  logic reset_n,
    input  logic start,
    input  logic done
);

    // Assertion block
    property check_done_after_start;
        @(posedge clk) disable iff (!reset_n) $rose(start) |-> ##[1:5] done;
    endproperty

    // Bind the property to an assertion
    assert property (check_done_after_start)
        else $fatal("Assertion failed: 'done' not asserted within 5 cycles after 'start'!");

endmodule

Property:

  • @(posedge clk): Monitors the property on the positive edge of the clock.
  • disable iff (!reset_n): Disables the assertion when the system is in reset.
  • $rose(start): Detects the rising edge of the start signal.
  • |-> ##[1:5] done: Specifies that the done signal must be asserted within 1 to 5 cycles after the rising edge of start.

Assertion:

  • The assert property binds the property to an actionable assertion.
  • If the condition fails, $fatal is triggered, halting the simulation.

Waveform:

vlsiworlds.com/
Execute on

2. $fell

The $fell function checks if least significant bit (LSB) of a signal or expression transitions from 1 or x or z (previous clocking value) to 0 in a given clock cycle. This is useful for detecting falling edges.

Syntax:

$fell(signal)

Example:

The following module monitors a valid signal and ensures that whenever there is a falling edge on valid, a clear signal is asserted within 4 clock cycles.

module fell_assertion_example (
    input  logic clk,
    input  logic reset_n,
    input  logic valid,
    input  logic clear
);

    // Assertion block
    property check_clear_after_valid_fall;
        @(posedge clk) disable iff (!reset_n) $fell(valid) |-> ##[1:4] clear;
    endproperty

    // Bind the property to an assertion
    assert property (check_clear_after_valid_fall)
        else $fatal("Assertion failed: 'clear' not asserted within 4 cycles after 'valid' falls!");

endmodule

Property:

  • @(posedge clk): Monitors the property on the positive edge of the clock.
  • disable iff (!reset_n): Disables the assertion when the system is in reset.
  • $fell(valid): Detects the falling edge of the valid signal.
  • |-> ##[1:4] clear: Specifies that the clear signal must be asserted within 1 to 4 cycles after the falling edge of valid.

Assertion:

  • The assert property binds the property to an actionable assertion.
  • If the condition fails, $fatal is triggered, halting the simulation.

Waveform:

vlsiworlds.com/
Execute on

3. $stable

The $stable function ensures that a signal maintains its value (i.e., no changes occurred during the cycle).

Syntax:

$stable(signal)

Example:

property stable_check;
@(posedge clk) penbl |-> $stable(paddr);
endproperty

// Bind the property to an assertion
    assert property (stable_check)
        else $fatal("Assertion failed: addr is not stable when enbl is high");

This assertion ensures that paddr must be stable, when penbl is high.

4. $past

The $past function is used to access the value of a signal in a previous clock cycle. It is essential for comparing historical values of signals.

Syntax:

$past(signal, cycles, getting expression)

The getting expression is optional expression.

Example:

 property check_data_change_validity;
        @(posedge clk) disable iff (!reset_n)
        (enable && (data != $past(data))) |-> valid;
    endproperty

    // Bind the property to an assertion
    assert property (check_data_change_validity)
        else $fatal("Assertion failed: 'valid' not asserted when 'data' changed with 'enable' active!");

(enable && (data != $past(data))): Checks if enable is high and data has changed from its previous value.

|-> valid: Ensures that valid is asserted in the same cycle.

Example 2:

assert (data == $past(data, 1)) else $fatal("Data mismatch with the previous cycle");

This ensures that the data signal in the current cycle matches its value from one cycle ago.

5. $onehot

The $onehot function checks whether exactly one bit in a signal is set to 1.

Syntax:

$onehot(signal)

Example:

assert ($onehot(select)) else $fatal("Select signal is not one-hot encoded");

This ensures that the select signal is a valid one-hot encoding.

6. $onehot0

The $onehot0 function verifies whether zero or one bit in a signal is set to 1.

Syntax:

$onehot0(signal)

Example:

assert ($onehot0(state)) else $fatal("State signal has multiple bits set");

This is useful when the signal can have either no active bits or one active bit.

7. $countones

The $countones function counts the number of bits set to 1 in a signal.

Syntax:

$countones(signal)

Example:

assert ($countones(flags) <= 3) else $fatal("Too many flags are active");

This ensures that no more than three bits in the flags signal are active.

8. $isunknown

The $isunknown function detects whether a signal contains unknown (x) or high-impedance (z) values.

Syntax:

$isunknown(signal)

Example:

assert (!$isunknown(status)) else $fatal("Status signal contains unknown values");

This ensures that the status signal does not have invalid values.

Use Cases for Built-In Methods

  1. Debugging and Diagnostics: These functions allow for precise monitoring of signal behavior during simulation and verification.
  2. Simplified Expressions: Built-in methods reduce complex logic into compact, easy-to-read assertions.
  3. Error Detection: Using functions like $isunknown helps identify invalid signal states early in the design phase.

Practical Example: Combining Built-In Functions

Here’s an example of how multiple built-in methods can work together in an assertion:

assert (enable && $rose(clk) && !$isunknown(data)) 
else $fatal("Enable active but data is unknown or clock did not rise");

This ensures that when enable is active, the clock must rise, and the data signal must not contain invalid values.

Previous
Next