Home > Community > Forums > Functional Verification > forall and endpoint/ended

Email

* Required Fields

Recipients email * (separate multiple addresses with commas)

Your name *

Your email *

Message *

Contact Us

* Required Fields
First Name *

Last Name *

Email *

Company / Institution *

Comments: *

 forall and endpoint/ended 

Last post Sun, Mar 18 2007 4:01 PM by archive. 1 replies.
Started by archive 18 Mar 2007 04:01 PM. Topic has 1 replies and 998 views
Page 1 of 1 (2 items)
Sort Posts:
  • Sun, Mar 18 2007 4:01 PM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,910
    forall and endpoint/ended Reply

    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.


    Originally posted in cdnusers.org by weberrm
    • Post Points: 0
  • Thu, Apr 19 2007 7:10 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,910
    RE: forall and endpoint/ended Reply

    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.


    Originally posted in cdnusers.org by TAM
    • Post Points: 0
Page 1 of 1 (2 items)
Sort Posts:
Started by archive at 18 Mar 2007 04:01 PM. Topic has 1 replies.