[ 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 finitestate 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 alarmrtl
Let Axiom_der = Axioms Of alarmgates
ProveNotAlwaysFalse (Axiom_ref)
Prove (Axiom_ref => Axiom_der)
Let Assert_ref = Asserts Of alarmrtl
Let Assert_der = Asserts Of alarmgates
Prove (Axiom_ref => (Assert_ref => Assert_der))
Let ClockEvents_ref = Clocks Of alarmrtl
Let ClockEvents_der = Clocks Of alarmgates
Value (master__clock'event Of alarmrtl)
Prove (Axiom_ref => (ClockEvents_ref <=> ClockEvents_der))
Prove ((Axiom_ref And Master__clock_event_ref) =>
(Transition (state(1) Of alarmrtl) <=>
Transition (state_ff_b1.t Of alarmgates)))
Prove ((Axiom_ref And Master__clock_event_ref) =>
(Transition (state(0) Of alarmrtl) <=>
Transition (state_ff_b0.t Of alarmgates)))
Prove (Axiom_ref => (Domain (ring Of alarmrtl) <=>
Domain (ring Of alarmgates)))
Prove (Axiom_ref => (Domain (ring Of alarmrtl) =>
(Value (ring Of alarmrtl) <=>
Value (ring Of alarmgates))))
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 finitestate 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 topsecret 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 alarmrtl3
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 ]
