P2VSIM: A SIMULATION AND VISUALIZATION TOOL FOR THE P2V COMPILER

• Main Author: Almeida, Oscar
• Other Authors: Liu, Jyh-Charn
• Format: Others
• Language: English
• Published: 2010
• Subjects: PSL; P2V; assertion-based verification; GUI
• Online Access: http://hdl.handle.net/1969.1/ETD-TAMU-2009-05-606

The Property Specification Language (PSL) is an IEEE standard which allows developers to specify precise behavioral properties of hardware designs. PSL assertions can be embedded within code written in hardware description languages (HDL) such as Verilog to monitor signals of interest. Debugging simulations at the register transfer level (RTL) is often required to verify the functionality of a design before synthesis. Traditional methods of RTL debugging can help locate failures, but do not necessarily immediately help in discovering the reasons for the failures. The P2VSim tool presents the ability to combine multiple Verilog signals not only instantaneously, but also across multiple clock cycles, producing a graphical display of the state of active PSL assertions in a given RTL simulation. When using the P2VSim tool, users will write PSL assertions directly into their Verilog source files. After the tool searches for and loads the embedded assertions, execution trace monitors for the relevant Verilog signals are dynamically generated and written back into the Verilog source code. P2VSim then invokes an RTL simulator, Modelsim, to generate a simulation execution trace, requiring that the designer has some hardware or software testbench already in place. Next, the input PSL assertions are parsed into time intervals that have logical and temporal properties. These intervals are to be displayed graphically when PSL property checking is performed. Finally, the user is allowed to step through simulation one cycle at a time, while the tool applies the simulation execution trace to the instantiated time intervals, performing PSL property checking at each clock cycle. From this, the user can witness the exact clock cycles when PSL assertions are satisfied or violated, along with the causes of such results.