Stats

  • Locked Locked
  • Replies 6
  • Subscribers 65
  • Views 15350
  • 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

initial statement issue in IFV

DouglasYaya

Dear Sir/Lady:

I have a question while using IFV, there is a simulation model in my design, after running the verification flow for several cycles, I did not find PRINET was set to  1b'1, this seems to be the issue related with initial statement, I do not know how to slove, could you help me? Thank you!

  =========================Command Line=========================

 iev +64bit *.sv +tcl+sim.tcl +covoverwrite +coverage+all

 =========================simulation model=========================

 module PRI(PRI);
  input PRI;
parameter RST_PULSE = 1;

reg PRINET;

initial
begin
 PRINET = 1'b0;
 #RST_PULSE
 PRINET = 1'b1;
end

endmodule

=========================TCL script file=========================

clock -add  ck  -initial 1  -width 1  -period 2 


force   sp  1'b1
force   cd  1'b0
force   d   1'b1

run 6

init -load -sst2 douglas.shm

init -show

constraint -add -pin sp 1'b1

constraint -add -pin cd 1'b0

constraint -add -pin d  1'b1

assert -add -block

assert -add -fsm

define constraint_trace on

define witness_check trace

prove

 

Parents

  • One applies the formal tool to the DUT itself. There should be no testbench involved. IFV applies all possible stimulus to the design (subject to the constraints), so no testbench should be involved. 

     

    If IFV finds that parts of the design itself are not synthesizable, it will complain loudly and "black-box" them. That means it will drop them from the analysis and make no assumptions about their outputs. 

     

    If you want to analyze a block that communicates to a memory or across a particular protocol, then things get more complex. You don't necessarily need a fully synthesizable model of the connected block. But you do need some kind of IP that will model that memory or protocol for the formal tool. Some vendors can sell you a set of assertions that define a properly behaving AHB interface, for example. If you apply those assertions to the port on the DUT, then you don't need an actual simulation model. Others may provide a light-weight synthesizable model of the slave that doesn't do anything more than respond correctly to the master. The same applies to a memory.

Reply

  • One applies the formal tool to the DUT itself. There should be no testbench involved. IFV applies all possible stimulus to the design (subject to the constraints), so no testbench should be involved. 

     

    If IFV finds that parts of the design itself are not synthesizable, it will complain loudly and "black-box" them. That means it will drop them from the analysis and make no assumptions about their outputs. 

     

    If you want to analyze a block that communicates to a memory or across a particular protocol, then things get more complex. You don't necessarily need a fully synthesizable model of the connected block. But you do need some kind of IP that will model that memory or protocol for the formal tool. Some vendors can sell you a set of assertions that define a properly behaving AHB interface, for example. If you apply those assertions to the port on the DUT, then you don't need an actual simulation model. Others may provide a light-weight synthesizable model of the slave that doesn't do anything more than respond correctly to the master. The same applies to a memory.

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.