Assertion for non-overlap sequence detector

SystemVerilog
, ,
1

for a non-overlap sequence detector of 1101,
I wanna have 2 assertions to test it
1: upon seeing 1101 sequence, detected should be asserted.
2: if detected is asserted, past sequence should be 1101.

property seq1101_to_det;                                                        
@(posedge clk) sequence_in ##1 sequence_in ##1 !sequence_in ##1 sequence_in |=> detected;
endproperty

question1:
for a sequence of 1101101, since it’s non-overlap, detected will only asserted on 1101(detcted)101, but assertion will fail on the latter part of the sequence, meaning this property actually describes 1101(detcted)101(detected). how can I prevent this issue?

property upon_det_seq1101;    
@(posedge clk) @rose(detected) |->  // past sequence should be 1101.
endproperty

question2:
My initial feeling is to finish this assertion with $past function, but I don’t know how to implement it, or maybe there’re some nicer way?

Thanks,
Jeff

2

In reply to Jeff_Li_90:

  1. Looking for a sync pattern of 16 bits
    a a !a a; a a !a a; not(a a !a a); a a !a a;
  2. If you have a good first 4 bits, you want to exclude the other attempts
  3. My untested approach is to use a lock to start.
    This should resolve your 1101101
  4. The unlock resets if it fails to find a match.

TWO SOLUTIONS: COMPLEX ONE HERE, SIMPLER ONE IN THE REPLY


// NEEDS TESTING BADLY.  WAY TOO COMPLEX OF AN APPROACH 
    bit clk, a, b, c, rst_n, lock, detected;
    function void set_lock(bit q);
      if(q) lock <=1'b1; 
      else lock <= 1'b0;
    endfunction

    sequence seq1101_to_det; @(posedge clk)  a ##1 a ##1 !a ##1 a;  endsequence 
    // 16 bits sequence    a a !a a; a a !a a; not(a a !a a); a a !a a; 
    // put a lock 12 bits           <--------------------------------->

    ap_detected: assert property(  
     @(posedge clk) disable iff(rst_n==0) 
            lock==0 ##4 (seq1101_to_det.triggered, set_lock(1)) ##4 
                        ( (seq1101_to_det.triggered ##4
                           !seq1101_to_det.triggered ##4
                           (seq1101_to_det.triggered, set_lock(0)))) //intersect 1[*12])
                                            |=> detected) else  set_lock(0); 
    
    ap_no_sync_TF: assert property(  // pattern no pattern 
          @(posedge clk) disable iff(rst_n==0) 
                         lock==0 ##4 seq1101_to_det.triggered ##4 
                         (!seq1101_to_det.triggered, set_lock(0))); 
                         
      ap_no_sync_TTT: assert property(  // 3 sequences od same pattern 
            @(posedge clk) disable iff(rst_n==0) 
                           lock==0 ##4 seq1101_to_det.triggered ##4
                                      seq1101_to_det.triggered ##4
                                       (seq1101_to_det.triggered, set_lock(0)));

      ap_no_sync_TTTT: assert property(  // 4 sequences od same pattern 
          @(posedge clk) disable iff(rst_n==0) 
             lock==0 ##4 seq1101_to_det.triggered ##4
               seq1101_to_det.triggered ##4
               seq1101_to_det.triggered ##4
                (seq1101_to_det.triggered, set_lock(0)));

After some more thoughts, there is no need for that “lock” concept.
At every clocking event there is a need to look for async pattern.

Let me if this works out.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

3

In reply to ben@SystemVerilog.us:

A much much easier solution for the detection of a sync pattern in a stream:


    bit[15:0] sync=16'b1101110100001101, log; 

    always_ff @(posedge clk or negedge rst_n) begin
      if(!rst_n) log=0; 
      else log<= {a, log[14:0]}; 
      a_sync: assert(log[15:8]==sync[15:8]  && log[7:4]!=1101 && log[3:0] == sync[3:0])
               detected = 1; else detected=0; 
    end

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

4

In reply to ben@SystemVerilog.us:

A useful comment by a colleague.
Should you shift it into log from the right?
Also, I am not sure about the actual requirement. Is it to detect the sequence to be used somewhere, or fail any time it does not match?
I think for detection it would be better to use a cover and use the action block to signal it to whatever needs this info.
[Ben] I agree with the use of the cover instead of the assert.
As to the direction of the shift, you are correct.
In any case, the approach is correct.

5

In reply to ben@SystemVerilog.us:

Hi Ben,

Thank you for the solutions, Yes I agree that it seems putting it into a stream is the easier way to go.

6

In reply to ben@SystemVerilog.us:

revisit:
found sync_accept_on might be able to solve my issue.

property seq1101_to_det;                                                        
@(posedge clk) sync_accept(detected) sequence_in ##1 sequence_in ##1 !sequence_in ##1 sequence_in |=> detected;
endproperty

upon detected assertion, sequence detector fsm would return to initial stage, so it’s safe to kill current thread and make it vacuous I think

7

In reply to Jeff_Li_90:

upon detected assertion, sequence detector fsm would return to initial stage, so it’s safe to kill current thread and make it vacuous I think
bit detected;
@(posedge clk) sync_accept(detected) sequence_in ##1 sequence_in ##1 !sequence_in ##1 sequence_in |=> detected;

I presume that you have an FSM that sets/resets the bit detected.
The assertion as you wrote would not compile because the ! in !sequence_in is a logical operator. You cannot use the not in … ##1 sequence_in ##1 not(sequence_in) because the not is a property operator. To fix that you can write


 sequence_in ##1 sequence_in ##4 !sequence_in.triggered ##1 sequence_in |=> detected;

Now on the accept_on. !800’2017 says:
*The accept_on/reject_on family of operators just terminates the property as an accept (true vacuously, with no contribution to the pass statistics) or reject (false vacuously, with contributions to the failed statistics).

The accept_on (expression_or_dist) property_expr accepts the property as true if the expression_or_dist (called the abort condition) is true. Otherwise, with the abort condition as false, the property expression evaluates to completion. The abort condition with the accept_on is asynchronous, whereas the sync_accept_on is synchronous to the clock under current consideration for the property. Unlike disable iff, the synchronous abort condition is sampled during the Preponed sampling region for properties.*
You do not need it in this case, as it does nothing for you. All it does for you is kill the first attempt after detected==1. At every clocking event you start evaluating the sequence:
sequence_in ##1 sequence_in ##4 !sequence_in.triggered ##1 sequence_in
Here is an example of the accept_on. Note that when done occurs at any time, even within the repetition cycles, the assertion is true.


ap_accept_disable : assert property (@ (posedge clk)
  disable iff (!reset_n)
    sync_accept_on ( done )
     $rose(dma_req) |=> data_transfer[*100]);

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

8

In reply to ben@SystemVerilog.us:

Hi Ben,

It compiles.

I agree with you sycn_accept_on here is not the ideal choice, but I would argue this might be one of the feasible working around.