Verilog model of PSL > Forums

Forums

Subject: Verilog model of PSL

Posting to forums is available to community members only.
Login or Register

Rate this topic:

Author

Messages

weberrm
Posts: 0
Online: User is Offline

10/17/2006 3:32 PM
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!

cbeaureg
Posts: 3
Online: User is Offline

10/19/2006 8:50 AM
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

weberrm
Posts: 0
Online: User is Offline

10/19/2006 9:00 AM
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));

ckomar
Posts: 0
Online: User is Offline

10/19/2006 9:11 AM
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

weberrm
Posts: 0
Online: User is Offline

10/19/2006 9:24 AM
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));

ckomar
Posts: 0
Online: User is Offline

10/19/2006 10:51 AM
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

Posting to forums is available to community members only.
Login or Register