| 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, 41 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 |
bugfinder
Senior
Joined: Jan 12, 2004
Posts: 19
|
 Posted: Sun Dec 05, 2004 11:47 pm Post subject: Using assertions to check multiple changes within a cycle |
 |
|
Hi Ben,
I am not sure whether thisthread is the right place to post this question.
| The moderator wrote: | | Please start a new thread if a question/topic is significantly different from the one described by the subject lines. Topics/threads can be links via URLs. |
A general question I have.
Is it possible to write assertions(PSL or SVA) on VHDL variables which will
change values multiple time within a clock cycle. Ex:
process(clk,reset)
variable a: integer range 0 to 63;
begin
.,..
a: = b + c;
....
a := c * d;
...
a := x + y;
end process;
I want to check whether variable 'a' always stays within a predefined range etc.
Do current tools support in dynamic simulations(modelsim/vcs-mx).
A sub question is, can I write different assertions at different points in the
process on the same variable.
Thanks. |
|
| Back to top |
|
 |
hemanth
Senior
Joined: Aug 16, 2004
Posts: 93
Location: Bangalore
|
| Posted: Mon Dec 06, 2004 12:33 am Post subject: |
|
|
Below are the restrictions in latest version of modelsim:
Embedded assertions have the following restriction as to where they can be embedded:
• Assertions can be embedded anywhere inside a Verilog module except initial blocks,
always blocks, tasks, and functions. They cannot be embedded in UDPs.
• Assertions can be embedded only in declarative and statement regions of a VHDL entity
or architecture body.
• In a statement region, assertions can appear at places where concurrent statements may
appear. If they appear in a sequential statement, ModelSim will generate an error.
• Assertions cannot be embedded in VHDL procedures and functions.
As you can see it effectively rules out using variables(shared variables go through).
The psl lrm itself dosent talk about this(its mentioned that boolean expressions contain signals or memory elements) but its requirement is that a basic expression must describe the state of a design. Though I believe this dosent rule out variables explicitly, I think it has to do with sequential design when states are decided at specific edges of clock. But then it may be so that even if variables(shared for ex) are used their value is visible only at an edge of the clock in a psl clocked expression..is this entirely correct ?
I would like to hear others opinions on this.
-Hemanth |
|
| Back to top |
|
|
srini
Senior
Joined: Jan 23, 2004
Posts: 430
Location: Bengaluru, India
|
| Posted: Mon Dec 06, 2004 9:37 am Post subject: Re: Assertions on VHDL Variables |
|
|
| bugfinder wrote: | Hi Ben,
A general question I have.
Is it possible to write assertions(PSL or SVA) on VHDL variables which will
change values multiple time within a clock cycle. Ex:
|
PSL doesn't support immediate assertions - i.e. it can't extract the "context" where the PSL code is embedded. I think it is under consideration for next release(s) though. SVA supports it fully, but truly speaking it is in the context of SystemVerilog/Verilog. However a capable mixed-mode simulator in principle shall allow inlined SVA comments inside VHDL process as you are looking for (though I believe there is an elegant solution for your specifci example case, see below). While it may look as if SVA + VHDL is mixed-mode against PSL + VHDL - from a language perspective both are mixed-language solutions as of today.
| Quote: |
process(clk,reset)
variable a: integer range 0 to 63;
begin
.,..
a: = b + c;
....
a := c * d;
...
a := x + y;
end process;
I want to check whether variable 'a' always stays within a predefined range etc.
|
A simple VHDL solution will be to use
| Code: |
assert (a > min_value and a < max_value) report "error"
|
Few notes:
-Just pseudo code, need to fix syntax.
- Hopefully the different assignments you've shown are mutually exclusive, if not, you need to insert this piece of assertion every where you change the variable.
- Also there is OVL available for it.
| Quote: |
Do current tools support in dynamic simulations(modelsim/vcs-mx).
|
VCS-MX does support SVA + VHDL today, call your AE for more on this.
| Quote: |
A sub question is, can I write different assertions at different points in the
process on the same variable.
Thanks. |
Again, this will go back to "context" awareness of your assertion language - PSL isn't while SVA is. However, I would recommend you use the "correct" solution for the problem in hand - in your example (perhaps it was rather a toy example) you are better off using OVL/VHDL assert than any thing more complex. The real power of assertion languages come from temporal specifications - IMO.
HTH,
Srini
_________________
Srinivasan Venkataramanan
Chief Technology Officer, CVC www.cvcblr.com
A Pragmatic Approach to VMM Adoption
SystemVerilog Assertions Handbook
Using PSL/SUGAR 2nd Edition.
Contributor: The functional verification of electronic systems |
|
| Back to top |
|
|
cindy
Industry Expert
Joined: Aug 17, 2004
Posts: 309
|
| Posted: Tue Dec 07, 2004 3:45 am Post subject: |
|
|
bugfinder,
| Quote: | Is it possible to write assertions(PSL or SVA) on VHDL variables which will
change values multiple time within a clock cycle. |
yes, this is possible in psl, using an unclocked assertion.
the clock in psl is used to ensure that different kinds of tools (for instance, cycle-based vs. event-based) will give the same result. the purpose of having unclocked properties is not to lose access to the finer granularity of time as seen by some of the tools. to quote the lrm v1.1, p. 24:
| Quote: | | PSL does not dictate how time ticks for an unclocked property. Thus, unclocked properties are used to reason about the sequence of signal values as seen by the verification tool being used. For instance, a cycle-based simulator sees a sequence of signal values calculated cycle-by-cycle, while an event-based simulator running on the same design sees a more detailed sequence of signal values. |
as to this question:
| Quote: | | Do current tools support in dynamic simulations(modelsim/vcs-mx). |
i suspect not, but i do not know. the language, however, supports it, for any tool vendor interested in implementing it in the future.
srini,
| Quote: | | PSL doesn't support immediate assertions - i.e. it can't extract the "context" where the PSL code is embedded. |
the term "immediate assertion" is an sva concept, referring to a test of an expression when the assertion statement is executed. the fact that psl does not define an animal called "immediate assertion" nor does it allow assertions to be mixed freely with design code, does not mean that the language is not capable of doing what bugfinder wants.
to summarize, the following unclocked property:
| Code: | | assert always (a > min_value & a < max_value); |
states that signal "a" must stay within the specified range, including transitory behavior within a clock cycle.
note that this psl assertion stands alone, outside of the design. thus, only a single instance of the assertion is needed, even if there are multiple non-mutually exclusive assignments to "a" within the code.
cindy. |
|
| Back to top |
|
|
srini
Senior
Joined: Jan 23, 2004
Posts: 430
Location: Bengaluru, India
|
| Posted: Tue Dec 07, 2004 4:02 am Post subject: |
|
|
| cindy wrote: |
srini,
| Quote: | | PSL doesn't support immediate assertions - i.e. it can't extract the "context" where the PSL code is embedded. |
the term "immediate assertion" is an sva concept, referring to a test of an expression when the assertion statement is executed. the fact that psl does not define an animal called "immediate assertion" nor does it allow assertions to be mixed freely with design code, does not mean that the language is not capable of doing what bugfinder wants.
to summarize, the following unclocked property:
cindy. |
Cindy,
I respect the vast experience you have with Sugar/PSL and am sure you know far more intricacies of PSL than I do. Having said that, let me clarify what I meant to say:
As hemanth pointed out, current tools (not sure of IBM ones though) disallow properties inside a procedural code, say we have a case statement:
case sel
0 : // some thing
1 : // some thing else
default : assert "Illegal value"
-- Pseudo code, neither Verilog nor VHDL
-- May not be a good example
As far as I understand PSL, a tool may not/atleast need not derive the context - i.e fire this assertion only when sel is not 0 or 1.
Cindy - It will be great if you can confirm this for us.
I don't mind calling it with a different name than "immediate assertion" - if that will help anyone.
Thanks,
Srini
_________________
Srinivasan Venkataramanan
Chief Technology Officer, CVC www.cvcblr.com
A Pragmatic Approach to VMM Adoption
SystemVerilog Assertions Handbook
Using PSL/SUGAR 2nd Edition.
Contributor: The functional verification of electronic systems |
|
| Back to top |
|
|
cindy
Industry Expert
Joined: Aug 17, 2004
Posts: 309
|
| Posted: Tue Dec 07, 2004 4:58 am Post subject: |
|
|
srini,
| Quote: | As hemanth pointed out, current tools (not sure of IBM ones though) disallow properties inside a procedural code, say we have a case statement:
case sel
0 : // some thing
1 : // some thing else
default : assert "Illegal value"
-- Pseudo code, neither Verilog nor VHDL
-- May not be a good example
As far as I understand PSL, a tool may not/atleast need not derive the context - i.e fire this assertion only when sel is not 0 or 1. |
you are correct that psl does not define embedding of assertions inside of executable code like your case statement example. my point was that there are other means of supporting what bugfinder wants, so that the lack of a particular construct does not necessarily answer the question.
i am sorry to be picky about the terminology, but i want to be careful not to confuse between the lack of a construct called "immediate assertion" and the lack of the ability to accomplish what immediate assertions do in another language. the lack of a construct called immediate assertions in psl does not mean that times in between clock ticks are necessarily lost.
cindy. |
|
| Back to top |
|
|
srini
Senior
Joined: Jan 23, 2004
Posts: 430
Location: Bengaluru, India
|
| Posted: Tue Dec 07, 2004 5:36 am Post subject: |
|
|
| cindy wrote: | you are correct that psl does not define embedding of assertions inside of executable code like your case statement example. my point was that there are other means of supporting what bugfinder wants, so that the lack of a particular construct does not necessarily answer the question.
|
So, technically speaking (since you say similar functionality can be achieved) do you think that "VHDL variable" (which is limited to inside a process - leaving out shared var for now) can be used inside a PSL assertion? - Again I don't intend to compare languages, rather am curious to understand - also I don't see much value in using a special assertion language for this purpose (as I mentioned in my reply to the OP).
Thanks,
Srini
_________________
Srinivasan Venkataramanan
Chief Technology Officer, CVC www.cvcblr.com
A Pragmatic Approach to VMM Adoption
SystemVerilog Assertions Handbook
Using PSL/SUGAR 2nd Edition.
Contributor: The functional verification of electronic systems |
|
| Back to top |
|
|
cindy
Industry Expert
Joined: Aug 17, 2004
Posts: 309
|
| Posted: Wed Dec 08, 2004 3:25 am Post subject: |
|
|
srini,
| Quote: | | So, technically speaking (since you say similar functionality can be achieved) do you think that "VHDL variable" (which is limited to inside a process - leaving out shared var for now) can be used inside a PSL assertion? |
as far as the language is concerned, there are two issues:
first, can you write a boolean expression containing a vhdl variable? (i don't know vhdl, but i assume that something like "a>b" would be boolean no matter the type of "a" and "b".)
if the answer to this question is yes, then it is possible to write a psl assertion that refers to a vhdl variable.
second, can your verification tool access the values of the vhdl variables (for instance, to display them in a waveform)?
if the answer to this question is yes, then it is possible to implement support for such a psl assertion in the tool.
cindy. |
|
| Back to top |
|
|
hemanth
Senior
Joined: Aug 16, 2004
Posts: 93
Location: Bangalore
|
| Posted: Wed Dec 08, 2004 4:37 am Post subject: |
|
|
| cindy wrote: |
as far as the language is concerned, there are two issues:
first, can you write a boolean expression containing a vhdl variable? (i don't know vhdl, but i assume that something like "a>b" would be boolean no matter the type of "a" and "b".)
if the answer to this question is yes, then it is possible to write a psl assertion that refers to a vhdl variable.
second, can your verification tool access the values of the vhdl variables (for instance, to display them in a waveform)?
if the answer to this question is yes, then it is possible to implement support for such a psl assertion in the tool.
|
cindy,
Thats where the quirk is; unlike verilog for which variables are variables, in VHDL there is a specific type of object called "variable" which is local to the process in which it is defined (something like a local variable of a function in c) and hence not visible/accessible outside that process (shared variables are an exception, which are visible in all processes). Though as you said all operators can be used on them but only in the specific process where it is declared.
Now, the simulator(Modelsim) dosent allow any psl declaration inside VHDL processes, hence mandating only the use of signals for psl expressions. But signals in vhdl are memory elements and dont have the instantaneous value grabbing quality of Variables, taking only a single value in one complete process execution.
Modelsim dosent display variables in waveform as they are not considered memory elements(it only shows value at the current simulation time) added to that the new modelsim also dosent allow unclocked psl declarations. Looks like the vendors make a hash of things 
-hemanth |
|
| Back to top |
|
|
Ajeetha
Senior
Joined: Mar 29, 2004
Posts: 424
Location: Bengaluru, India
|
| Posted: Wed Dec 08, 2004 6:21 am Post subject: |
|
|
Hi,
| hemanth wrote: |
Modelsim dosent display variables in waveform as they are not considered memory elements
-hemanth |
Slightly unrelated post/clarification (not relevant to assertions):
Modelsim does allow VHDL Variables to be viewed as waveform. Use a TCL command as:
add wave /top/dut/entity_name/process_name/var_name
The catch is you need to specify the process label/name before the variable name. From modelsim doc:
--------
Limitations: VHDL variables and Verilog memories can be added using the variable’s full name only (no wildcards).
------
Regards,
Ajeetha
_________________
Ajeetha Kumari,
CVC Pvt Ltd. http://www.cvcblr.com
* A Pragmatic Approach to VMM Adoption http://www.systemverilog.us/
* SystemVerilog Assertions Handbook
* Using PSL/Sugar |
|
| Back to top |
|
|
hemanth
Senior
Joined: Aug 16, 2004
Posts: 93
Location: Bangalore
|
| Posted: Thu Dec 09, 2004 12:25 am Post subject: |
|
|
ajeetha,
thanks, I am corrected.
hemanth |
|
| 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
