| 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, 50 guest(s) and 0 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 |
gallopr
Newbie
Joined: Nov 10, 2004
Posts: 1
|
 Posted: Wed Nov 10, 2004 7:58 am Post subject: PSL Newbie question |
 |
|
Am trying to write a property to check the value out of a register is not x the cycle after a readspecifer is non zero. This is just like some simple examples I have but involves buses and comparisons which I think are what is catching me out.
I currently have:
| Code: | | property RegReadPortNotX = never ((readspec[5:0] !== 6'h0) -> next ((^(out0[31:0])) === 1'bx)); |
but I get an error compiling with ncvlog:
| Code: | | Illegal context for a Sugar formula. |
at the -> operator.
Any ideas?
Thanks
Russ |
|
| Back to top |
|
 |
vhdlcohen
Industry Expert
Joined: Jan 05, 2004
Posts: 1237
Location: Los Angeles, CA
|
| Posted: Wed Nov 10, 2004 9:40 am Post subject: |
|
|
| Quote: | | property RegReadPortNotX = never ((readspec[5:0] !== 6'h0) -> next ((^(out0[31:0])) === 1'bx)); |
You should never use a "never" with an implication operator because it will yiled errors. and many compilers now forbid it. Specifically,
never (a -> b) says that the property a-> b should always be FALSE.
The never of false is true. But if "a" is zero or false, then a -> b is vacuously TRUE,
Change you code to:
| Code: | | property RegReadPortNotX = never {readspec[5:0] !== 6'h0 ; ^(out0[31:0]) === 1'bx}; |
I am not sure about your comparison of a 32 bit vector to a 1 bit though!
But the concept is to use "never {sequence}" instead of the implication.
Ben Cohen
_________________
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 |
|
|
hemanth
Senior
Joined: Aug 16, 2004
Posts: 93
Location: Bangalore
|
| Posted: Mon Nov 15, 2004 2:26 am Post subject: |
|
|
I think you can convert that NEVER to an equivalent ALWAYS and write something like-
property RegReadPortNotX = always((readspec[5:0] !== 6'h0) -> next(^(out0[31:0]) !== 1'bx)); |
|
| Back to top |
|
|
vhdlcohen
Industry Expert
Joined: Jan 05, 2004
Posts: 1237
Location: Los Angeles, CA
|
| Posted: Mon Nov 15, 2004 11:36 am Post subject: |
|
|
| Quote: | I think you can convert that NEVER to an equivalent ALWAYS and write something like-
property RegReadPortNotX = always((readspec[5:0] !== 6'h0) -> next(^(out0[31:0]) !== 1'bx)); |
In the general case, to state that:
if(A) then never B at next cycle, and
if(!A) then vacuously true
you can write one of the followings:
never {A ; B} // never of a sequence
always {A} |=> {!B} // I prefer sequences
always {A} |=> {B} |-> {false}
This last case is valid because a property is defined as:
FL_Property ::= // among other things
Sequence [ ! ]
| Sequence |-> FL_Property
| Sequence |=> FL_Property
and thru recursion, you get:
FL_Property ::=
Sequence |=> Sequence |-> FL_Property
A tool supports that fully supports PSL should support this.
Ben Cohen
_________________
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
