| Login | | 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. | |
| Who's Online | There are currently, 64 guest(s) and 1 member(s) that are online.
You are Anonymous user. You can register for free by clicking here | |
 | |
|
Verification Guild: Forums |
|
| View previous topic :: View next topic |
| Author |
Message |
hemanth
Senior
Joined: Aug 16, 2004
Posts: 93
Location: Bangalore
|
 Posted: Fri Nov 19, 2004 1:33 am Post subject: |
 |
|
| romi wrote: | Thanks for the input. I get compile errors with cindy's examples.
| Code: |
// psl a_to_b0: assert always ( a -> (b | next (b before a)));
|
ncvlog: *E,ILLPRI (/test.v,15|45): illegal expression primary [4.2(IEEE)].
// psl a_to_b0: assert always ( a -> (b | next (b before a)));
|
ncvlog: *E,EXPRPA (/test.v,15|55): expecting a right parenthesis (')') [4.3][9.7(IEEE)].
// psl a_to_b0: assert always ( a -> (b | next (b before a)));
|
ncvlog: *E,ALXSCN (/test.v,15|60): Expected statement terminator ";".
// psl a_to_b1: assert always ( {a} |-> { b | { true ; (~a & ~b)[*] ; ~a & b }});
|
ncvlog: *E,ILLPRI (/test.v,16|51): illegal expression primary [4.2(IEEE)].
|
Is there something obvious that I'm missing? Thanks again. |
Romi,
Yes your first property compiles but only if the '|' is replaced by '||' but I am not sure why it has to be so, as both are valid verilog constructs and should hold for single bit values.
The second property works, but apart from changing true to [*1] you will have to put the first 'b' in the expression within braces as we can only OR compound seres and braces are reqd around 'b' for that.
hemanth |
|
| Back to top |
|
 |
hemanth
Senior
Joined: Aug 16, 2004
Posts: 93
Location: Bangalore
|
| Posted: Fri Nov 19, 2004 2:01 am Post subject: |
|
|
It appears that we can only use verilog constructs '||' and '&&' (as opposed to '|' and '&') when combining psl expressions in verilog domain (refer psl lrm v1.1 page 33). So I guess what romi observed is along right lines. hence my earlier observation about both being verilog constructs is inconsequential because we actually have a psl expression as characterized by keywords -next and before.
hemanth |
|
| Back to top |
|
|
cindy
Industry Expert
Joined: Aug 17, 2004
Posts: 309
|
| Posted: Sun Nov 21, 2004 2:17 am Post subject: |
|
|
ben,
please note that your proposed solution:
| Code: | | always (a -> next (b before_ a)) |
is not the same as the property described by the formula we were discussing:
| Code: | | always (a -> (b || next (b before a))) |
to see why, consider a trace such that "a" is asserted at cycles N and N+1 (and for simplicity, at no other cycle in the trace), and "b" is asserted at cycle N+1. the first property above holds on this trace, but the second does not.
cindy. |
|
| Back to top |
|
|
vhdlcohen
Industry Expert
Joined: Jan 05, 2004
Posts: 1237
Location: Los Angeles, CA
|
| Posted: Sun Nov 21, 2004 5:44 pm Post subject: |
|
|
Cindy,
You're correct:
| Code: |
always (a -> next (b before_ a))
would be satisfied by either
sequence a !b&&!a !b&&!a ... !b&&!a ba
or sequence a !b&&!a !b&&!a ... !b&&!a b |
and | Code: |
always (a -> (b || next (b before a)))
would be satisfied by either
sequence ab
or sequence a !b&&!a !b&&!a .. !b&&!a b&&!a |
I would add there there is a need to change in the antecedent "a" to "rose(a)" to avoid possible errors when only the first change in "a" is needed.
Thanks Cindy for pointing my error.
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 |
|
|
|
|
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
|
| |
|
|
Forum FAQ
Search
Usergroups
Profile
Digest
Log in
