| 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, 40 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 |
kirloy
Senior
Joined: Sep 20, 2004
Posts: 174
|
 Posted: Wed Oct 20, 2004 9:47 am Post subject: OR-ing sequences in PSL |
 |
|
I want to assert such property:
in english: assert
There should hold at least one of sequences: {a;b}, {c;d}
in PSL:
as1:assert: always{a;b} | always{c;d};
or maybe
as1:assert: always(always{a;b} | always{c;d});
is it possible with PSL??? |
|
| Back to top |
|
 |
cindy
Industry Expert
Joined: Aug 17, 2004
Posts: 309
|
| Posted: Wed Oct 20, 2004 9:59 am Post subject: |
|
|
kirloy,
from the english, it is not clear what you want to assert, therefore it is hard for me to say what the psl is.
your first example:
| Code: | | as1:assert: always{a;b} | always{c;d}; |
says that either the lhs holds, or the rhs does. the lhs says that a holds at every cycle, and b holds in all cycles but the first (do you see why?). the rhs says that c holds in every cycle, and d holds in all cycles but the first. is this what you meant?
in your second example, the extra always is redundant.
cindy. |
|
| Back to top |
|
|
srini
Senior
Joined: Jan 23, 2004
Posts: 430
Location: Bengaluru, India
|
| Posted: Wed Oct 20, 2004 1:25 pm Post subject: |
|
|
| kirloy wrote: | I want to assert such property:
in english: assert
There should hold at least one of sequences: {a;b}, {c;d}
in PSL:
as1:assert: always{a;b} | always{c;d};
or maybe
as1:assert: always(always{a;b} | always{c;d});
is it possible with PSL??? |
Hi,
Try looking for "Sequence composition" operators in LRM/our book, there is a Sequence - OR ing that matches your requirement (or atleast what I understand as your requirement).
Good Luck
Srinivasan
_________________
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 |
|
|
kirloy
Senior
Joined: Sep 20, 2004
Posts: 174
|
| Posted: Thu Oct 21, 2004 1:36 am Post subject: |
|
|
My mistake. I should ask about property ORing.
I know how works sequence OR.
So in english it should be:
There should hold at least one of properties : always{a;b}, always{c;d} during the simulation
Cindy:
| Quote: | the lhs says that a holds at every cycle, and b holds in all cycles but the first (do you see why?). the rhs says that c holds in every cycle, and d holds in all cycles but the first. is this what you meant?
|
Yes I see. This sequences are only for example.
The problem is about ORin properties. How Properties are treated in such expresion(I don't know if you see the problem). May such expresion be used in simulation (or only in Formal Verification).
2.
This 2 assertion are equevalent?
as1:assert: always{a;b} | always{c;d};
as1:assert: always{{a;b} |{c;d}};
I think that it isnt the same. Becouse 2nd assertion starts from all clocks, while 1st describe different behaviour - just check if at least one of component properties holds during all simulation time. So when should be reported failure of this property, at the and of simulation? When 2nd of component property fails??? |
|
| Back to top |
|
|
hemanth
Senior
Joined: Aug 16, 2004
Posts: 93
Location: Bangalore
|
| Posted: Thu Oct 21, 2004 2:50 am Post subject: |
|
|
| I think as1 is one you should be looking for as it describes what you want. on the other hand as2 contrains at least one of them to be true all the time so it fails if at least one dosent occur every time. |
|
| Back to top |
|
|
cindy
Industry Expert
Joined: Aug 17, 2004
Posts: 309
|
| Posted: Thu Oct 21, 2004 7:03 am Post subject: |
|
|
kirloy,
| Quote: | Yes I see. This sequences are only for example.
The problem is about ORin properties. How Properties are treated in such expresion(I don't know if you see the problem). May such expresion be used in simulation (or only in Formal Verification). |
i'm not sure i see the problem, but i'll try to answer. it is possible to put logical operators (and, or , not etc.) between properties. see lrm 1.1 section 6.2.1.7 (logical fl properties).
regarding using such a property in simulation, there are two answers:
answer a: in theory, any psl foundation language property can be checked in simulation.
answer b: many tools support only the simple subset (see lrm 1.1 section 4.4.4) for simulation. the simple subset supports logical operators between properties, but one of them must be a boolean. for example:
is such a property.
i should note that in my 10 years' experience with psl and its precursor, sugar, i have never seen a practical example of a foundation language property that could not be expressed with the simple subset. therefore, if you are struggling with an actual property (rather than just these toy examples we have been discussing) please consider posting it here in english, so that we can explore how to express it in psl.
| Quote: | This 2 assertion are equevalent?
as1:assert: always{a;b} | always{c;d};
as1:assert: always{{a;b} |{c;d}};
I think that it isnt the same. Becouse 2nd assertion starts from all clocks, while 1st describe different behaviour - just check if at least one of component properties holds during all simulation time. So when should be reported failure of this property, at the and of simulation? When 2nd of component property fails??? |
the two are not the same, but i am not sure that i follow your reasoning as to why not. so just to clarify:
the first says that "either always {a;b} happens or always {c;d} happens", where "always" refers to every single cycle.
the second says that "always, either {a;b} happens or {c;d} happens", where again, "always" refers to every single cycle.
therefore, the difference doesn't stem from the need to check during all simulation time, as you say, but rather from what is checked during all simulation time.
as to when the property fails:
in the first case, the left-hand-side of the "or" operator is "always {a;b}" and the right-hand-side is "always {c;d}". suppose that both sides hold up to time 50, and then at time 50 the left-hand-side fails while the right-hand-side holds. then, both sides hold up until time 75, at which time the right-hand-side does not hold, while the left-hand-side does. you can now report a failure of the whole property, because it requires that either the left-hand-side holds at all times, or the right-hand-side does. and at time 75 you can say for sure that this is not so.
in the second case, the left-hand-side is "{a;b}" and the right-hand-side is "{c;d}". looking at the same temporal behavior of these new left- and right-hand-sides as above, we have that you cannot yet report a failure at time 75. that is because the second case requires that at each time step, at least one of the left- or right-hand-sides holds. and up to time 75, at least one of them does. in order to report a failure, you would have to find a cycle where both the left- and right-hand-sides do not hold.
i hope this helps.
cindy. |
|
| 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
