Question on the Intersect operator of SVA sequences

[puranik.sunil]

Hi,
I need to write an assertion for following problem:

1. Each transaction is delimited by sop and eop and should contain exactly two read and three write requests with following characteristics:

• There should be exactly two read requests issued before time t.
• There should be exactly three write requests issued before time t.
• At clock tick t, first occurrence of eop should happen

This can be written using intersect operator as follows :

assert property (sop |-> read [=2] intersect write [=3] intersect eop [-> 1]);

Now I have read in one of the books on SVA that All the formal verification tools internally eliminate the intersect operator. So can this logic be implemented without using intersect operator? What will be the property expression in that case?

rgs,
-sunil

[ben2]

In reply to puranik.sunil@tcs.com:

You can use the within operator; however, if the within is handled like the intersect because, per 1800

The construct seq1 within seq2 is an abbreviation for the following: 
(1[*0:$] ##1 seq1 ##1 1[*0:$]) intersect seq2

When you say formal verification tools internally eliminate the intersect operator, do you mean that they internally convert it to something else, or is it illegal?
I’ll ask this question to one of my colleague who is an expert on formal verification, and I’ll get back to you.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

• SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
  // For 10% discount, use code 45KJT5GN @ https://www.createspace.com/5810350
• A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
• Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
• Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
• Component Design by Example ", 2001 ISBN 0-9705394-0-1
• VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
• VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115

---

[puranik.sunil]

Hi Ben,

the book says the FV tools in their internal implementation eliminate the intersect operator and generate all the possible combinations of events. One of the exercises given in the book is as follows :

1. Write the following property without Intersect operator:

a1: assert property ( 
command |-> write_cmpl [-> 1] intersect read_cmpl [-> 2]);

Now with goto repetition operator, at the last clock tick one read_cmpl and one write_cmpl (the only one) should happen at the same time. (read_cmpl && write_cmpl). Considering all combinations of remaining events, (one read_cmpl, !read_cmpl, !write_cmpl), we need to consider all following possibilities.

1. read_cmpl && !write_cmpl followed by some indefinite number ([*0:$]) of !read_cmpl && !write_cmpl followed by read_cmpl && write_cmpl;

or

2. indefinite number of times ([*0:])!write_cmpl&& !read_cmpl, followed by read_cmpl && !write_cmpl followed by indefinite number of times ([*0:])!write_cmpl&& !read_cmpl, followed by read_cmpl && write_cmpl;

If we combine sequence 1 and 2 above using OR operator shall we get the logic described in property a1 that is - write_cmpl [-> 1] intersect read_cmpl [-> 2]?

Can the similar approach be followed for my earlier question given below if we need to re-write it without intersect operator ?

assert property (sop |-> read [=2] intersect write [=3] intersect eop [-> 1]);

rgs,
-sunil

[ben2]

In reply to puranik.sunil@tcs.com:

FV tools in their internal implementation eliminate the intersect operator

• What is the title of the book?
• A colleague tried the intersect operator in a formal verification tool, and it is supported, at least by that tool.
• Contact your tool vendor’s support on this issue. In this forum, we do not talk about specific tools, so please mention the tool. Language issues and books are OK to talk about

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

• SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
  // For 10% discount, use code 45KJT5GN @ https://www.createspace.com/5810350
• A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
• Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
• Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
• Component Design by Example ", 2001 ISBN 0-9705394-0-1
• VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
• VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115

---

[puranik.sunil]

Hi Ben,

The book title is “The Power of Assertions in system verilog” by Eduard Cerny.
We are using questasim however, my question is not specific to this tool. I have a general question (which is rather academic in nature) that given an assertion which uses Intersect operator, can we write the same logic without using the intersect operator, (based on the statement made in the book. The book also says that Intersect operator is replaced by all combinations of events).

for example,

a1: assert property ( 
command |-> write_cmpl [-> 1] intersect read_cmpl [-> 2]);

Question was can we implement the logic of assertion a1 in alternative way without using Intersect since the book gives this as exercise question at the end of chapter. How to replace this logic by all combinations of events as stated in the book?

To summarize, the question I wanted to ask was : Is the logic given in question asked in my July 24 post correct? Can the intersect operator be replaced by the logic given in the July 24 post. (please refer to the question asked in my July 24 post above)

rgs,
-sunil

[ben2]

In reply to puranik.sunil@tcs.com:
Your equivalent equations are too complex, and hard to follow.
Formal verification tools do support the intersect.
One of the best way to check for equivalency is to use constrained-random tests on your test model. I use the following constrained-random tests to verify assertions.
You can vary your constraints to test various combinations. If your original and equivalent assertions behave exactly the same, in all respects, they they are equivalent. However, the 2 assertions may express different notions of the requirements, but are not identical.

import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
	bit clk, a, b;  
	default clocking @(posedge clk); endclocking
	initial forever #10 clk=!clk;   

 initial begin 
     repeat(200) begin 
       @(posedge clk);   
       if (!randomize(a, din)  with 
           { a dist {1'b1:=1, 1'b0:=3};
             b dist {1'b1:=1, 1'b0:=2};

           }) `uvm_error("MYERR", "This is a randomize error")
       end 
       $finish; 
    end 
endmodule  

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

• SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
  // For 10% discount, use code 45KJT5GN @ https://www.createspace.com/5810350
• A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
• Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
• Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
• Component Design by Example ", 2001 ISBN 0-9705394-0-1
• VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
• VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115

---

[ben2]

In reply to ben@SystemVerilog.us:
After more thoughts,

seq1 intersect seq2 
// equivalent to 
(seq1 within seq2) and (seq2 within seq1)

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

• SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
  // For 10% discount, use code 45KJT5GN @ https://www.createspace.com/5810350
• A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
• Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
• Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
• Component Design by Example ", 2001 ISBN 0-9705394-0-1
• VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
• VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115

---

[Mechanic]

Hi All,

Could you please let me know can we rewrite the above property with goto repetation also as below.If not let me know.

assert property (sop |-> read [->2] intersect write [->3] intersect eop [-> 1]);

It would be a great help if someone elaborate how the multiple intersect will work with both → and = Non consecutive operator.
Thanks in advance

[ben2]

In reply to sudharshan:

b[->2] // is equivalent to:
!b[*0:$] ##1 b ##1 !b[*0:$] ##1 b
// In other words any two "b"s ending with a "b"

b[=2] // is equivalent to:
  !b[*0:$] ##1 b ##1 !b[*0:$] ##1 b ##1 !b[*0:$]
// In other words any two "b"s not necessarily ending with a "b", 
// could be NO "b"s after the last "b"

// Thus, what you need is
assert property ($rose(sop) |=> read [=2] intersect write [=3] intersect eop [-> 1]);

http://SystemVerilog.us/vf/intersect1.sv

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home

• SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
• A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
• Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
• Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
• Component Design by Example ", 2001 ISBN 0-9705394-0-1
• VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
• VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115

---

1. SVA Alternative for Complex Assertions
   https://verificationacademy.com/news/verification-horizons-march-2018-issue
2. SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
3. SVA in a UVM Class-based Environment
   https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment

[Mechanic]

In reply to ben@SystemVerilog.us:

Thanks Ben for the clarification on the “->” and “=” operator.

1.In the image the Sop is rising exactly at the posedge clk so the assertion will active from the next clock similarly for write and read .
Since assertions are evaluated in the pre-poned region

As per my understanding if i use → operator then the 2nd read and 3rd write and EOP must happen simultaneously.

please correct me if i am wrong.

2.I know that intersect is similar to and but both the sequences must be of same length.
If there are multiple intersect as mentioned above i got confused How it behaves. could you please help me out.

Thanks in advance

[ben2]

In reply to Mechanic:

In reply to ben@SystemVerilog.us:
1.In the image the Sop is rising exactly at the posedge clk so the assertion will active from the next clock similarly for write and read . Since assertions are evaluated in the pre-poned region

I would rather think of the Sop being generated from a clocked FF, thus after the clocking event (@(posedge clk), Sop will be a 1’b1 after a small delay (2.g., 1 to 2ns), In assertions, as you know, all signals are sampled in the Preponed Region, just before the clocking event. Thus, the assertion starts (is successfully attempted) when the sampled value of the Sop is a 1’b1. The waveforms show signals rising at the clocking event, but that rise is NOT in the Preponed region, it’s; beyond that point, actually in the Nonblocking assignment region.

As per my understanding if i use → operator then the 2nd read and 3rd write and EOP must happen simultaneously.

That is correct.

2.I know that intersect is similar to and but both the sequences must be of same length. If there are multiple intersect as mentioned above i got confused How it behaves. could you please help me out.

Take a look at the syntax for a sequence

sequence_expr ::=
  cycle_delay_range sequence_expr { cycle_delay_range sequence_expr }
  ...
  | sequence_expr intersect sequence_expr
  | sequence_expr or sequence_expr
  ...
cycle_delay_range ::=
## constant_primary
| ## [cycle_delay_const_range_expression ]
| ##[*]
| ##[+]

// Thus, since a sequence can also be defined as 
sequence_expr intersect sequence_expr 
// then following is also a sequence 
sequence_expr intersect (sequence_expr intersect sequence_expr)

// If you want to know have it behaves, you can think of it as a 3 AND logic gate. 
// Each signal of that gate is true as long as the sequence it represents is true. 
// Example (not quite SVA, but a concept for simplicity 
logic a, b, s, s1_ab, s2_ac, s3_bc, T=1'b1;
int cycle; //  
sequence ab; a ##1 T ##1 b; 
sequence ac; a ##1 T ##1 c;
sequence bc; b ##1 T ##1 c;
assign s1_ab= (a && cycle==1) || (T && cycle==2) || (b && cycle==3);  
assign s1_ab= ...
// The intersect of the sequences ab, aC, bc is like gate ANDing s1_ab, s2_ac, s3_bc,
// Again, this is conceptual, just for explanation or analogies. 
 

Ben SystemVerilog.us

[Mechanic]

In reply to ben@SystemVerilog.us:

sop |->write[=2] and read [=3] ##0 eop[->1]
Does This assertion will also work for " there must be three reads and two wites between SOp and EOP"?

[ben2]

In reply to Mechanic:

 

sop |->write[=2] and read [=3] ##0 eop[->1]
// Does This assertion will also work for " there must be three reads and two wites between SOp and EOP"?
[Ben] yes and no, meaning that it may but without a guarantee 
// the following sequences satisfy the property 
// eop > WR.. RD.. RD.. RD.. EOP.. WR
// thus 3 reads followed by eop must occur with 2 writes. 
// the 2 parts of the Anding sequences must just occur, but each
// sequence can end at any time. One sequence can be 5 cycles, the other 200.


sop |->write[=2] intersect read [=3] ##0 eop[->1]
// This assertion will also work for " there must be three reads and two wites between SOp and EOP"

Ben systemverilog.us