Thursday, July 29, 2010     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: how to aggregate tests and results
Posting to forums is available to community members only.
Login or Register
Rate this topic:
   
Author Messages
e_vangelist
Posts: 5
Online: User is Offline
4/14/2008 4:05 AM  
Hi,

It is the first time I used formal verification. In my case, I verified an internal bus protocol by writing some PSL assertions. I developped some overconstraints to configure the tool : like never write or never read an so on...
But I am not allowed to change them unless a reset command is done, that I do not want to issue. Is the tool is able to aggreate the results in different configurations?

Do you have another ideas apart from merging scripts ?

Thanks for your answers

Fred
jmueller
Posts: 14
Online: User is Offline
4/14/2008 4:56 AM  
Hi Fred,

before I can think of alternatives I need to understand what you want to achieve. I understand that you wrote properties to check a bus protocol and use formal verification to exhaustively verify the interface. But what is the benefit of splitting and merging the verification? Don't you want to guarantee protocol compliance in all possible scenarioes?

Thanks,
Joerg.
e_vangelist
Posts: 5
Online: User is Offline
4/14/2008 5:25 AM  
Hi Joerg,


Thanks to help me, I really appreciate it.
Just for clarifyng:
My exact role is to verify and correct the contents of the PSL versus the spec and run them on an already verified IP. So I am not the developper of the PSL but I 'm acting as a reviewer.

So, I understand your questions.
"But what is the benefit of splitting and merging the verification? Don't you want to guarantee protocol compliance in all possible scenarioes?"

The thing is that we use those overcontrains to trigger some assertions that were not triggered without overconstaints. At the end, I want to merge or split all the results whether I am using particular overcontraint or not.

ex :
run without overconstraint
status : 3 properties no triggered
run with set of overcontrains
3 properties are triggered and passing but others are not triggered.

How to merge the results ?


Thanks for your help Joerg !

See you,

Fred
jmueller
Posts: 14
Online: User is Offline
4/14/2008 5:40 AM  
Hi Fred,

I still don't fully understand.

If a property does not trigger in one environment, then it will also not trigger if you add constraints (overconstraint). Only if you remove constraints there is a chance to trigger previously untriggered properties.

If you want to verify a set of protocol properties I recommend to systematically inject errors in the design and test if they are caught by the properties. Other methods include back to back testing. The IFV Advanced Training has a section dedicated to this type of property development and verification.

Regards,
Joerg.
e_vangelist
Posts: 5
Online: User is Offline
4/14/2008 5:49 AM  
Ok Joerg,

Thanks , it seems I need some IFV training. I will ask cadence for near future.

Best regards,

Fred
Posting to forums is available to community members only.
Login or Register


ActiveForums 3.6
     
Copyright 2006 Cadence Design Systems, Inc.