SystemVerilog Tutorial PART 22: by Abhiram Rao

Assertions in SystemVerilog - Part5

Examples

The following are examples of multiple-clock specifications:

 sequence s1;            @(posedge clk1) a ##1 b; // single clock sequence endsequence

 sequence s2;             @(posedge clk2) c ##1 d; // single clock sequence endsequence

1) Multiple-clock sequence

 sequence mult_s;       @(posedge clk) a ##1 @(posedge clk1) s1 ##1 @(posedge clk2) s2; endsequence

2) Property with a multiple-clock sequence

 property mult_p1;       @(posedge clk) a ##1 @(posedge clk1) s1 ##1 @(posedge clk2) s2; endproperty

3) Property with a named multiple-clock sequence

 property mult_p2;    mult_s; endproperty

4) Property with multiple-clock implication

 property mult_p3;      @(posedge clk) a ##1 @(posedge clk1) s1 |=> @(posedge clk2) s2; endproperty

5) Property with named sequences at different clocks. In this case, if s1 contains a clock, then it must be identical to (posedge clk1). Similarly, if s2 contains a clock, it must be identical to (posedge clk2).

 property mult_p5                @(posedge clk1) s1 |=> @(posedge clk2) s2; endproperty

6) Property with implication, where antecedent and consequent are named multi-clocked sequences

 property mult_p6;           mult_s |=> mult_s; endproperty

7) Property using clock flow and overlapped implication:

 property mult_p7;           @(posedge clk) a ##1 b |-> c ##1 @(posedge clk1) d; endproperty

Here, a, b, and c are clocked at posedge clk.

8) Property using clock flow and if...else:

 property mult_p8;              @(posedge clk) a ##1 b |-> if (c)             (1 |=> @(posedge clk1) d) else             e ##1 @(posedge clk2) f ; endproperty

Here, a, b, c, and e are clocked at posedge clk.