Stats

  • Locked Locked
  • Replies 5
  • Subscribers 64
  • Views 14377
  • Members are here 0
This discussion has been locked.
You can no longer post new replies to this discussion. If you have a question you can start a new discussion

Verilog model of PSL

archive

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
Parents

  • 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
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
Children
No Data

Community Guidelines

The Cadence Design Communities support Cadence users and technologists interacting to exchange ideas, news, technical information, and best practices to solve problems and get the most from Cadence technology. The community is open to everyone, and to provide the most value, we require participants to follow our Community Guidelines that facilitate a quality exchange of ideas and information. By accessing, contributing, using or downloading any materials from the site, you agree to be bound by the full Community Guidelines.