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: forall and endpoint/ended
Posting to forums is available to community members only.
Login or Register
Rate this topic:
   
Author Messages
weberrm
Posts: 0
Online: User is Offline
3/18/2007 4:01 PM  
The module below has 2 assumption examples (one using endpoint and one using ended()).  In each of them, I am trying to only allow responses to addresses that have already had requests made to them.

Before forall support, a stable, undriven signal was used for the index in properties like the ones below.  Now, with forall support, I'm trying to come up with a more portable and complete solution.  However, both properties fail in the compilation.  Can someone explain the "undeclared identifier"s problem?  There only seems to be a "undeclared" problem inside of ended or endpoint.

Thanks!

module test
#(
parameter
MEM_D=8,
ADDR_W=3
)
(
input clk,
input rq_valid,rs_valid,
input [ADDR_W-1:0] rq_addr,rs_addr

);

//psl endpoint rq_to_rs(const i)=
// {rq_valid & rq_addr==i;~(rs_valid & rs_addr==i)[*] ; rs_valid & rs_addr==i}
//;

//psl assume_good_rs0: assume
// forall i in {0:MEM_D-1}: always(
// {rs_valid & rs_addr==i} |->
// {rq_to_rs(i)}
//)@(posedge clk);

//psl assume_good_rs1: assume
// forall i in {0:MEM_D-1}: always(
// {rs_valid & rs_addr==i} |->
// {ended({rq_valid & rq_addr==i;~(rs_valid & rs_addr==i)[*] ; rs_valid & rs_addr==i})}
//)@(posedge clk);


endmodule

Error with module above:
$ ifv test.v -s
ifv: 05.83-s001: (c) Copyright 1995-2007 Cadence Design Systems, Inc.
file: test.v
// {ended({rq_valid & rq_addr==i;~(rs_valid & rs_addr==i)[*]rs_valid & rs_addr==i})}
                               |
ncvlog: *E,UNDIDN (test.v,27|31): 'i': undeclared identifier ?.5(IEEE)].
// {ended({rq_valid & rq_addr==i;~(rs_valid & rs_addr==i)[*]rs_valid & rs_addr==i})}
                                                       |
ncvlog: *E,UNDIDN (test.v,27|55): 'i': undeclared identifier ?.5(IEEE)].
// {ended({rq_valid & rq_addr==i;~(rs_valid & rs_addr==i)[*]rs_valid & rs_addr==i})}
                                                                                 |
ncvlog: *E,UNDIDN (test.v,27|81): 'i': undeclared identifier ?.5(IEEE)].
        module worklib.test:v
                errors: 3, warnings: 2
ncvlog: *F,NOTOPL: no top-level unit found, must have recursive instances.
ncverilog: *E,VLGERR: An error occurred during parsing.  Review the log file for errors with the code *E and fix those identified problems to proceed.  Exiting with code (status 2).
ifv: *F,EXEERR: Errors encountered, exiting FormalVerifier. Check formalverifier.log for details.

Error if assume_good_rs1 is commented out.
$ ifv test.v -s
ifv: 05.83-s001: (c) Copyright 1995-2007 Cadence Design Systems, Inc.
file: test.v
// {rq_to_rs(i)}
|
ncvlog: *E,UNDIDN (test.v,21|0): 'assume_good_rs0_forgen_0__i': undeclared identifier ?.5(IEEE)].
        module worklib.test:v
                errors: 1, warnings: 1
ncvlog: *F,NOTOPL: no top-level unit found, must have recursive instances.
ncverilog: *E,VLGERR: An error occurred during parsing.  Review the log file for errors with the code *E and fix those identified problems to proceed.  Exiting with code (status 2).
ifv: *F,EXEERR: Errors encountered, exiting FormalVerifier. Check formalverifier.log for details.
TAM
Posts: 56
Online: User is Offline
4/19/2007 7:10 AM  
Just for an update for this issue. The problem seems to be a bug in the forall implementation when the forall index is used in any of the PSL built-in functions, ended() or prev() or whatever. The index is not recognized as having been declared. For what it is worth, the problem isn't in IFV itself, but appears in their language parser. It has been reported to Cadence R&D.
Posting to forums is available to community members only.
Login or Register


ActiveForums 3.6
     
Copyright 2006 Cadence Design Systems, Inc.