Dynamic Property Checking - Worked Examples
The various files necessary to run this case study can be obtained from the TransEDA web site at: www.transeda.com/vmm/ If you encounter any problems in obtaining these files please contact TransEDA at the e-mail address: firstname.lastname@example.org
Directory and File Structure
Create a directory (e.g. my-pc) on your system and then unpack the complete set of files that you obtained in the above step into that area. Make sure the directory contains the following files and that the filenames and suffix are correct.
blackjack.v // Blackjack card game design
blackjack_tb.v // This is the test bench
doit.pc.bat // Command line batch file
vnavigator.par // Parameter file
pc_collection.spec // Specifications file
pc_blackjack_library // Library of properties
legal // Wanted properties
prohibited // Prohibited properties
vnavigator_results // Results directory
explain.txt // Explanation of the design
Command Line Batch File
A command line batch file (called doit.pc.bat) is supplied which can be used to automate the process of analyzing and instrumenting the Verilog source files, running the simulation and collecting the activity-data for the results file.
To assist you in understanding how the results file is produced, each line of the batch file is explained below.
1. vnlib -verilog -delete my-work
2. vnlib -verilog -create my-work=./my-work
3. vnlib -verilog -setwork my-work
4. vnpcvalidate -spec pc_collection.spec
5. vnvlog -property -- blackjack.v blackjack_tb.v
6. vnsim -pc -- blackjack_tb
7. vnpcmatch -spec pc_collection.spec
8. vnresults -pc -spec pc_collection.spec
Lines 1 to 3 create a new library to hold the design files that will be analyzed and instrumented. Line 4 checks that the property specifications are syntaxtically correct while line 5 instruments the two design files with the property attribute to collect dynamic property coverage. Line 6 specifies the name of the test bench or top-level module (e.g. blackjack_tb) and runs a normal Verilog simulation to collect the coverage-data for the complete design. This information is written to a results file that has a default name of vnavigator.index. Line 7 performs a match between the tabular trace file (i.e. simulation results) and the properties for the design.
Line 8 is a post-processing stage that creates a set of text files from the simulation results that were matched in line 7. Two text files are produced by this step.
The first text file (called spec_legal.txt)gives a detailed list of the legal or wanted properties and how many times each property was encountered. Any properties that were not encountered will be flagged as an error.
The second text file (called spec_prohibited.txt) gives a detailed list of the unwanted or prohibited properties. None of these properties should have been encountered and should therefore have a count of zero. Any properties that have a count value of one or more are flagged as an error.
Description of the Design
The design is based on modelling the behavior of the dealer in a game of Blackjack (also know as Pontoon or 21). The dealer must follow the rules of the casino: to hold on hands of 17 or more and draw another card on hands of 16 or less. If the value of the hand is greater than 21 the dealer has gone bust. Aces in the game are worth 11 or 1, picture cards (Jack, Queen or King) are worth 10. The maximum number of cards in any hand is 5.
Collecting Coverage Results
Make sure you are positioned in the directory that you created to hold the Verilog source files. Invoke the command line batch file by entering the following text string.
This action will automatically invoke the VN-Property DX part of Verification Navigator and carry out the following steps.
… Check the syntax of the properties used in the design.
… Analyze and Instrument the Verilog source files.
… Call the simulator to collect dynamic property coverage information.
… Output a results file containing dynamic property coverage information.
… Produce text file(s) containing dynamic property coverage information.
The name of the results file is: vnavigator.index which is located in the default sub-directory: vnavigator_results
Viewing Coverage Results
There are two ways to view the detailed property coverage information that was produced by the command line batch file. You can either inspect the contents of the plain text coverage files with a text editor or use the GUI (graphical user interface) that is available within VN-Property DX. This worked example will make use of the graphical user interface which can be invoked by entering the following text string.
This action will bring up a top-level
flowchart, as shown in Figure F-1, to guide you through the various tools
that are available within Verification Navigator's verification environment.
The first button will invoke the Static Verification tool know as
VN-Check. Further details on this particular tool can be found in Appendix
second button will invoke the Dynamic Verification tool known as VN-Property
DX. You should click this button to bring up another flowchart, as shown
in Figure F-2 below. This flowchart is known as the Verification Flow
and is designed to guide you through the various parts of the Dynamic
third button will cause a window to be displayed that shows how many
of the design units or modules have satisfied the user specified sign-off
fourth button will invoke the Testsuite Optimisation tool know as VN-Optimise.
Further information on this particular tool can be found in Chapter
The Verification Flow flowchart, as shown in Figure F-2, is used to allow you to interact graphically with VN-Cover to create libraries, select the design files that you want to analyze and set up communication with your chosen simulator. As we have already generated the results file using the command line script (doit.pc.bat) you can skip this stage and move on to inspecting the dynamic coverage results.
Click the Results button - the sixth button
This action will bring up the window
as shown below.
Click the Load Results Files button to display the results files that are available.
Select the sub-directory labelled vnavigator_files
and then select the results file vnavigator_index
within that directory. This action will load the requested results
file. A summary of the dynamic property coverage that has been achieved is
displayed in the Results Summary window.
Clicking the Detail button, at the base
of the Results Summary window, will enable you to obtain detailed information
about dynamic property coverage for the various sub-sequences in the design.
The action of clicking the Detail button will cause the display screen to
change and become populated with the set of six windows as shown in Figure
The Flow Manager window is really an iconised version of the Verification Flow window and can be used as a way to return to the main flow if you need to repeat the instrumentation or simulation phases.
The right-hand section of the Hierarchy window, as shown in Figure F-6, shows a summary of the dynamic property coverage for the section of the design's hierarchy that is currently selected. At the moment the whole of the design's hierarchy (i.e. <root>) has been selected so what is indicated is a global summary for the property coverage for the whole design.
Shown on the left-hand section of the Hierarchy window is a list of the libraries that VN-Cover visited and found to contain properties. In this particular case two libraries are listed which have the names: "legal" and "prohibited".
The right-hand section of the Hierarchy window gives a breakdown of the properties that have been categorized into the two classes of `expected behaviour' and `prohibited behaviour'.
A detailed list of which particular properties were satisfied or violated can be obtained by clicking each one of the libraries listed under the Property Coverage heading in the left-hand section of the Hierarchy window.
Figure F-7 shows an example of the contents
of the Metrics View window after the library named Legal
has been selected in the Hierarchy window. As can be seen in the figure below,
three of the wanted or desired properties did not occur during the simulation
and have been flagged as an error condition. All the other properties listed
in the Metrics View window did occur at least once and therefore satisfied
the property coverage criteria.
Figure F-8 shows an example of the contents
of the Metrics View window after the library named Prohibited
has been selected in the Hierarchy window.
As can be seen in the above figure, one of the prohibited or not wanted properties actually occurred during the simulation and was flagged as an error condition. All the other properties (shown in the Metrics View window) never occurred which satisfied this particular property coverage criteria.