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.