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 3:00 PM by archive. 0 replies.
Started by archive 18 Mar 2007 03:00 PM. Topic has 0 replies and 1676 views
Page 1 of 1 (1 items)
Sort Posts:
  • Sun, Mar 18 2007 3:00 PM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    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 expalain the "undeclared identifier"s problem?  There only seems to be a "undeclared" problem inside of ended or endpoint.

    Thanks!

    <br>module test<br>#(<br>parameter<br>MEM_D=8,<br>ADDR_W=3<br>)<br>(<br>input clk,<br>input rq_valid,rs_valid,<br>input [ADDR_W-1:0] rq_addr,rs_addr<br><br>);<br><br>//psl endpoint rq_to_rs(const i)=<br>// {rq_valid & rq_addr==i;~(rs_valid & rs_addr==i)[*];rs_valid & rs_addr==i}<br>//;<br><br>//psl assume_good_rs0: assume<br>// forall i in {0:MEM_D-1}: always(<br>// {rs_valid & rs_addr==i} |-> <br>// {rq_to_rs(i)} <br>//)@(posedge clk);<br><br>//psl assume_good_rs1: assume<br>// forall i in {0:MEM_D-1}: always(<br>// {rs_valid & rs_addr==i} |-> <br>// {ended({rq_valid & rq_addr==i;font>font><font color="#0000ff"><font face="Courier New">~(rs_valid & rs_addr==i)font>font><font color="#0000ff"><font face="Courier New">[*];rs_valid & rs_addr==i})} <br>//)@(posedge clk);<br><br><br>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 [12.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 [12.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 [12.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 [12.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
Page 1 of 1 (1 items)
Sort Posts:
Started by archive at 18 Mar 2007 03:00 PM. Topic has 0 replies.