How to simulate a design with a psl file using Modelsim?

[Laverne]

modelsim vunit file

Hi all,

Can some please verify if this is true...
For simulation, instead of writing a regular testbench you would write a psl file for your design and use Modelsim to simulate.
I am very new to this vhdl stuff and have been doing lots of reading but still confuse

If it is true then please provide a simple design with psl so that I can follow through it.

Thanks in advance

regards

 

[lordsathish]

Re: PSL file-Modelsim

Hey i am not sure of the .psl file...but you can definitely use the .do file to simulate your verilog or vhdl file... the .do files are macros... you must have used the command window in modelsim to force inputs... you have to use the same commands to write that .do file and can simulate it....

 

[Laverne]

Re: PSL file-Modelsim

Thanks for your input.
Anyone else have any suggestion?

Regards

 

[vinodkumar]

Re: PSL file-Modelsim

hi not known about PSL file,but iam also using .do file.

 

[walid farid]

Re: PSL file-Modelsim

Hi,
What i know is that you can use TCL or DO files ; and i think that PSL files stands for Property Specific Language.
PSL is designed to be used by both formal (mathematical proof) and dynamic (simulation based) methods of checking.

 

[salma ali bakr]

Re: PSL file-Modelsim

you can have PSL properties directly within your RTL code...or you can have vunits (verification units) in separate files with all the properties gathered up...and these vunits are bound to the design files

 

[Laverne]

Re: PSL file-Modelsim

thank you all for the response. your effort in trying to help is very much appreciated.

what i am looking for is an example of a simple design plus external psl file (verification unit file) that i can follow through using modelsim.
so basically...two files.
1. design.vhd
2. design_tb.psl

Xmas to all.

regards
Laverne

 

[walid farid]

Re: PSL file-Modelsim

Hi,
There are some examples with ModelSim, they are some how big designs .. if you want them i can upload them.

 

[salma ali bakr]

Re: PSL file-Modelsim

see this book please...

Using PSL/Sugar for Formal and Dynamic Verification
2nd Edition
Guide to Property Specification Language for Assertion-Based Verification

I'm not sure if it's here on the forum...I had it as paperback...it's got great examples for what you want...

 

[Laverne]

Re: PSL file-Modelsim

walid,
if you can please upload them. do you have a step by step process of how to simulate a design with a psl file using Modelsim? the simplest the better as i am very new to this vhdl stuff.

salma ali bakr,
thanks for the heads up.

Added after 3 minutes:

this is what i found during my search. the link below has both a design and psl file.
basically i copy/paste both design and psl file and simulate with modelsim but somehow i never see the assertion part/value in modelsim.
what am i missing?

http://www.cs.chalmers.se/Cs/Grundutb/Kurser/svh/Tools/jaspergold/

 

[salma ali bakr]

Re: PSL file-Modelsim

you have to add the assertions to your wave...
you'll find them under your design unit..
and you'll just right click and add them to the wave
they should give you passed or failed...etc

 

[walid farid]

Re: PSL file-Modelsim

Here it is , but it is some how BIG.
The Instructions are in a file "doit.sh", so if you have linux or Cygwin on windows just use "doit.sh demo" ... otherwise just open the file and u can find the ModleSim Instructions.
Its one of the ModelSim examples so you can find it on Modeltec..../examples/psl/vhdl/

 

[Laverne]

Re: PSL file-Modelsim

i got it working with psl using modelsim.
but now i got another problem. when i run the simulation i got nothing but red and blue lines in the wave window. this only happens when using psl. with a regular testbench there is a timing diagram. need to work on this.

again, thanks to all for all the help

regards

 

[walid farid]

Re: PSL file-Modelsim

Hi,

*Why don't you list the ModelSim commands you are using and upload the design?
*What ModelSim version, are you using ?

 

[Laverne]

Re: PSL file-Modelsim

hi,

i have attached 2 files.
one is a design and the other is psl file.

please keep in mind that i am not after the design itself as can be seen from the file.
what i am after is how to simulate the design with a psl file as oppose to the a regular testbench. so therefore...the file is just some very basic stuff.

i am not sure this is the way to do it. it is my first attempt at trying psl and also some what new to vhdl.

modelsim version is 6.2c Se

regards

 

[salma ali bakr]

Re: PSL file-Modelsim

i saw both files
they should work properly

so you simulated the psl file
and what happened...? something wrong with the waves..?

i've worked with psl before but never tried to do separate files for the properties
it's always better to embed them in your code, it'll be easier this way to follow up with them...or put them in the test bench...no need to use the vunit even...but it's always good practice to test the untested

 

[walid farid]

Re: PSL file-Modelsim

Here is what i done ......

use these commands:
vcom DFF_CLEAR.vhd -pslfile DFF_CLEAR_TB.psl
vsim dff_clear -assertdebug
view assertions

Then try to force the signals using the ModelSim GUI .... instead of a testBench
and here is the view i got.

 

[salma ali bakr]

Re: PSL file-Modelsim

ya walid ya gamed
walahee enta 7'osara fel balad di

good job man
keep up the support :arrow:

i didn't know about the -pslfile thing
cause i had them always embedded in the design or the testbench
thanks for clearing that up

 

[walid farid]

Re: PSL file-Modelsim

Ba3d ma 3endakom ya Salma
and you are WELCOME

 

[Laverne]

Re: PSL file-Modelsim

hi,

i follow those commands and did not get the same result.
mine still shows red and blue lines.

can you clarify what you meant by:
force the signals using the Modelsim GUI...instead of a testbench.

here is how i do mine. maybe i am missing a step somewhere.
1. create a directory
2. save two files to the above directory; design and psl
3. run modelsim, create project/work directory and point to number 1 above.
4. load two files into modelsim
5. compile the design file
6. add all signals to the wave window
7. run those commands
8. press the run button(as shown from the screenshot)

thanks