How to use Shared Variable

SHARED VARIABLES can help you to solve really difficult PSL Assertion problems.

Say you need a Signal or a Sequence Seq1 to Occur Twice in an antecedent & the SECOND Occurrence MUST then be followed by another Sequence Seq2.

THEN

You DO NOT WANT Another thread to start <<<<<<<<<<<

UNTIL

After the SECOND Occurrence of Seq1 & then the Occurrence of Seq2.

System Verilog's First Match

OR

PSL's goto repetition ie. [->]

Will NOT STOP the UNWANTED thread starting on the SECOND Concurrence of Seq1.

Unwanted threads can be avoided.

HOW?

Create a shared variable that has the following functions (methods).

type PSL_BOOL_PType is PROTECTED

impure function get( Get_Enable : BOOLEAN ) return BOOLEAN;

impure function clr( Clr_Enable : BOOLEAN ) return BOOLEAN;

impure function set( Set_Enable : BOOLEAN ) return BOOLEAN;

end PROTECTED PSL_BOOL_PType;

These all Return the State of the BOOLEAN variable inside the PROTECTED BODY

BEFORE

the function was called.

I'll leave you to write the PROTECTED BODY.

Declare Your_Shar_Var

shared variable Your_Shar_Var : PSL_BOOL_PType;

You can then use Your_Shar_Var to DISABLE the triggering of new threads for your assertion by using

Your_Shar_Var.clr(rose(Last))

in the antecedent

Where

Last is the Last signal to rise in Seq1.

You then need another property that includes:-

{rose(Last):ended(Seq1)} |->

{

Seq2 : (Your_Shar_Var.set(TRUE) or TRUE) -- ORDER of eval Means Your_Shar_Var.set MUST Come 1st

}

This not only checks for Seq2

but ALSO

Re-enables the triggering of new threads.

************

* IMPORTANT

************

PSL has LEFT to Right ORDER of evaluation

SO

This Means these Functions (Methods) MUST

Sometimes Come FIRST ie. on the LEFT of an EXPRESSION

OTHERWISE, they May NOT GET CALLED.

There is a neater way of

doing

Seq2 : (Your_Shar_Var.set(TRUE) or TRUE)

but

it it requires another function.

There really should have been a simple built in way of doing this in PSL & SVA

BUT

As I said above

First Match OR goto repetition [->] WILL NOT DO IT.

..............................................................

PSL was developed from IBM Sugar

SVA syntax is almost the same as PSL

BUT

JUST TO BE DIFFERENT & INCOMPATIBLE

They changed a few things like putting the Clock at the beginning of a property & stuff like# #1

THERE WAS NO EXCUSE FOR THIS.

UNFORTUNATELY

All 3 Languages use the most APPALLINGLY BAD CRYPTIC SYNTAX

BUT

We are stuck with it.

Have you tried this type of Assertion aux code with a formal analysis tool? Does it work?

I have used JasperGold breifly and the general consesus was to simplify assertertions as much as possible, and remove all aux code out of the assertions. The simpler the assertion (ie. no functions etc) the faster it will complete.

Ideally you want

a -> b

Tricky,

I have not had the Luxury of trying it on a Formal Verification Tool.

It simulates just fine.

In other cases, this kind of technique certainly SPEEDS UP simulation by avoiding REDUNDANT THREADS in badly written very INEFFICIENT PROPERTIES when someone has dumped them on me & I don't have time to fix them.

BUT

in those cases I don't leave the aux code in the files, I just use it to investigate the problems.

People who write INEFFICIENT PROPERTIES just don't care about how long we have to wait. Their attitude is that their properties do check & it is someone else's problem if the project is delayed.

I would be very interested to know if JasperGold or VC Formal etc. can handle PSL_BOOL_PType properly.

If there is anyone out there reading this & with access to Formal Verification Tools then please TRY IT OUT & let us all know.

In THEORY, if those tools implement VHDL2008 PROPERLY then all should be well.

Tricky, maybe you could try it with JasperGold.

PSL_BOOL_PType is a very simple Protected Type & once created it can be used over & over again without much effort.

Using aux code feels like a bit of a Kludge but we have to live in the real world.

I could say the same thing about PSL & SVA. (Double Kludge)

ANYWAY

For the situation described in my previous post we really SHOULD NOT have to do this.

There SHOULD have been a simple BUILT IN way of doing this in PSL & SVA

BECAUSE

As I said before

First Match OR goto repetition [->] WILL NOT DO IT.

I no longer have access to JG - it was temporary.

Protected types are VHDL 2002, not 2008. So should work with JG.

From my JG training - AUX code is a necessity. But anything that prevents separate threads being needed is what you have to do for formal. JG doesnt really support anything clever in asserts - otherwise the prove time just explodes. Aux code also increases the State space, so making it non-synthesisable probably wont really work with JG. All AUX code I have seen for JG was basically synthesisable verilog (Ive only worked with SVA).

I said VHDL2008 because of the PSL

I doubt that old tools that had to have PSL in comments would work.

Tricky ask what I try to do?

I learn

Thank Designer123

Good info

I try it and it work

--- Quote Start ---

Tricky ask what I try to do?

I learn

--- Quote End ---

Like I said in post.

For synthesis, they're pretty useless.

So unless you explain why you want one, it's difficult to help..

Tricky

I not want one

I learn all part of VHDL

I want job in new team