First_match operator

SystemVerilog
,
1

Hello,

I would like some clarification on how first_match works. Additionally, could you explain its benefits in the industry?

In my code, C is high for 3 clock cycles starting at 5 ns, D is high for 3 clock cycles starting at 15 ns, and E is high for 1 clock cycle starting at 25 ns.

Here’s the sequence and properties I’m working with:

sequence SEQ_CD;
    C[*1:3] ##1 D;
endsequence

property FM_prop;
    first_match(SEQ_CD) |=> E;
endproperty

property normal_prop;
    SEQ_CD |=> E;
endproperty

I expected that the output would trigger first_match only once, but instead, it triggers three times. Could you explain why this happens?

Here’s a link to the code and log on EDA Playground: EDA Playground

Thank you in advance for your help!

2

A concurrent assertion starts a new thread every clock cycle regardless of what expressions appears in your property. That thread (also called an attempt) remains active until the property passes or fails. Ranges may cause additional threads to be forked off. In your example, a new thread starts every clock cycle, but vacuously passes when C is 0, so that attempt gets immediately terminated.

first_match() makes more sense when used on a subsequence of a larger sequence. It prevents backtracking when a match on the subsequence is found, but a later term in the sequence does not match

Let’s take a look at a slightly modified example below which adds B to complete sequence.

On cycle 1, C is 0. Both assertions vacuously pass. Both threads are done.
On cycle 2. C is 1. Both assertions have repetition 1 of C. Both assertions start 2 new threads: the next cycle looking for repetition 2 of C or looking for D. There are now 4 active threads that started on cycle 2.

On cycle 3. C is still one. A new set of 4 threads start on cycle 3, but the rest of this discussion focuses on the threads that started on cycle 2.

Here’s where things diverge with the first_match assertion. D is now 1, so that is a match for sequence SEQ_CD. The first_match(SEQ_CD) kills the thread looking (and would have found) repetition 2 of C, and prevents creating the thread looking for repetition 3 of C. The first_match assertion has only one thread that started on cycle 2 now looking for B in the next cycle. The normal assertion has 3 threads; looking in the next cycle for B, D, or repetition 3 of C.
On Cycle 4, B is 0. There is no match for the first_match assertion, so that is a vacuous pass. D is 0, but C is still 1, so that leaves one thread still active for the normal assertion looking for D in the next cycle. That thread eventually passes.
I’ll stop going into details; the point was to show you how first_match prevents a later match of a larger sequence.

module sequence_operators;

  bit a_clk;
  bit B,C,D,E;

  initial repeat(50) #5 a_clk = ~ a_clk;

  default clocking my_clk @(posedge a_clk);
  endclocking

  initial begin
    $dumpfile("waveform.vcd");
    $dumpvars;
  end
  
  initial begin
    @(negedge a_clk); {B,C,D,E}  <= 4'b0_1_0_0;
    @(negedge a_clk); {B,C,D,E}  <= 4'b0_1_1_0;
    @(negedge a_clk); {B,C,D,E}  <= 4'b0_1_0_0;
    @(negedge a_clk); {B,C,D,E}  <= 4'b0_1_1_0;
    @(negedge a_clk); {B,C,D,E}  <= 4'b1_1_0_1;
  end
  
  sequence SEQ_CD;
    C[*1:3] ##1 D;
  endsequence
  property FM_prop;
    first_match(SEQ_CD) ## 1 B |=> E;
  endproperty
  property normal_prop;
    SEQ_CD ##1 B |=> E;
  endproperty

  first_matchh : assert property(FM_prop)
    $info ("\033[32m first_match assertion passed @%0t", $time);
    else
    $error ("\033[31m first_match assertion failed @%0t", $time);
  normal : assert property(normal_prop)
    $info ("\033[32m normal assertion passed @%0t", $time);
    else
    $error ("\033[31m normal failed @%0t", $time);
endmodule
1 Like
3

I would rewrite this as

ap_cde: assert property(@ (posedge clk) 
               $rose(C) ##1 first_match(C[*1:2] ##1 D)  |-> ##1 E);  
// The property is vacuous if $rose(C) if false.

Thanks Dave for taking the time to explain the attempts.

4

If C holds for 3 cycles why is first_match necessary? Would this suffice?
$rose(C) ##1 C[*2] ##1 D

or even C[*3] ##1 D

And if needed check that C is 3 cycles surrounded by !C on either side.
In general, I rey to stay away from using first_match. It can be complex implementation in some cases, in particular for formal tools.

5

To match more closely with my updated example, first_match makes more sense with

 assert property(@ (posedge clk) 
               $rose(C) ##0 first_match(C[*1:3] ##1 D) ##1 B |-> ##1 E);

The $rose(C) ##0 keeps the repetitions from overlapping attempts, and the first_match() prevents backtracking when B is false.