IBM®
Skip to main content
    Israel [change]    Terms of use
 
 
 
    Home    Products    Services & solutions    Support & downloads    My account    
IBM Research

FoCs

Formal Verification


Using PSL/Sugar in VCS Environment


There is an easy way to use PSL/Sugar in the Synopsis VCS environment using FoCs:

  1. Write a PSL/Sugar file:
    vunit r1 {     
    	assert {[*];  !aa;  bb(1)} (0) ; 
    }
    You may copy the file from here.

  2. Generate the Verilog checker from the PSL/ Sugar file using FoCs (file checker.v).
    The following FoCs settings are chosen in the generation:
    • Generate Module - YES
    • Produce Instantiation Code - YES
    • Checker Module Name - Use Vunit Name
    • Create Enable Signals - per assertion only
    • Automatic Vacuity Check - NO

  3. Write an input behavior file for the Verilog file. Here is an example of such a file: r1.v.

  4. Next, use VCS to build an executable model of the checker. To do this with the files used in this example, issue the following command:
    >vcs r1.v checker.v
    You should next see some messages from VCS, informing you that the files r1.v and checker.v were parsed and that the generation of the model has been successfully completed.

  5. Now the model has been built and the next step is to execute it to find out if the tests written in the testbench pass or fail.
    Type:
    > simv
    You should now see more messages, informing you about the progress of the simulation. In this example, the following message is issued, informing that the test failed after cycle 1.


 
 

    About IBMPrivacyContact