Question on "implies" operator of the property expression

SystemVerilog
1

Hi,

I am having following question on the “implies” operator of properties:

  1. I have come across following Logic to be implemented in one of the books on SVA assertions :

A signal sig should be high from m >= 0 clocks before an event ev happens and should remain high until n >= 0 clocks after the event. That is if event ev happens at time 10, m= 2 and n = 3, then sig should be high from clock tick 8 to 13. Now solution given is


a1: assert property (strong (##m ev) implies sig [*(m+n+1)]);

The book also says this is equivalent to


a2: assert property (!sig |-> !ev [*(m+1)]) and (ev |-> sig[*(n+1)]));

Now my understanding is that - assertion a1 consists of two properties connected by implies which start execution at same time. So the event ev takes place after initial delay of m clock ticks and sig remains high for m+n+1 clocks. So sig is high m clocks before ev and high n clocks after ev - which is what the problem specification requires. (is this understanding correct?)
However, I am not clear about how assertion a2 implements the same logic. I am clear about second part of a2 i.e. (ev |-> sig[(n+1)]. After ev takes place signal sig is high for n+1 clocks starting with the clock at which ev happens. However, the first part of assertion a2 ((!sig |-> !ev [(m+1)])) is not clear to me. Can someone explain this. (I am just wondering if there is some typo in the book).

  1. Also the book says that following two properties p1 and p2 are equivalent. I am not clear about how they are equivalent. How does one establish the equivalence of p1 and p2


property p1;
not (a[*] ##1 b);
endproperty

property p2;
not (!b[+] ##0 !a);
endproperty

rgs,
-sunil

2

In reply to puranik.sunil@tcs.com:

let m=2; let n=3;
	bit clk, a, b, sig;  
	// event ev;  // Illegal event value in SVA expression.
// ****** ev cannot be an event !!!!**
	let ev = a==b; // **OK** 
	default clocking @(posedge clk); endclocking
	initial forever #10 clk=!clk;  
	//A signal sig should be high from m >= 0 clocks before an event ev happens 
	// and should remain high until n >= 0 clocks after the event. 
	// That is if event ev happens at time 10, m= 2 and n = 3, 
	// then sig should be high from clock tick 8 to 13. Now solution given is 
	a1: assert property (strong (##m $rose(ev)) implies sig [*(m+n+1)]);
    // The book also says this is equivalent to 
    a2: assert property ((!sig |-> !$rose(ev) [*(m+1)]) and ($rose(ev) |-> sig[*(n+1)]));

Comments:

  1. Ev cannot be an event, it has to be an expression
  2. I would use the $rose(ev)
  3. I don;t believe you need the strong in the antecedent of the implies.
  4. a2 is very similar to a1 and expresses the same notion (IMHO), but they are not totally eauivalent. The big difference between the two is vacuity.
    The best way to run a simulation and do the comparison. See my test results and the model below.

1300×585 47.4 KB

1326×624 35.9 KB

Link to test model for implies

On the properties below, I don’t see how they are equivalent.


 property p1;
       not (a[*] ##1 b);
       // not(a[*0:$] ##1 b) // equivalent
       // not(a[*0] ##1 b or a[*1:$] ##1 b) // equivalent
       // not(b or (a[*1:$] ##1 b))  // equivalent
    endproperty
 
    property p2;
      not (!b[+] ##0 !a);  // equivalent
      // not (!b[*1:$] ##0 !a);
    endproperty

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
3

Hi Ben,

thanks for a detailed reply. I have one more question on equivalence of properties :

s #-#  p

is equivalent to

not (s |-> not p)


p s_until q

is equivalent to

not ((not q) until_with (not p))

p until q

is equivalent to

 not ((not q) s_until_with (not p))

Is there is any formal proof to prove these equations?

rgs,
-sunil

4

In reply to puranik.sunil@tcs.com:

Is there is any formal proof to prove these equations?

I don’t know how exactly how these equivalences were derived. But empirically, they do work.
I am more of a practical guy than a math guy.
Ben SystemVerilog.us

5

Hi Ben,
this is given in the book on SVA which I am reading.
I also work in verification of ASIC designs and do not work in mathematics but just wanted to know out of curiosity. Thanks anyways for replying.
rgs,
-sunil