[ Chapter start ] [ Previous page ] [ Next page ]

# 13.8 Formal Verification

Using logic synthesis we move from a behavioral model to a structural model. How are we to know (other than by trusting the logic synthesizer) that the two representations are the same? We have already seen that we may have to alter the original reference model because the HDL acceptable to a synthesis tool is a subset of HDL acceptable to simulators. Formal verification can prove, in the mathematical sense, that two representations are equivalent. If they are not, the software can tell us why and how two representations differ.

## 13.8.1 An Example

We shall use the following VHDL entity with two architectures as an example: 1

**
port**
(Clock, Key, Trip : **
in**
bit; Ring : **
out**
bit);

The following behavioral architecture is the reference model :

**
type**
States **
is**
(Armed, Off, Ringing); **
signal**
State : States;

**
if**
Clock = '1' **
and**
Clock'EVENT **
then**

**
when**
Off => **
if**
Key = '1' **
then**
State <= Armed; **
end**
**
if**
;

**
when**
Armed => **
if**
Key = '0' **
then**
State <= Off;

**
elsif**
Trip = '1' **
then**
State <= Ringing;

**
when**
Ringing => **
if**
Key = '0' **
then**
State <= Off; **
end**
**
if**
;

Ring <= '1' **
when**
State = Ringing **
else**
'0';

The following synthesized structural architecture is the derived model :

**
library**
cells; **
use**
cells.**
all**
; // ...contains logic cell models

**
architecture**
Gates **
of**
Alarm **
is**

**
component**
Inverter **
port**
(i : **
in**
BIT;z : **
out**
BIT) ; **
end**
**
component**
;

**
component**
NAnd2 **
port**
(a,b : **
in**
BIT;z : **
out**
BIT) ; **
end**
**
component**
;

**
component**
NAnd3 **
port**
(a,b,c : **
in**
BIT;z : **
out**
BIT) ; **
end**
**
component**
;

**
component**
DFF port(d,c : **
in**
BIT; q,qn : **
out**
BIT) ; **
end**
**
component**
;

**
signal**
State, NextState : BIT_VECTOR(1 **
downto**
0);

g2: Inverter **
port**
**
map**
( i => State(0), z => s1 );

g3: NAnd2 **
port**
**
map**
( a => s1, b => State(1), z => s2 );

g4: Inverter **
port**
**
map**
( i => s2, z => Ring );

g5: NAnd2 **
port**
**
map**
( a => State(1), b => Key, z => s0 );

g6: NAnd3 **
port**
**
map**
( a => Trip, b => s1, c => Key, z => s3 );

g7: NAnd2 **
port**
**
map**
( a => s0, b => s3, z => NextState(1) );

g8: Inverter **
port**
**
map**
( i => Key, z => NextState(0) );

( d => NextState(0), c => Clock, q => State(0), qn => **
open**
);

( d => NextState(1), c => Clock, q => State(1), qn => **
open**
);

To compare the reference and the derived models (two representations), formal verification performs the following steps: (1) the HDL is parsed, (2) a finite-state machine compiler extracts the states present in any sequential logic, (3) a proof generator automatically generates formulas to be proved, (4) the theorem prover attempts to prove the formulas. The results from the last step are as follows:

By constructing and then proving formulas the software tells us that architecture RTL implies architecture Gates (implication is the default proof mechanism—we could also have asked if the architectures are exactly equivalent). Next, we shall explore what this means and how formal verification works.

## 13.8.2 Understanding Formal Verification

The formulas to be proved are generated in a separate file of proof statements :

Let Axiom_ref = Axioms Of alarm-rtl

Let Axiom_der = Axioms Of alarm-gates

ProveNotAlwaysFalse (Axiom_ref)

Prove (Axiom_ref => Axiom_der)

Let Assert_ref = Asserts Of alarm-rtl

Let Assert_der = Asserts Of alarm-gates

Prove (Axiom_ref => (Assert_ref => Assert_der))

Let ClockEvents_ref = Clocks Of alarm-rtl

Let ClockEvents_der = Clocks Of alarm-gates

Value (master__clock'event Of alarm-rtl)

Prove (Axiom_ref => (ClockEvents_ref <=> ClockEvents_der))

Prove ((Axiom_ref And Master__clock_event_ref) =>

(Transition (state(1) Of alarm-rtl) <=>

Transition (state_ff_b1.t Of alarm-gates)))

Prove ((Axiom_ref And Master__clock_event_ref) =>

(Transition (state(0) Of alarm-rtl) <=>

Transition (state_ff_b0.t Of alarm-gates)))

Prove (Axiom_ref => (Domain (ring Of alarm-rtl) <=>

Domain (ring Of alarm-gates)))

Prove (Axiom_ref => (Domain (ring Of alarm-rtl) =>

(Value (ring Of alarm-rtl) <=>

Value (ring Of alarm-gates))))

Formal verification makes strict use of the terms axiom and assertion . An axiom is an explicit or implicit fact. For example, if a VHDL signal is declared to be type BIT , an implicit axiom is that this signal may only take the logic values '0' and '1' . An assertion is derived from a statement placed in the HDL code. For example, the following VHDL statement is an assertion:

assert Key /= '1' or Trip /= '1' or NextState = Ringing

report "Alarm on and tripped but not ringing";

A VHDL assert statement prints only if the condition is FALSE . We know from de Morgan’s theorem that (A + B + C)' = A'B'C' . Thus, this statement checks for a burglar alarm that does not ring when it is on and we are burgled.

In the proof statements the symbol '=>' means implies . In logic calculus we write A ⇒ B to mean A implies B . The symbol '<=>' means equivalence , and this is stricter than implication. We write A ¤ B to mean: A is equivalent to B . Table 13.13 show the truth tables for these two logic operators.

## 13.8.3 Adding an Assertion

If we include the assert statement from the previous section in architecture RTL and repeat formal verification, we get the following message from the FSM compiler:

REPORT: Alarm on and tripped but not ringing

STATEMENT or DECLARATION: line8

(key And trip And memoryofdriver__state(0))

This message tells us that the assert statement that we included may be triggered under a certain condition: (key And trip And state(0)) . The prefix 'memoryofdriver__' is used by the theorem prover to refer to the memory element used for state(0) . The state 'off' in the reference model corresponds to state(0) in the encoding that the finite-state machine compiler has used (and also to state(0) in the derived model). From this message we can isolate the problem to the following case statement (the line numbers follow the original code in architecture RTL ):

**
when**
Off => **
if**
Key = '1' **
then**
State <= Armed; **
end**
**
if**
;

**
when**
Armed => **
if**
Key = '0' **
then**
State <= Off;

**
elsif**
Trip = '1' **
then**
State <= Ringing;

**
when**
Ringing => **
if**
Key = '0' **
then**
State <= Off; **
end**
**
if**
;

When we start in state Off and the two inputs are Trip = '1' and Key = '1' , we go to state Armed , and not to state Ringing . On the subsequent clock cycle we will go state Ringing , but only if Trip does not change. Since we have all seen “Mission Impossible” and the burglar who exits the top-secret computer room at the Pentagon at the exact moment the alarm is set, we know this is perfectly possible and the software is warning us of this fact. Continuing on, we get the following results from the theorem prover:

Prove (Axiom_ref => (Assert_ref => Assert_der))

But is VALID under Assert Context of alarm-rtl3

We included the assert statement in the reference model ( architecture RTL ) but not in the derived model ( architecture Gates ). Now we are really mixed up: The assertion statement in the reference model says one thing, but the case statement in the reference model describes another. The theorem prover retorts: “The axioms of the reference model do not imply that the assertions of the reference model imply the assertions of the derived model.” Translation: “These two architectures differ in some way.” However, if we assume that the assertion is true (despite what the case statement says) then the formula is true. The prover is also saying: “Make up your mind, you cannot have it both ways.” The prover goes on to explain the differences between the two representations:

(Not state(1) And key And state(0) And trip)

There are 1 cubes and 4 literals in the complete equation

***Local Variable Assert_der is:

Not key Or Not state(0) Or Not trip

There are 3 cubes and 3 literals in the complete equation

***Local Variable Assert_ref is: 1

***Local Variable Axiom_ref is:

There are 2 cubes and 2 literals in the complete equation

formulas VALID under assert context of der.model: 1

Study these messages hard and you will see that the differences between the two models are consistent with our explanation.

## 13.8.4 Completing a Proof

To fix the problem we change the code as follows:

**
if**
Trip = '1' **
then**
NextState <= Ringing;

**
when**
Armed => **
if**
Key = '0' **
then**
NextState <= Off;

**
elsif**
Trip = '1' **
then**
NextState <= Ringing;

**
when**
Ringing => **
if**
Key = '0' **
then**
NextState <= Off; **
end**
**
if**
;

This results in a minor change in the synthesized netlist,

g2: Inverter port map ( i => State(0), z => s1 );

g3: NAnd2 port map ( a => s1, b => State(1), z => s2 );

g4: Inverter port map ( i => s2, z => Ring );

g5: NAnd2 port map ( a => State(1), b => Key, z => s0 );

g6: NAnd3 port map ( a => Trip, b => s1, c => Key, z => s3 );

g7: NAnd2 port map ( a => s0, b => s3, z => NextState(1) );

g8: Inverter port map ( i => Key, z => NextState(0) );

state_ff_b0: DFF port map ( d => NextState(0), c => Clock, q => State(0), qn => open );

state_ff_b1: DFF port map ( d => NextState(1), c => Clock, q => State(1), qn => open );

Repeating the formal verification confirms and formally proves that the derived model will operate correctly. Strictly, we say that the operation of the derived model is implied by the reference model.

[ Chapter start ] [ Previous page ] [ Next page ]