Getting started with Jasper Gold 7.1

Using Jasper Gold

The documentation of Jasper Gold is available in the directory /chalmers/sw/sup/jaspergold/7.1p003/jaspergold_7.1p003/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.

A very small example

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:


library ieee;
use ieee.std_logic_1164.all;
use ieee.std_logic_arith.all;

entity sum_of_last_two is
  generic( bits : natural );
  port( clk, reset : in std_logic;
        i : in unsigned(bits-1 downto 0);
        o : out unsigned(bits-1 downto 0) );
end entity sum_of_last_two;

architecture behav of sum_of_last_two is
  signal last : unsigned(bits-1 downto 0);
begin
  seq : process(clk, reset)
  begin
    if(reset = '1') then
      last <= conv_unsigned(0, bits);
    elsif(rising_edge(clk)) then
      last <= i;
    end if;
  end process seq;

  comb : process(last, i)
  begin
    o <= i + last;
  end process comb;
end architecture behav;

And the property file:


vunit sum_properties(sum_of_last_two(behav)) {

  default clock is (rising_edge(clk));



  property sum_correct is

   always next (o = i + prev(i));



  property sum_zero is

   always next (i = 0 -> o = prev(i));



  assert sum_correct;

  assert sum_zero;

}

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. circuit.vhdl and properties.psl). Then, make a Tcl script to tell Jasper Gold what to do with the files above:


analyze -vhdl circuit.vhdl

analyze -vhdl -psl properties.psl



elaborate -parameter bits 8 -vhdl -top sum_of_last_two(behav)



reset "reset"

clock clk

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 run.tcl. 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.

About these properties

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 (rising_edge(clk)). 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.

Differences between `next` and `prev`

One might expect next and prev to be each others inverses, and operate very similarly. However, the two are fundamentally different:

prev is a PSL function which given a VHDL-expression returns the value that the expression had in the last clock cycle.
next is a PSL construct with which you construct PSL formulas. If f is a PSL formula, then next f means that the formula f should be true in the next clock cycle.

In other words, we cannot express the property of our circuit as next(o) = i + next(i), since next will not give us the next value of a signal.

(The PSL book mentions such a next operator, but it is not implemented in Jasper Gold.)

Exercise (not to be handed in)

Modify the above VHDL program so that it sums not only the current and previous inputs, but the current and the two previous. You will have to be even more careful about your use of next and prev.
Play with changing the sizes of the instances that you verify in order to see the effect on verification time. (Remember that you had to fix generic parameters in the Tcl script.)

Parameterized properties

When working with parameterized (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.
The following property states that if the current and previous value of i are greater than or equal to 2**(bits-1) (half the possible range of nubers with bits number of bits, ** means exponentiation), then the output is less than the input (because of overflow):


  property sum_overflow is

   always next ((i >= (2**(bits-1))) AND (prev(i) >= (2**(bits-1))) -> o < i);

Since this property refers to the parameter bits, it actually talks about all possible instances of the circuit at the same time.

Documentation

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 7.1 tool is available in the directory /chalmers/sw/sup/jaspergold/7.1p003/jaspergold_7.1p003/doc .

Verifying reset

We said above that "the reset condition is always true before the initial clock cycle, and always false during and after the initial cycle". This means that properties like


  always reset -> output = 0;

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).

Coverage and type constraints

Jasper Gold automatically extracts coverage directives for properties with preconditions. These appear as additional tasks in the task list. If a coverage check fails, it means that you have a property where the precondition is always false (which means that the property is not really checking anything). This should be treated as a bug and be fixed accordingly. One exception is when the precondition involves the reset signal (see above).

If you declare your own enumerable type, e.g.


  type state_type is (start,idle,waiting,run,errors);

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.


  subtype count_type is integer range 0 to 9;

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.