Page 2 of 2 FirstFirst 12
Results 11 to 16 of 16

Thread: How to use Shared Variable

  1. #11
    Tricky is offline Moderator **Forum Master**
    Join Date
    Oct 2008
    Posts
    5,701
    Rep Power
    1

    Default Re: How to use Shared Variable

    In what context are you looking at?
    There is NO REASON to use a shared variable in synthesis code - other than for a write-before read ram inference
    There are loads of reasons to use them in testbenches.

    What are you trying to do?

  2. #12
    Join Date
    Mar 2011
    Posts
    13
    Rep Power
    1

    Default Re: 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.
    Last edited by designer123; October 3rd, 2017 at 10:38 AM.

  3. #13
    Tricky is offline Moderator **Forum Master**
    Join Date
    Oct 2008
    Posts
    5,701
    Rep Power
    1

    Default Re: How to use Shared Variable

    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

  4. #14
    Join Date
    Mar 2011
    Posts
    13
    Rep Power
    1

    Default Re: How to use Shared Variable

    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.

  5. #15
    Tricky is offline Moderator **Forum Master**
    Join Date
    Oct 2008
    Posts
    5,701
    Rep Power
    1

    Default Re: How to use Shared Variable

    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).

  6. #16
    Join Date
    Mar 2011
    Posts
    13
    Rep Power
    1

    Default Re: How to use Shared Variable

    I said VHDL2008 because of the PSL

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

Similar Threads

  1. Replies: 2
    Last Post: October 22nd, 2016, 11:52 AM
  2. Replies: 9
    Last Post: April 15th, 2014, 11:07 AM
  3. Replies: 1
    Last Post: March 17th, 2013, 03:07 AM
  4. How to define a variable and assign a variable
    By tesleft in forum General Altera Discussion
    Replies: 4
    Last Post: February 16th, 2013, 05:49 PM
  5. Replies: 0
    Last Post: July 21st, 2010, 01:54 AM

Bookmarks

Posting Permissions

  • You may not post new threads
  • You may not post replies
  • You may not post attachments
  • You may not edit your posts
  •