Wednesday, February 08, 2012     Register | Login | Search | Contact Us
     
   
     
     

Many of you already received communications about the move of the Cadence user community into cadence.com. And many of you have already joined, with over 4000 registrations in the first two weeks.

The new Cadence Community enhances the ability of Cadence users to connect and collaborate. In addition to moving the community into cadence.com -- enabling single sign-on for community, Sourcelink and Cadence events -- the new site is organized around nine technology segments, giving you easy access to product information, training, forums and blogs. Some of the new features include:
  • Ability to respond to posts via e-mail
  • Technology-specific blogs
  • Latest Web 2.0 social networking capabilities
  • Public profile options
  • Private messaging
  • Friends lists
Visit the new Cadence Community today at www.cadence.com/community and join the discussions!

Registration note: Due to the scope of the enhancements and the new SSO registration system, we were not able to migrate existing cdnusers.org member accounts. So new registrations are required, but this enables a broader set of functionality we think you'll enjoy.

Forum note: Under the guidance of forum moderators, we have taken the 20+ cdnusers.org forums and consolidated them into 11 forums on the new site. Posts have been brought over so you can leverage that posting history. CDNusers forums will be set to read only starting 7/30, and cdnusers.org will be redirected to the new community on 8/4.

Best regards,
Mike and Tom

Michael A. Catrambone - Steering Committee Chairman
Distinguished Engineer
PCB/Mechanical
UTStarcom, Inc.

Tom Diederich
Cadence Community Manager
Home
Forums
Forums > Functional Verification > Assertion-Based Verification and Formal Analysis

Subject: Property transformations
Posting to forums is available to community members only.
Login or Register
Rate this topic:
   
Author Messages
TG
Posts: 1
Online: User is Offline
11/07/2006 5:06 AM  
There are many ways of specifying the same behaviour by writing a variety of PSL/SVA assertions.
For example, a specification says that after req the grant should come within 5 clock cycles. I wrote it
like

// psl property P1:  (always ( req ) -> {!gnt[*0:4] ; gnt } ) @ (posedge clk);

how do I write this same property using the never form ?
Can this behaviour be written in any other form ? What are the advantages disadvantages of these
different forms.

TG
TAM
Posts: 56
Online: User is Offline
11/07/2006 7:28 AM  
You could write it in the "never" form by saying, "we'll never see grant low for more than 4 clock cycles after a request."

// psl property P1: never { req; !gnt[*5] };

What you lose with this form is the concept of a "trigger." When you use the implication operator, the tool will keep track of the number of times the check was triggered, in this instance the number of times a request was made. In the "never" form, there is no specific trigger for the assertion, it checks for the sequence at every cycle.
axels
Posts: 0
Online: User is Offline
11/07/2006 12:47 PM  

The suggestion for the conversion into a never {sequence} form is not quite right.
There are problems with the first expression of the sequence and with
the timing (repetition value).

It should be:

    never {req && ! gnt; !gnt[*4]} @(posedge clk);

The first expression needs to be extended to include " && !gnt"
The timing needs to be shortened to "*4".
Beware that the original property used a non-overlapping implication operator.


Generally it is recommend to double check the converted version using the tool
by using the following procedure:
–
  1. put the original and derived property into a dummy module
  2. run the original as a constraint and the derived one as an assertion
  3. prove
  4. reset
  5. flip the original into an assertion and the derive into a constraint
  6. prove
It is important to check it both ways. Otherwise the constraining of
one property could mask a problem.

This could be automated with scirpts

In this particular case do the following:

dummy.v:

module dummy (input clk, output req, gnt);
// psl P1_orig: assume (always (req) -> {!gnt[*0:4] gnt}) @(posedge clk);
// psl P1_derived: assert never {req && !gnt; !gnt[*4]} @(posedge clk);
endmodule

dummy.tcl:
# run1
prove
constraint -show

reset
# flip it
assertion  -del -all
constraint -del -all
assertion  -add *orig
constraint -add *derived
# run2
prove
constraint -show


ifv dummy.v +tcl+dummy.tcl
TAM
Posts: 56
Online: User is Offline
11/07/2006 12:54 PM  
Oops, Axels is right. I read the original sequence as if it used the non-overlapping implication operator |=>, while in fact it appears as if it was supposed to be using the overlapping form of that operator |->.
Posting to forums is available to community members only.
Login or Register


ActiveForums 3.6
     
Copyright 2006 Cadence Design Systems, Inc.