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: Using Assertions to test arbiter priority
Posting to forums is available to community members only.
Login or Register
Rate this topic:
   
Author Messages
gobuffs
Posts: 3
Online: User is Offline
12/12/2007 9:46 AM  
Can anyone share how they use PSL to test arbiter priority? In other words, if I have multiple req inputs, and the priority is hardcoded (reqA higher than reqB, whch is higher than reqC), how can I use ABV to test this?
jmueller
Posts: 14
Online: User is Offline
12/13/2007 1:04 AM  
Hi Gobuffs,

there are 2 excellent places to look at:

1) the IAL library (part of any IUS installation) contails a item called ial_arbiter. It is qualified for simulation.
2) in the IFV installation there are 4 vcomps, one of them is the vcomp_arbiter (IFV62-p001/doc/ifvref/example/meth/verif_docs/vcomp_arbiter.zip). It is qualified for formal verification.

Both of them can serve as starting point or template for your verification task.

Regards,
Joerg.
gobuffs
Posts: 3
Online: User is Offline
12/19/2007 1:56 PM  
I can't find anything in ial_arbiter.vlib that answers my question.  Anyone else have any thoughts?
jb
Posts: 16
Online: User is Offline
12/19/2007 2:29 PM  
If your arbiter is a priority encoded arbiter. You should be able to create the following series of properties to ensure the priority encoding is working. These properties work on the premise that the currently granted channel has its req asserted and no other higher requests asserted. The goal of these properties is to give you a starting point to customize your own properties for your specific design.

Given:

4 input priority encoded arbiter with channels a, b, c, and d. Channel a has the highest priority and d the lowest.

// psl assert_A_should_be_granted: assert always {gnta} |-> {reqa};
// psl assert_B_should_be_granted: assert always {gntb} |-> {regb & !rega};
// psl assert_C_should_be_granted: assert always {gntc} |-> {reqc & !reqa & !reqb};
// psl assert_D_should_be_granted: assert always {gntd} |-> {reqd & !reqa & !reqb & !reqc};

You will probably have to fine tune these properties to handle other channels arbitrating for service while the current channel is granted but I hope you get the idea. In reality you may have to create aux signals that you can place into these properties to check for grants at the correct points in time in the arbitration.

In other words, the language behind assert_A_should_be_granted should read: IF channel a is granted I just have to make sure channel A requested service at the appropriate time.

For the property assert_D_should_be_granted it should read: If channel d is granted, I must have had no other higher priority channels requesting service.

Hope this helps.

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


ActiveForums 3.6
     
Copyright 2006 Cadence Design Systems, Inc.