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

---

13.8.1  An Example

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

entity Alarm is

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

end Alarm;

The following behavioral architecture is the reference model :

architecture RTL of Alarm is

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

begin

process (Clock) begin

if Clock = '1' and Clock'EVENT then

case State is

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

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

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

end if ;

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

end case ;

end if ;

end process ;

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

end RTL;

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

signal s0, s1, s2, s3 : BIT;

begin

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

end Gates;

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:

formulas to be proved: 8

formulas proved VALID: 8

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 :

# axioms

Let Axiom_ref = Axioms Of alarm-rtl

Let Axiom_der = Axioms Of alarm-gates

ProveNotAlwaysFalse (Axiom_ref)

Prove (Axiom_ref => Axiom_der)

# assertions

Let Assert_ref = Asserts Of alarm-rtl

Let Assert_der = Asserts Of alarm-gates

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

# clocks

Let ClockEvents_ref = Clocks Of alarm-rtl

Let ClockEvents_der = Clocks Of alarm-gates

Let Master__clock_event_ref =

Value (master__clock'event Of alarm-rtl)

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

# next state of memories

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

# validity value of outbuses

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.

TABLE 13.13  Implication and equivalence.
A	B	A ⇒ B	A ¤ B
F	F	T	T
F	T	T	F
T	F	F	F
T	T	T	T

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:

<E> Assertion may be violated

SEVERITY: ERROR

REPORT: Alarm on and tripped but not ringing

FILE: .../alarm-rtl3.vhdl

FSM: alarm-rtl3

STATEMENT or DECLARATION: line8

.../alarm-rtl3.vhdl (line 8)

Context of the message is:

(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 ):

case State is

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

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

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

end if ;

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

end case ;

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

Formula is NOT VALID

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:

***Difference is:

(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:

Not state(1) Or Not state(0)

There are 2 cubes and 2 literals in the complete equation

 

formulas to be proved: 8

formulas proved VALID: 7

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:

...

case State is

when Off => if Key = '1' then

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

else NextState <= Armed;

end if ;

end if ;

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

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

end if ;

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

end case ;

...

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.