A short demo on how to use Jasper Gold is given in the first lecture. The documentation of Jasper Gold is available in the directory
/cab/cestud/sw/jaspergold/4.6.p002/jaspergold_4.6p002/doc/. You can get access
to the reference manual by clicking on Help (the rightmost menu item) in the tool.
Start Jasper Gold by typing
jg at a shell prompt.
To focus on some important details, we show an example of how to use Jasper Gold. We will verify that a very simple circuit works. The circuit takes an unsigned as input, and gives back an unsigned, which is the sum of the current value of the input and the previous value of the input. Here is the VHDL code:
And the property file:
This shows the main structure of a PSL file. More properties can be added in the same way. Make sure you don't forget
rising_edge in the clock expression. If you do, you will get very strange counter examples.
Put these two pieces of code in two files (e.g.
Then, make a Tcl script to tell Jasper Gold what to do with the files above:
The first two lines will read in the circuit and its properties. In the third line, we state that we want to verify the entity
sum_of_last_two and the architecture
behav. We also instantiate the generic parameter
bits to the value 8 (since we can only verify specific instances of generic circuits).
The script also tells which clock signal and reset condition to use in the verification.
Verification is done under the assumption that the reset condition is always true before the initial clock cycle, and always false during and after the initial cycle.
Put the script in a file (e.g.
run.tcl) and start Jasper Gold.
Click on the button in the upper left corner of the tool bar and choose the file
You can also give the commands in the script directly at the Jasper Gold prompt, or by clicking in the menus.
The upper left window now shows a tree of modules (which happens to only contain one node, since this is not a structural description). The upper right window shows the properties associated with the selected module.
To attempt to prove the selected properties, simply type
prove -all   at the prompt (or find the corresponding button). If the proof succeeds, you will see a green mark at each property. If a proof fails, the property will be marked by a red cross.
We have declared two properties:
sum_correct, which says that the output should be the sum of the current and the previous value of the input, and
sum_zero, which is only a special case of the previous property, included only to show how to write several properties in the same file.
We also tell Jasper Gold what our clock event is for these properties (
Finally, we assert that these two properties should be checked by Jasper Gold.
So, why do we have a
next in the properties? What a property of the shape
always next P really means is that in all cycles, except possibly the first one, P holds. The reason for using it is that
prev is not defined in the first clock cycle, therefore all properties involving
prev must include a next before the prev.
generic) circuits, it's a good practice to verify a few different instances -- not just one. In this case, instead of writing separate properties for each instance (which makes it easy to introduce copy-paste errors), it is often convenient to make the properties parameterized so that the same property can cover all instances. We can do this simply by referring to the generic parameter in the properies.
iare greater than or equal to
2**(bits-1)(half the possible range of nubers with
bitsnumber of bits,
**means exponentiation), then the output is less than the input (because of overflow):
Since this property refers to the parameter
bits, it actually talks about all
possible instances of the circuit at the same time.
There is an excellent PSL reference guide available with the Jasper Gold distribution. If you're running on a Chalmers computer, you'll find it here. Print this guide (it is two pages long) and keep it next to you while you're writing your properties. (Some parts of the guide may be outdated, but most of it is still valid.)
The full documentation for the Jasper Gold 4.6 tool is available in the directory
An example design with properties can be found in the directory
will always be true, regardless of whether reset is working or not. Jasper Gold discovers such vacuous properties and reports them as precondition failures (see below). If you want to verify the reset behavior (not required for our labs), you can just remove (or change) the reset condition from the Tcl file. This may of course cause other properies to fail (if they depend on correct initialization).
If you declare your own enumerable type, e.g.
values of this type will be encoded as a bit vector with as few bits as possible. In the example above, this means three bits. Using three bits for
state_type means that we'll have eight possible states, but only five which are legal. The same situation arises for sub-types, like e.g.
To check that the synthesized design is not able to end up in an illegal state (after reset), Jasper Gold extracts type constraints for such signals. Type constraint violations should also be treated as bugs. The normal solution is to use the reset signal to force the design into a legal state.