Home > Community > Forums > Functional Verification > Verilog model of PSL

Email

* Required Fields

Recipients email * (separate multiple addresses with commas)

Your name *

Your email *

Message *

Contact Us

* Required Fields
First Name *

Last Name *

Email *

Company / Institution *

Comments: *

 Verilog model of PSL 

Last post Tue, Oct 17 2006 3:32 PM by archive. 5 replies.
Started by archive 17 Oct 2006 03:32 PM. Topic has 5 replies and 1579 views
Page 1 of 1 (6 items)
Sort Posts:
  • Tue, Oct 17 2006 3:32 PM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    Verilog model of PSL Reply

    I would like to know if there is a way to create a verilog model, with verilog that IFV can understand, of the following PSL (din_old is driven by the PSL assumption):
     
    reg [W-1:0] din_old;
    //psl assume_din_old: assume always (din_old==prev(async_din));
     
    Take special note that this property is unclocked.
     
     
    Below is how I do it for simulation, but IFV doesn't understand this non-synthesizable code.
     
    reg [W-1:0] din_follower,din_old;
    always @* begin
      if(async_din!=din_follower) begin
        din_old = din_follower;
      end
      din_follower = async_din;
    end

    Any ideas?

    Thanks!


    Originally posted in cdnusers.org by weberrm
    • Post Points: 0
  • Thu, Oct 19 2006 8:50 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: Verilog model of PSL Reply

    IFV reduces your code to be:

    din_follower = async_din;

    I'm not sure how your verilog code behaves in simulation
    but they is a potential race condition between the if(async!=din_follower)
    and din_follower = async_din. So I'm not sure what value will have din_old.
    One solution could be to wrap your verilog using 'ifdef to use it in simulation
    and use only the assume property in IFV. Hope this can help.

    -claude


    Originally posted in cdnusers.org by cbeaureg
    • Post Points: 0
  • Thu, Oct 19 2006 9:00 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: Verilog model of PSL Reply

    I don't see a race.  A change in async_din starts the sequence.  Since async_din changed it will not equal din_follower, din_old is updated to din_follower and din_follower is updated to async_din.  The block executes again because din_follower updated, but since now async_din equals din_follower, there are no updates.

    My question is what verilog is equivalent to the below PSL, but I'd like to know how you see a race too.  Thanks.

    reg [W-1:0] din_old;
    //psl assume_din_old: assume always (din_old==prev(async_din));







    Originally posted in cdnusers.org by weberrm
    • Post Points: 0
  • Thu, Oct 19 2006 9:11 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: Verilog model of PSL Reply

    Hi!
     
     I wrote a response yesterday to this but apparently it got lost somewhere.  My first observation was that the code you have was synthesizable by IFV.  It synthesizes to a latch which is non-ideal but nonetheless, it does synthesize.  Second, I had some questions as to how simlution and formal will model the property.

    In the simulation world, the property you have is evaluated any time din_old or async_din changes (ie event based). In the formal world, this property will be evaluated at every engine crank. An engine crank is typically both edges of your fastest clock. In this way, what you have in formal and what you have in simulation are not the same.

    So I have a couple of questions
    Are you concerned about consistency between formal and simulation?
    Are you trying to duplicate the formal behavior in simulation?  That is, only evaluate at the same engine cranks?

    Regards,
    Chris



    Originally posted in cdnusers.org by ckomar
    • Post Points: 0
  • Thu, Oct 19 2006 9:24 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: Verilog model of PSL Reply

    I am using the property in formal and the verilog in simulation.  I would like to use just one model for both formal and simulation.  Therefore, it has to be verilog since PSL cannot currently drive things in simulation.

    I am trying to duplicate the formal behavior of the PSL below with verilog.

    reg [W-1:0] din_old;
    //psl assume_din_old: assume always (din_old==prev(async_din));



    Originally posted in cdnusers.org by weberrm
    • Post Points: 0
  • Thu, Oct 19 2006 10:51 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: Verilog model of PSL Reply

    Perhaps the following would work?

    `ifdef SIMULATION

    reg [W-1:0] din_old;
    always @(posedge fast_clock or negedge fast_clock)
    begin
    din_old <= async_din;
    end

    `else

    // psl assume_din_old : assume always (din_old == prev (async_din));

    `endif

    Regards,
    Chris


    Originally posted in cdnusers.org by ckomar
    • Post Points: 0
Page 1 of 1 (6 items)
Sort Posts:
Started by archive at 17 Oct 2006 03:32 PM. Topic has 5 replies.