SVA Sequence Subtleties (Sequence fusion / Sequence concatenation)

SystemVerilog
, , , ,
1

Hi guys,

I’m quite new to SVA properties and assertions, so this might be a noob question.
But I think getting a good answer to this will bring me a long ways towards developing a real understanding.

I’m trying first with a short version.
If you need more detail in order to help, I’ll supply more context.

I’m using variants of the following sequence to check generic responses to requests on an interface.
The sequence is called from within a property, whenever a transaction is requested.
Once the sequence matches, I call another property which checks the responses.
The sequence carries an argument num_ahead, which specifies the number of outstanding unrelated responses expected before the relevant response arrives.

I’m observing some strange behavior depending on very subtle differences in the code.
In particular I can’t explain the difference which I observe for the following two variants.
Regarding the observed behavior, unfortunately I can’t go much beyond “variant 2 works, variant 1 does not”.
So some fundamental explanation of the difference between the two would be very very much appreciated.
Can anybody explain what is happening here?

Variant 1:


sequence response_queue (local input int unsigned num_ahead);
  ( 
    (num_ahead > 0) && transaction_advance [->1], num_ahead--)
  ) [*]
  ##1
  (
    (num_ahead == 0) [->1]
  )
endsequence

Variant 2:


sequence response_queue (local input int unsigned num_ahead);
  1'b1 ##0 // Added sequence fusion with 1'b1
  (        // Added parenthesis
    ( 
      (num_ahead > 0) && transaction_advance [->1], num_ahead--)
    ) [*]
    ##1
    (
      (num_ahead == 0) [->1]
    )
  );
endsequence

Any help is appreciated,
No.

2

In reply to No:
There are sayings that are good advice, particularly in software:

  • KISS
  • Why make it complicated when you can make it simple?
  • Why make it simple when you can make it complicated?

SVA is rich, maybe too rich, in features and possibilities.

1131×768 99.9 KB

Declaring local variables in sequence_port_list is confusing. I wrote several books,
lots of SVA code, analyzed several users’s requirements and have never found the need to do that. Declare the local variables in the assertion_variable_declaration; it make it so much easier.
Here is an awful example that demonstrates why one may want to declare local variables in the port list. I say awful because it creates code that is hard to read an understand, and then you have to worry that you don’t violate the many rules of doing this local variable declaration in the port list. My advice, KISS!


bit clk, a, b, c;
default clocking cb_clk @ (posedge clk); endclocking
sequence q_local_formal_arguments2( local input int i=0, untyped j, k,
                                    local output bit t);
   (i>10, j=i) ##1 (1, j=data, t=1'b1) ##1 k;
endsequence
property p_test_untype;
  int x, z; // local variable
  bit r; // local variable
  (a, x=10) ##1 
   q_local_formal_arguments2( .i(x), .j(z), .k(a), .t(r)) ##1 x==z ##0 r;
endproperty : p_test_untype
ap_test_untype: assert property(p_test_untype);

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) 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:
You sequence declaration does not look correct. You need to explain your requirements.
This is my guess at what you need


sequence response_queue(sig); 
 int num_ahead;
 @(posedge clk) ($rose(sig), num_ahead=data) ##0 
  (num_ahead > 0 && transaction_advance, num_ahead--)[*1:$] ##1
   num_ahead <= 0);
endsequence

(num_ahead == 0) [->1] cause way too many threads.
I strongly urge you to read my papers

4

In reply to ben@SystemVerilog.us:

Thanks very much Ben.
Yes, I absolutely agree.
I should KISS as much as I can. ;)

But I can’t really seem to get around using that sequence.
Your guess is close but not quite there.
However, I think I can now explain better

I essentially need a dynamic repeat expression, i.e. I need to see transaction_advance go high (or stay high) num_ahead times before I continue.

So the entire property could be written as something like this:


property p_transaction;
  int num_ahead;
  (request_advance, num_ahead=data)
  ##1 transaction_advance [=num_ahead]
  |-> ##[1:$] response_advance
endproperty

Unfortunately the [=num_ahead] notation does not allow dynamic numbers of repetition.
So I’ve tried your sequence sq_rpt_simple_count from your SVA package SVA: Package for dynamic and range delays and repeats | Verification Academy.
Buy it seems that doesn’t support 0-repetitions.

With that do you have any suggestions?

5

In reply to No:

Quick responss: use my Package on dynamic repeats
SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy