Verilog model of PSL

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

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.

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

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.

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