A Community of Verification Professionals

Create an Account	Home | Calendar | Downloads | FAQ | Links | Site Admin | Your Account
Login Nickname Password Security Code: Type Security Code BACKWARD Don't have an account yet? You can create one. As a registered user you have some advantages like theme manager, comments configuration and post comments with your name. Modules · Home · Downloads · FAQ · Feedback · Recommend Us · Web Links · Your Account Advertising Who's Online There are currently, 57 guest(s) and 0 member(s) that are online. You are Anonymous user. You can register for free by clicking here    Verification Guild: Forums  Forum FAQ   Search   Usergroups   Profile  Digest    Log in  PSL clocked SERE and endpoints problems          Verification Guild Forum Index -> Assertions View previous topic :: View next topic   Author Message Thrakath Senior Joined: May 11, 2004 Posts: 15 Location: Dresden, Germany Posted: Mon Jun 21, 2004 3:06 am    Post subject: PSL clocked SERE and endpoints problems Hi, I got a problem again. I want to discribe that a read signal must occur after a sequence in the input si. si is sampled on the posedge of sck. But the problem is that the legth of the read signal is half a clock and so i can not evaluate the read signal at a clockedge. Look below Code: sck__|-|_|-|_|-|_|-|_|-|_|-|_|-|_|-|_|-|_|-|_|-|_|-|_|-|   si__|--|___|--|___________________________________ read __________|-|__________________________________ How can I dicribe it? Should i Use endpoints and the eventually statement? My sugestion but i'm not sure. Code: always ({si;!si;si}@(posedge sck))->next read; Thanks Last edited by Thrakath on Mon Jun 21, 2004 9:18 am; edited 1 time in total Back to top bdeadman Senior Joined: Jan 06, 2004 Posts: 204 Location: Austin, TX Posted: Mon Jun 21, 2004 8:16 am    Post subject: I think the easiest way to do this is to sample on BOTH edges of the clock, and to use the clock signal in your expressions, for example, something like: always {{ (sck && si) ; (!sck) } |=> read }@ (edge sck); Note : I haven't checked the syntax! I am also confused by your diagram because I think the property won't be satisfied for the first sample of si is high. Regards Bernard Back to top Thrakath Senior Joined: May 11, 2004 Posts: 15 Location: Dresden, Germany Posted: Mon Jun 21, 2004 9:22 am    Post subject: Hi, sorry there was a little mistake. I`ve edit it. The problem of your solution is that read change on the edges of sck. So you can not sample it by the clock. I think i must check this with an unclocked statement but the startseqence must be clocked. Thanks Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1238 Location: Los Angeles, CA Posted: Mon Jun 21, 2004 9:28 am    Post subject: It looks like the READ is on the negedge of the clock. If so, Code: // psl property P = // always {si;!si;si}@(posedge sck)|=> {read}@ (negedge sclk); //  // you could also clock everything at the negege if that works out.   //psl default clock= (negedge sclk);   // psl property P2 = always {si;!si;si} |=> {read}; // FYI, and to start SV discussion, in SystemVerilog, the same thing can be expressed as: Code:   property p1; // no formal parameters used in this example    @ (posedge sclk) si ##1 !si ##1 si |=>                // now transitioning to 1st negedge of sclk     @ (negedge sclk) read;   endproperty : p1   p1_label: assert property (p1) else // if error    begin              $display ("%m @ time %t, p1 Failure, si= %b, read=%b", $time, si, read);       $warning ("P! ERROR no read when expected”);        handle_read_err <= 1’b1; // This can cause the testbench to take a reactive action     end;     // note: in SystemVerilog, everything is considered a SERE, thus no "{}"   //  are needed.   Also "##1" in SV is equivalent to ";" in PSL Ben _________________ Ben Cohen http://www.systemverilog.us/ * SystemVerilog Assertions Handbook, 3rd Edition, 2013 * A Pragmatic Approach to VMM Adoption * Using PSL/SUGAR ... 2nd Edition * Real Chip Design and Verification * Cmpt Design by Example * VHDL books Back to top Thrakath Senior Joined: May 11, 2004 Posts: 15 Location: Dresden, Germany Posted: Mon Jun 21, 2004 9:34 am    Post subject: Hi Sorry Ben but the READ goes high on the falling edge of SCK and then READ goes low on the next rising edge of SCK. I do not know on which pionts i could evaluate the READ signal Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1238 Location: Los Angeles, CA Posted: Mon Jun 21, 2004 9:39 am    Post subject: I provided a reply before reading that the READ signal is not synchronous to either edge of sclk. Code: //psl default clock = 1'b1; // take out effect of a predefined default clock, and make property // sensitive to signals in the property. / psl property P = // always {si;!si;si}@(posedge sck)(eventually! read); //  // you could also create a delayed clock from the READ in the testbench   assign rd_delayed = #1 read;     / psl property P2 = // always {si;!si;si}@(posedge sck)|=> {read}@ (posedge rd_delayed); //  // In SystemVerilog, you would need to create this artificial clock. // Ben _________________ Ben Cohen http://www.systemverilog.us/ * SystemVerilog Assertions Handbook, 3rd Edition, 2013 * A Pragmatic Approach to VMM Adoption * Using PSL/SUGAR ... 2nd Edition * Real Chip Design and Verification * Cmpt Design by Example * VHDL books Back to top bdeadman Senior Joined: Jan 06, 2004 Posts: 204 Location: Austin, TX Posted: Mon Jun 21, 2004 9:44 am    Post subject: Quote: The problem of your solution is that read change on the edges of sck Do you mean that the duration of read can be less than half a clock cycle, and that it cannot be quarateed to be true on EITHER posedge or negedge of sck? If that's the case you do indeed need an unclocked property, but the whole property can be unclocked if you include the clock into the enabling sequence - note: this is how the re-write rules of PSL define the semantics of clocked properties. I think this will ultimately be longer but more likely to work than endpoints etc., however I would need a more detailed description of the enabling sequence to be sure I have this right. If you apply the re-write rules in the LRM you'll end up with something like: { (sck && si) ; !sck ; {sck && !si}[*] ; (sck && si) ; !sck } |-> read Note : you'll need to make sure any default clock you've specified doesn't apply. Regards Bernard Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1238 Location: Los Angeles, CA Posted: Mon Jun 21, 2004 9:51 am    Post subject: It looks like my replies are not synchronized with the actual posts. WHile I am composing a reply, a new reply shows up! Anyway, Quote: Sorry Ben but the READ goes high on the falling edge of SCK and then READ goes low on the next rising edge of SCK. I do not know on which pionts i could evaluate the READ signal In that case, you could simply use the rising edge of sclk as the default clock. Code: clk     r    f    r    f   // r= rise, f=fall read   0001111000 // I show a delta time after rising edge before                            // read goes low. Thus,          default clock = posedge sclk; always {si;!si;si}|=> {read}; Am I seeing som ething wrong on this? Ben _________________ Ben Cohen http://www.systemverilog.us/ * SystemVerilog Assertions Handbook, 3rd Edition, 2013 * A Pragmatic Approach to VMM Adoption * Using PSL/SUGAR ... 2nd Edition * Real Chip Design and Verification * Cmpt Design by Example * VHDL books Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1238 Location: Los Angeles, CA Posted: Mon Jun 21, 2004 9:56 am    Post subject: The timing diagram did not show up well. You'll need to redraw it. But from what you wrote, READ is valid at the rising edge of sclk. _________________ Ben Cohen http://www.systemverilog.us/ * SystemVerilog Assertions Handbook, 3rd Edition, 2013 * A Pragmatic Approach to VMM Adoption * Using PSL/SUGAR ... 2nd Edition * Real Chip Design and Verification * Cmpt Design by Example * VHDL books Back to top Thrakath Senior Joined: May 11, 2004 Posts: 15 Location: Dresden, Germany Posted: Tue Jun 22, 2004 1:44 am    Post subject: Hi, ok iwill redraw the diagram but it is difficult. Code:   _   _   _   _   _   _   _   _   _   _   _   _ _/ \_/ \_/ \_/ \_/ \_/ \_/ \_/ \_/ \_/ \_/ \_/ \ sck    ____    ____ __/    \__/    \__________________________si                 _ _______________/ \_____________________read sck ist the clock si is valid on the posedge sck read goes high on the negedge of sck and Low on next rising edge of sck If i use a defaultclock for sampling the start sequence on SI I do not know how to check READ, because READ is not valid on any edges of SCK. Is it posible to discribe it without an extra clock? Another point is that start sequence could be also 1 0 0 and not only 010. So the startseqence must be clocked. There is a second problem. If i want to sample the the start condition on the posedge and the answer sequence on the negedge of the clock the ncverilog from cadence will not compile it. (expecting statement Termintaor ';') Code: always {si;!si;si}@(posedge sck)|=>{read}@(negedge sck); What is wrong at this code? Thanks Last edited by Thrakath on Tue Jun 22, 2004 12:10 pm; edited 1 time in total Back to top bdeadman Senior Joined: Jan 06, 2004 Posts: 204 Location: Austin, TX Posted: Tue Jun 22, 2004 10:30 am    Post subject: First, you wrote Quote: read goes high on the negedge of sck and high on next rising edge of sck I assume this is a typo, and it should have read Quote: read goes high on the negedge of sck and ***LOW*** on next rising edge of sck If this is correct, how does read go low? If read is set from a state machine, or some other latch that's clocked by sck, OR if it's derived from sck by a non-blocking assignment (VHDL / SystemC assignments are also good) then I think it ought to be OK to sample the property using posedge sck. If this is not the case, my suggestion is still to use an unclocked property, but follow the re-write rules in the LRM to manually convert the enabling expression (LHS) from clocked to un-clocked. Regards Bernard Back to top Thrakath Senior Joined: May 11, 2004 Posts: 15 Location: Dresden, Germany Posted: Tue Jun 22, 2004 12:13 pm    Post subject: oh Bernhard, you are right. It was a typo. Low is correct. Read is set by a state machine. I will try to convert the clocked seqence in an unclocked seqence. Thanks all Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1238 Location: Los Angeles, CA Posted: Tue Jun 22, 2004 2:39 pm    Post subject: Quote: Read is set by a state machine. I will try to convert the clocked seqence in an unclocked seqence. I am missing something here. Isn't your FSM clocked? Even if READ is derived using combinational logic, it still is derived from your clocked FSM, and you should be able to check it a clock edge. Ben _________________ Ben Cohen http://www.systemverilog.us/ * SystemVerilog Assertions Handbook, 3rd Edition, 2013 * A Pragmatic Approach to VMM Adoption * Using PSL/SUGAR ... 2nd Edition * Real Chip Design and Verification * Cmpt Design by Example * VHDL books Back to top Thrakath Senior Joined: May 11, 2004 Posts: 15 Location: Dresden, Germany Posted: Wed Jun 23, 2004 6:51 am    Post subject: hi This is not my design. Read is driven by a kobinatorik witch is a gate for SCK. The kobinatorik is driven by a state machine whith is clocked by SCK. Back to top Display posts from previous: All Posts1 Day7 Days2 Weeks1 Month3 Months6 Months1 Year Oldest FirstNewest First         Verification Guild Forum Index -> Assertions All times are GMT - 5 Hours Page 1 of 1   Jump to: Select a forum Main----------------MainEDA NewsCommunity Services Networking----------------Looking for a jobLooking for candidates Archives----------------AssertionsCoverageFormalSimulationDesignMiscellaneous Test----------------Test  You can post new topics in this forum You can reply to topics in this forum You cannot edit your posts in this forum You cannot delete your posts in this forum You cannot vote in polls in this forum Forums ©

Verification Guild © 2006 Janick Bergeron
Web site engine's code is Copyright © 2003 by PHP-Nuke. All Rights Reserved. PHP-Nuke is Free Software released under the GNU/GPL license.
Page Generation: 0.674 Seconds