 |
 |
 |
 |
| |
|
Appendix F
Dynamic Property Checking - Worked Examples
Resources
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: vmm@transeda.com
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.
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.
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.
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 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 the flowchart.
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 F-5.
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.
|
|
