Sequence and Property in Assertions

What is a Sequence in Assertions?

A sequence defines an ordered set of events or conditions over time. Sequences capture temporal relationships between signals, such as when specific conditions must hold over a series of clock cycles. They are the building blocks for properties, making them essential for writing expressive assertions.

Syntax

sequence <sequence_name>;
  <expression>;
endsequence

Example: A Simple Sequence

Suppose we want to define a sequence where a signal req is followed by a signal ack within two clock cycles.

sequence req_ack_sequence;
  req ##1 ack;
endsequence

Here:

• req indicates that the request signal is asserted.
• ##1 ack specifies that the acknowledgment signal (ack) must be asserted one clock cycle later.

What is a Property in Assertions?

A property describes a condition that must hold for a given sequence. Properties are used to express rules or requirements that the design should adhere to. They can be used directly in assertions to ensure compliance with design specifications.

Syntax

property <property_name>;
  <sequence_or_expression>;
endproperty

Example: A Property for a Sequence

Using the sequence defined earlier, we can create a property to ensure that whenever a request (req) occurs, it is always followed by an acknowledgment (ack) within two cycles.

property req_ack_property;
  @(posedge clk) req_ack_sequence;
endproperty

Here:

• @(posedge clk) specifies that the property is checked on every rising edge of the clock (clk).
• req_ack_sequence links the previously defined sequence to the property.

The clock signal (clk) is integral to assertions as it defines the timing for evaluating sequences and properties. By associating assertions with clk, designers can ensure that temporal conditions are checked at precise clock edges.

Advanced Example: Using Delays and Overlaps

Sequences and properties can include delays and operators for more complex scenarios. Consider a situation where:

• A signal start must be followed by a done signal after exactly 3 clock cycles.

Sequence

sequence start_done_sequence;
  start ##3 done;
endsequence

Property

property start_done_property;
  @(posedge clk) start_done_sequence;
endproperty

Assertion

assert property (start_done_property);

Here, ##3 introduces a three-cycle delay between start and done.

Complete Code:

module test;

  // Signals
  reg clk;
  reg start;
  reg done;

  // Clock generation
  initial clk = 0;
  always #5 clk = ~clk; // 10ns clock period

  // Stimulus generation
  initial begin
    start = 0;
    done = 0;

    // Apply stimulus
    #15 start = 1; // start asserted at time 15ns
    #10 start = 0; // start deasserted at time 25ns

    #20 done = 1; // done asserted at time 45ns
    #10 done = 0; // done deasserted at time 65ns

    #20 $finish; // End simulation
  end

  // Sequence
  sequence start_done_sequence;
    start ##3 done;
  endsequence

  // Property
  property start_done_property;
    @(posedge clk) start_done_sequence;
  endproperty

  // Assertion
  assert property (start_done_property) $display("assertion got passed at %0t", $time);
    else $error("start_done_property failed at time %0t", $time);
    
    initial begin
      $dumpfile("test.vcd");
      $dumpvars();
    end

endmodule

The assertion will pass at 55ns for above code.

Waveform