This page provides a description of the language in which you can specify the how VHDL descriptions should behave when they are simulated. Such specification can then be checked fully automatically using CVC.
A specification is composed of a set of assumptions and commitments about a VHDL description. Assumptions describe an assumed behavior of the inputs (i.e. the signals of mode in) of the specified system. Commitments describe the behavior of the system provided that the guarantees hold. Assumptions can be viewed as axioms and commitments as theorems that can be derived from these axioms.
After the description of the language, we give a set of examples together with comments to guide the reader in its first steps with the language. We conclude by enumerating some common errors and give general guidelines for the efficient use of this language.
The grammar of the specification language is described as a set of production rules using Backus-Naur notation:
commitments
specification
assumption_formula ::= fairness | invariant
unit_designator::=[library.]entity(architecture)
tl_term::= un_cycle_quantifier commit_formula | [commit_formula bin_cycle_quantifier commit_formula]
specification_body::= {specification_item}
Case sensitivity and comments are as in VHDL: anything on a line hat follows two consecutive dashes is a comment and is ignored, and the language is case insensitive.
specification ::= specification identifier of unit_designator is specification_body end [specification] [identifier] ;
A specification applies to a specific VHDL design unit, identified by:
unit_designator::=[library.]entity(architecture)
A design unit must be an architecture body. The library designator is optional, in which case the unit is expected to be in the working library. It is an error if the designated unit is not in the designated library. Identifiers visible in the architecture body are also visible in the specification. Identifiers declared in declarative regions nested in the architecture body are also visible in the specification. If identifier conflicts occur, the identifier declared in the topmost region is visible. If there is still a conflict after this rule is applied, the visibility is undefined (this problem shall be resolved in the future).
specification_body ::= {specification_item}
specification_item::= abbreviation | assumption | commitment
The body of the specification is a list of specification items. A specification item can be an assumption, a commitment or an abbreviation.
abbreviation ::= abbreviation abbreviation_item {, abbreviation_item};
abbreviation_item::= identifier is expression
Abbreviations play the role of macros and permit to use identifiers to denote expressions. When the identifier later occurs in a term, it is expanded to the abbreviated expression. The expression can be any VHDL expression. Any VHDL declaration with the same identifier is hidden after the abbreviation.
assumption::= assume assumption_formula ;
assumption_formula::= invariant | fairness
invariant ::= always in_condition
fairness ::= recurring in_condition
in_condition must be a valid VHDL condition on the signals of mode in declared in the corresponding entity header. An invariant condition is assumed to hold in every simulation cycle, whereas a recurring condition is assumed to be valid infinitely often (see examples below). The scope of an assumption extends to the whole specification. Even if a commitment is expressed before an assumption, this assumption will be taken into account during its verification.
commitment:: commit identifier : term;
A commitment must have an identifier. This identifier is not considered as a declaration, thus it does not hide VHDL or abbreviation declarations. This identifier is used to label the tl_formula when reporting results.
term ::= condition | factor | (term)
factor ::= primary | not primary | primary { and primary } | primary { or primary} | primary { xor primary} | primary { xnor primary} | primary { => primary} | primary nand primary | primary nor primary
=> is the implication operator.
primary ::= simulation_quantifier ltl_term
simulation_quantifier::= a | e
a and e are the universal and existential quantifiers. Thus they respectively mean "for all simulations" and "for some simulation".
ltl_term::= un_cycle_quantifier term| [ term bin_cycle_quantifier term ]
un_cycle_quantifier::= x | f | g
bin_cycle_quantifier::= u | w
If F and G are arbitrary terms:
Thus, FwG is the same as (FuG) or (gF).
Abbreviations are a simple form of macros (without parameters). For instance:
abbreviation PUSHED is (PUSH and PUSH_RDY);
In the rest of the specification body, PUSHED will stand for the expression (PUSH and PUSH_RDY).
Recall that assumptions are conditions on the inputs of the system. In our VHDL subset, inputs are signals of mode in . Such condition can be assumed to be valid for all cycles of the simulation (we call these invariants) or valid infinitely often during a simulation (these are named fairness).
Let us consider a simple stack controller. The interface of such system can be:
entity STACK is (PUSH, POP: in BIT; PUSH_RDY, POP_RDY: out BIT) end entity STACK;
In order to indicate that the behavior of the stack has to be verified in an environment where the signals PUSH and POP are never asserted simultaneously, insert the following:
assume always not ((PUSH = '1' ) and (POP = '1'));
In general, invariants makes the verification less time consuming
Let us consider any clocked circuit.
entity E is (CLOCK: in BIT; ...) end entity E;
You do not wish to consider simulations where the clock signal remains infinitely stuck at '0' or at '1'. To do so, you have to say that it is infinitely equal to '0' and infinitely equal to '1', which is expressed as two fairness assumptions:
assume recurring (CLOCK = '0');
assume recurring (CLOCK = '1');
In general, fairness constraints makes the verification more time consuming.
Commitments can sometimes be tricky to read. Fortumately, important classes of properties can be expressed quite simply.
Suppose you want to check that something bad never happens. This something bad could be for instance that several supposedly mutually exclusive signals are simultaneously high, such as in a RTL description of a one-hot FSM, state-encoding flip-flops, or acknowledges to the clients of a bus controller, etc. This something bad can be bbreviated:
abbreviation MUTUAL_EXCLUSION_VIOLATED is <some condition> ;
The following commitment states that this bad thing never happens:
commit safe: ag not MUTUAL_EXCLUSION_VIOLATED;
This formula means "for all simulation, for all cycles, not MUTUAL_EXCLUSION_VIOLATED", or more succintly "it is always the case that not MUTUAL_EXCLUSION_VIOLATED".
From now on we will read ag as "it is always the case that"
In general, to check a formula of the form ag f, where f is a VHDL condition, with conventional simulation techniques, you have to write an assert statement in your testbench with the condition f, and then perform a complete coverage. Good luck!
A system can be restarted if whatever is current state is, it can eventually be driven to some so-called restart state. Let RESTART be the condition that represent this restart state:
commit RESTARTABLE: ag ef RESTART;
This formula reads "it is always the case that there is a simulation where in the future RESTART"
It is as well possible to he behavior of a design on a certain event. For instance, suppose you have an edge-triggered register. LD is the load signal, D_IN and D_OUT are the input and output data line:
commit load_1:ag((LD='0') => ax ((LD='1') => (D_IN='1') => af (D_OUT='1')));
This reads "it is always the case that if LD equal '0' then for all simulations at the next cycle if LD equals '1' then if D_IN equal '1' then for all simulations in a future cycle D_OUT equals '1'".
The pattern to retain here is to express that whenever the value of S changes from a to b then f is valid does the job: ag (S = a) => (ax (S = b) => f ).
Writing specifications that are different than what you have in mind is quite common. Hopefully, specifications are easier to debug than a VHDL description. Here is a list of things you should take care about when you write down a specification:
Precautions you should take while writing a specification resembles those you (should) take when programming: better to write several simple specifications than a large and complex one; group related properties into the same specification; specify incrementally, getting more and more precise as you gain confidence in your design and your specification, document your specifications.
First we show how to set up VHDL libraries, and in particular you should create the library STD before doing anything else with CV.
We then go on how to use CV in conjunction with standard EDA tools to debug your designs (section 5.2).
In the following, comands shall be typefaced in typewriter style.
You must have got hold of the CV distribution and compiled it if necessary. This distribution includes theVHDL analyzer cva and a VHDL model checker cvc. In order to use cva, you must setup a set of physical libraries and a mapping from logical library names to physical library names. A physical library is a directory, therefore it is created with the command mkdir. The mapping is realized via environment variable and the command setenv.
To illustrate these concepts we show how the STD library can be created and how the package STANDARD can be compiled in this library.
We first start by creating a directory $HOME/lib/cv where e will store all the physical libraries we will need:
> mkdir $HOME/lib/cv
We then create a physical library $HOME/lib/cv/std and map the logical name STD to this directory:
> mkdir $HOME/lib/cv/std
> setenv std $HOME/lib/cv/std
NOTE: Library logical names must be lowercase.
Before compiling the package STANDARD, we must set the working library. The mapping working library to logical library name is also realized with environment variable:
> setenv work std
Now we can compile the package:
> cva $HOME/cv.beta.1/vhdl/std/standard.vhdl
saving file /home/deharbe/lib/cv/std/standard.cv
To verify that a library unit was created in the library STD, list its contents:
> ls -l $std
-rw-r--r-- 1 deharbe 6616 Aug 16 14:22 standard.cv
Environment variables must be set each time you open a shell. You can do this in the file $HOME/.cshrc. For instance, for library STD:
setenv std $HOME/lib/cv/std
In this section we present a gate-level description of a simple mutual exclusion arbiter. We specify the mutual exclusion property and show that it is not valid. We get a VHDL that can be used to run a counterexample simulation, we leads us to the error location. After correction, we prove that the mutual exclusion is now valid.
The VHDL description is in the file me.vhdl.
> cat me.vhdl
entity CIRCUIT_ME is
port(REQ1, REQ2: in BIT;
ACK1, ACK2: out BIT;
CK: in BIT);
end CIRCUIT_ME;
architecture GATES of CIRCUIT_ME is
signal PS1, PS2, M1: bit;
signal L1, L4, L7, L10, L11, L12, L13, L14, L15, L19, L20: BIT;
begin
L1 <= not(REQ1 and REQ2);
L4 <= L1 or REQ1; -- should be L1 and REQ1
L10 <= PS1 or PS2;
L11 <= L10 and (not L1);
L12 <= L11 and PS1;
L13 <= PS2 and L11;
L14 <= (not L10) and (not L1);
L15 <= L14 and M1;
L7 <= not M1 and L14;
L19 <= L12 or L7 or L4;
L20 <= L15 or L13 or (L1 and REQ2);
ACK1 <= L19;
ACK2 <= L20;
MAIN:process
begin
wait on CK until CK='1';
PS1 <= L19;
PS2 <= L20;
M1 <= L19 or (not L20 and M1);
end process MAIN;
end GATES;
We first suppose there is an existing library design where we want to compile this description. So we first set this library as the working library and then compile the file:
> setenv work design > cva me.vhdl saving file /home/deharbe/lib/cv/design/circuit_me.cv saving file /home/deharbe/lib/cv/design/circuit_me-gates.cv
We would now like specify that indeed the grant signals ACK1 and ACK2 are never simultaneously high, i.e. equal to '1'. The specification file mutex.spec states exactly this:
> cat mutex.vhdl specification MUTEX of DESIGN.CIRCUIT_ME(GATES) is commit EXCLUSIVE: ag (not (PS1='1' and PS2='1')); end specification;
To check this specification, we call the program cvc with the following options:
> cvc -Wvhdl -hstill-inputs mutex
cvc: Cmu Vhdl model Checker (release 1.b.1)
specification: mutex.spec
design: univ_mrs.circuit_me(gates)
elaborating model
done
user time: 0.09s, system time: 0.02s
simplifying [dynamic reodering]
done
user time: 0.20s, system time: 0.00s
computing reachable states
[1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12]
The model has 1.374E+11 potential states (37 variables).
[1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12] [13] )
2984 states are reachable and 680 are stable.
822 nodes represent the valid states.
done
user time: 9.20s, system time: 1.22s
simplifying transition representation
reducing model...
...model reduction done
size of transition representation: 0
Model checking started
exclusive: AG (not ((ps1 = '1') and (ps2 = '1')))
checking property exclusive...
-- property exclusive is invalid --
user time: 0.05s, system time: 0.00s
Approximate bytes used: 396280
Number of nodes: 6654
Number of variables: 40
total time
user time: 10.99s, system time: 1.38s
cvc first displays the specification file name, and the design library, primary name, and secondary name. It then prints the different computation steps prior to the verification itself, which has a negative result. Various usage statistics are then printed. Since the property is not valid, a file containing a VHDL testbench has been generated. The name of this file is composed of the description names and the invalid property identifier:
> cat circuit_me-gates-exclusive.vhdl
entity TESTBENCH is
end;
architecture circuit_me_gates_exclusive of TESTBENCH is
signal a : bit := '0';
signal b : bit := '0';
signal s1 : bit := '0';
signal s2 : bit := '0';
signal ck : bit := '0';
component circuit_me
port(a: in bit; b: in bit; s1: out bit; s2: out bit; ck: in bit);
end component;
for all: circuit_me use entity work.circuit_me(gates);
begin
TEST: circuit_me port map(a, b, s1, s2, ck);
stimulus: process
begin
a <= '0';
b <= '1';
ck <= '0';
wait for 10 ns;
a <= '1';
b <= '0';
ck <= '1';
wait for 10 ns;
a <= '1';
b <= '0';
ck <= '0';
wait for 10 ns;
wait;
end process;
end;
If you simulate this file with a conventional simulator and trace the values of the interface signals, then you will see that signals ACK1 and ACK2 are simultaneously equal to '1'. This simulation can be used to trace back the error in the source code at the place indicated in the comments. Once the modifications are done, the VHDL description has to b recompiles with cva. You get the expected output from cvc:
> cva me.vhdl
...
> cvc -Wvhdl -hstill-inputs mutex
cvc: Cmu Vhdl model Checker (release 1.b.1)
specification: mutex.spec
design: univ_mrs.circuit_me(gates)
elaborating model
done
user time: 0.07s, system time: 0.03s
simplifying [dynamic reodering]
done
user time: 0.27s, system time: 0.00s
computing reachable states
[1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12]
The model has 1.374E+11 potential states (37 variables).
[1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12] [13] [14] [15] [16] [17] [18] )
4808 states are reachable and 904 are stable.
1405 nodes represent the valid states.
done
user time: 9.25s, system time: 1.54s
simplifying transition representation
reducing model...
...model reduction done
size of transition representation: 0
Model checking started
exclusive: AG (not ((ps1 = '1') and (ps2 = '1')))
checking property exclusive...
++ property exclusive is valid ++
user time: 0.03s, system time: 0.00s
Approximate bytes used: 340856
Number of nodes: 6781
Number of variables: 40
total time
user time: 10.01s, system time: 1.61s
Acknowledgements:
We would like to thank Laurence Pierre and Philippe Georgelin from Université de Provence, Marseilles, France for providing us (the correct version of) this example.
Documentation Sections: cva(1) VHDL Grammar cvc(1) Specification Language
Main Sections: Introduction Installation Documentation Examples