PSL- "How do I..."

romi · Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota

Is this forum the proper place to ask "How do I..." PSL questions? If not, where is a good place to do that? Thanks.

Janick · Posted: Thu Mar 11, 2004 9:18 pm **Post subject: Re: PSL- "How do I..."**

romi · Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota

Great!

I was wondering how a coverage assertion could be written in PSL to show that a signal, or expression, or even a sequence has toggled N number of times.

For instance, how would I write an assertion that fires when the result of the expression (A & ~B) went from 0->1, 100 times.

Thanks in advance.

Matilda · Newbie Joined: Jan 15, 2004 Posts: 3

One way to write

bdeadman · Posted: Mon Mar 15, 2004 9:21 am **Post subject:**

One of the attractions of Sugar (sorry, PSL...) is there are many ways to express the same thing, for example the expression can also be written as:

{ !(a&!b)[*] ; (a&!b) }[*100]

Incidentally, note that { rose(a&!b) }[*100] almost certainly won't work because you cannot have the same change in sucessive cycles, therefore Matilda used the [=100] non-sucesive repeat.

Regards

Bernard

romi · Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota

How about this one?

Property that says never 2 or more As before B. Another way of putting it is that if there is an A there should eventually be a B before another A.

Thanks.

romi · Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota

On a related note, how about this one?

The sequence must always be A then eventaully B then eventually C. Also, there can never be a B unless there was an A and there can never be a C unless there was a B. And A cannot repeat before B or C, B cannot repeat before C or A, and C cannot repeat before A again or B again.

This could be thought of as a control for a data buffer. A says allocate the buffer, B says data is available in the buffer, and C deallocates the buffer. We don't want things to happen like 2 allocates (As) or 2 availables (Bs) or a deallocate (C) before it is allocated and available.

If I can get an answer this one, I don't need the other one.

Thanks.

bdeadman · Posted: Sat May 08, 2004 10:58 am **Post subject:**

Quickly, and without thinking a lot, one way to write this is as three seperate requirements:

always { a } |=> { !c[*] ; b } !

always { b } |=> { !a[*] ; c } !

always { c } |=> { !b[*] ; a }

This says:

a must be followed by b without any c's, and there must eventually be a b

b must be followed by c without any a's, and there must eventually be a c

c must be followed by a without any b's, but there don't have to be any a's - you need this to make sure you don't get an error at the end of simulation

There are a few cases I haven't taken care of here, for example can a and b, or b and c or c and a happen simultaneously, but I'm sure you can expand the idea.

No doubt others will correct me if I screwed this up!

Hope this helps,

Bernard

vhdlcohen · Posted: Sat May 08, 2004 3:48 pm **Post subject:**

romi · Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota

Thanks for your help.

bdeadman, I think yours allows a to repeat again before b.

In addition to your three, I think these other 3 are also needed.

always { a } |=> { ~a[*];b }

always { b } |=> { ~b[*];c }

always { c } |=> { ~c[*];a }

Also, I added some to say neither a, b, or c can happen at the same time.

vhdlcohen, thanks for your help too. I have your "Using PSL/Sugar with Verilog and VHDL" book. This other book you mention must talk about using PSL for Formal verification in particular more closely. That is what I am using these properties for, to contrain my inputs in order to formally verify some checks within the module.

I was hoping someone would have a very concise way of reprenting these three signals that control the buffer, however, that doesn't seem to be the case. Looks like it will probably take at least a few properties (or sub-properties) to describe this seemingly simple interface.

This example was for just 1 buffer location, what if there are 32 locations and all the signals are vectors a[31:0], b[31:0], and c[31:0] doing the same thing. Does all this need to be repeated 31 times. Seems very cumbersome. I know the tool I'm using says it doesn't support parameterized properties for it's "formal" checker.

Although, what I'll end up with is a very well defined interface that nothing illegal will be able to penetrate! However, at what cost? Originally, I just had a couple properites within the module looking for a deallocate (c from above) when the buffer was inactive (internal state) or looking for an allocate (a) when the buffer was active (same internal state). It's taking many more properites to constrain the inputs than to do the internal checks. It also ends up making the internal checks useless because the ones on the interface will always catch the problem first. Is this how the process is supposed to work. Maybe so...

vhdlcohen · Posted: Sat May 08, 2004 9:06 pm **Post subject:**

How about the following:
always { a } |=> { (!a && !c)[*] ; b } !

always { b } |=> { (!b && !a)[*] ; c } !

always { c } |=> { (!c && !b)[*] ; a }

An alternate solution:
always a -> next (!a && !c)[*] until! b;
always b -> next (!b && !a)[*] until! c;
always c -> next (!c && !b)[*] until! a;

If "a" is a vector, and the tool supports the forall, then you can do:
reg [31:] a, b, c; // assumption on size of variables

property AbeforeBbeforeC =
forall m in {31:0} :
always a -> next (!a[m] && !c[m])[*] until! b[m];
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

vhdlcohen · Posted: Sat May 08, 2004 9:08 pm **Post subject:**

romi · Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota

Thanks again.

A couple more things.

Is this a good way to say that the signals can't be at the same time?

never ((a & b) | (b & c) | (c & a));

A separate issue...

I need to say that the the signals only rise and fall on a particular edge of a clock. How does the below look? What about the "@ *"? I needed tell it to always check instead of just at the default clock.

always (rose(a) | fell(a) -> rose(clk)) @ *;

vhdlcohen · Posted: Sat May 08, 2004 10:28 pm **Post subject:**

romi · Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota