Verifying Parametrised Hardware Designs
via Counter Automata
A. Smrčka1
T. Vojnar1
1 Faculty
of Information Technology
Brno University of Technology
Haifa Verification Conference 2007, Haifa, IL
Smrčka, Vojnar (FIT BUT, CZ)
Hardware Design → Counter Automaton
Outline
1
Motivation
2
Basics of RTL design and VHDL
3
Counter automata
4
Transformation VHDL → counter automata
5
Bad state specification
6
Experiments + conclusions
Smrčka, Vojnar (FIT BUT, CZ)
Hardware Design → Counter Automaton
A Common Process of FV of HW Design
A generic RTL design (VHDL, Verilog, . . . ) transformed to a
design using a given kind of gates.
RTL design
synthesis
gate-level
design
Smrčka, Vojnar (FIT BUT, CZ)
Hardware Design → Counter Automaton
A Common Process of FV of HW Design
Transforming gate-level design into a hardware description.
RTL design
synthesis
gate-level
design
place & route
hardware
Smrčka, Vojnar (FIT BUT, CZ)
Hardware Design → Counter Automaton
A Common Process of FV of HW Design
Given a specification and a gate-level design we can perform
formal verification (MC on a finite state systems).
RTL design
synthesis
gate-level
design
FV
place & route
Ok / bug
hardware
Smrčka, Vojnar (FIT BUT, CZ)
Hardware Design → Counter Automaton
A Common Process of FV of HW Design
Problem with parametric/generic properties of design.
Motivation: How to verify parametrised hardware design
generic
RTL design
concrete
synthesis
gate-level
design
FV
place & route
Ok / bug
hardware
Smrčka, Vojnar (FIT BUT, CZ)
Hardware Design → Counter Automaton
The Main Idea
Transform RTL design to a counter automaton, specify the set
of bad states, model check the generated automaton.
generic
RTL design
concrete
synthesis
transformation
counter
automaton
FV
gate-level
design
FV
place & route
Ok / bug
Ok / bug
hardware
Smrčka, Vojnar (FIT BUT, CZ)
Hardware Design → Counter Automaton
RTL Hardware Design
Register Transfer Level – RTL design provides a high-level
description of a circuit behaviour by defining the data transfer
between hardware registers and logical operations.
Logic gate – implements one of logical operations
¬, ∧, ∨, . . . (output depends only on the current input
combination)
Register (sequential gate) – a hardware element with
memory (output depends on the current and the past
inputs)
Signal – a wire that transfers data among combinational
and sequential gates
Component (module, entity) – an encapsulation of digital
circuit + I/O control
Smrčka, Vojnar (FIT BUT, CZ)
Hardware Design → Counter Automaton
Semantics of VHDL Constructs
Hardware design is described in a modular way.
entity counter is
generic ( max: integer );
port (
reset, clk: in std_logic;
cnt: out std_logic_vector(32 downto 0);
zf: out std_logic;
max
);
end entity;
clk
architecture cnt_arch of counter is
cnt =
begin
(cnt+1)
reset
process (reset, clk)
% max
begin
if (reset=’1’) then cnt <= 0;
elsif (clk’event and clk=’1’) then
if (cnt = max-1) then cnt <= 0;
else cnt <= cnt+1;
end if;
end if;
end process;
comp: entity comp32 port map ( cnt, 0, zf );
end;
Smrčka, Vojnar (FIT BUT, CZ)
Hardware Design → Counter Automaton
cnt
zf
Counter Automata
A counter automaton A = (X , Q, q0 , ϕ0 , δ)
X – a finite set of variables (counters)
Q – a finite set of control locations
q0 ∈ Q – a designated initial location
ϕ0 – an arithmetic formula of initial assignment
δ ⊆ Q × Φ(X ) × Q – a transition relation
Φ(X ) – a formula over X and X 0 (future references of
counters)
Example: Increment x modulo max + zero test
Z
Zx = 0
Z#
Z
q0
x < max
x0 = x + 1
"!x
= max
#
x < max
q1
x0 =
"!
x +1
x0 = 0
Smrčka, Vojnar (FIT BUT, CZ)
Hardware Design → Counter Automaton
Intermediate Behavioural Model
A direct mapping from VHDL source code to counter
automaton is too complex → introduce an intermediate
behavioural model as the “bridge”.
InterBM
RTL design
counter
automaton
Steps to produce a counter automaton:
1
Normalize the VHDL code of an RTL design
2
Refine an intermediate behavioural model
3
Build the counter automaton
Smrčka, Vojnar (FIT BUT, CZ)
Hardware Design → Counter Automaton
RTL Design :: Normalization of VHDL Code
Goal: obtain code using registered signals (1-bit type, bit
vectors), behavioural description, assignment statement + if
stmt only
1
Variables of user defined structural types → more variables
of simple types (single bit, bit vectors).
Bit vectors (constant size) accessed bitwise → more 1-bit
signals.
Bitwise operations over parameter sized bit vectors →
more complex arithmetic operations over bit vectors
2
Structural description → behavioural description (only
process and assignment statements are allowed)
3
Non-registered signals → expressions over registered
signals
4
Conditional assignments (with, case) → if statements
Smrčka, Vojnar (FIT BUT, CZ)
Hardware Design → Counter Automaton
Intermediate Behavioural Model :: Definition
M = (V , T , B), where:
V – a set of variables, we use V as “references” to V :
v
time
v =0
v0 = 1
↑v = 1
↓v = 0
current value of v
future value
positive edge ↑v = ¬v ∧ v 0
negative edge ↓v = v ∧ ¬v
T : V → {bool, int} – the type of a variable
Let E be a set of expressions over V (+, −, =, 6=, ≥, ¬, ∧, . . . ),
Let C ⊆ E be the set of boolean valued expressions.
B ⊆ C ∗ × V × E is a set of behavioural rules representing
conditioned assignments (b ∈ B, b : c → v := e)
Smrčka, Vojnar (FIT BUT, CZ)
Hardware Design → Counter Automaton
Intermediate Behavioural Model :: Definition
M = (V , T , B), where:
V – a set of variables, we use V as “references” to V :
v
time
v =0
v0 = 1
↑v = 1
↓v = 0
current value of v
future value
positive edge ↑v = ¬v ∧ v 0
negative edge ↓v = v ∧ ¬v
T : V → {bool, int} – the type of a variable
Let E be a set of expressions over V (+, −, =, 6=, ≥, ¬, ∧, . . . ),
Let C ⊆ E be the set of boolean valued expressions.
B ⊆ C ∗ × V × E is a set of behavioural rules representing
conditioned assignments (b ∈ B, b : c → v := e)
res0
¬res , ↑clk , (addr 6= max − 1)
¬res0 , ↑clk , (addr = max − 1)
¬res0 , ¬↑clk
0
Smrčka, Vojnar (FIT BUT, CZ)
→
→
→
→
addr
addr
addr
addr
:= 0
:= addr + 1
:= 0
:= addr
Hardware Design → Counter Automaton
Model :: Extracting from Source Code (1/2)
InterBM
RTL design
counter
automaton
M = (V , T , B)
Variables V contain all registered signals + parameters
T (v ) = bool if v is 1-bit signal,
T (v ) = int if v is a bit vector or a parameter
A VHDL expression: (clk’event and clk = ’1’)
InterBM expression: ↑clk ∈ E
Smrčka, Vojnar (FIT BUT, CZ)
Hardware Design → Counter Automaton
Model :: Extracting from Source Code (2/2)
Behavioural rules: B ⊆ C ∗ × V × E
Process if conditional statements such that every if sets
the value of only one state variable.
From every if statement, create a tree of preconditions
and expressions of the next values (missing branches
represent no change of the variable value: v 0 = v ).
Example
if c1 then
v := e1;
else
if c2 then
v := e2;
end if;
end if;
v0 =
c1
@1
0
@
c2
0 @1
e1
c1 → v := e1
¬c1 , c2 → v := e2
¬c1 , ¬c2 → v := v
@
v
Smrčka, Vojnar (FIT BUT, CZ)
e2
Hardware Design → Counter Automaton
Model :: Environment
For model checking, we need to model the environment too.
Environment = input signals of a component. Behaviour of the
environment can be completely random representation of an
input:
ε → v := random ∈ B for v ∈ V representing input signal.
Smrčka, Vojnar (FIT BUT, CZ)
Hardware Design → Counter Automaton
Model → Counter Automaton
InterBM
RTL design
InterBM:
Counter automaton:
counter
automaton
M = (V , T , B)
↓
A = (X , Q, q0 , ϕ0 , δ)
the set of counters X = {v | v ∈ V , T (v ) = int}
the control locations Q = {0, 1}Vq - set of all possible
evaluations of boolean variables
Vq = {v | v ∈ V , T (v ) = bool}.
initial state q0 , ϕ0 : one must provide an additional input of
the verification process (or can be guided by heuristics)
the transition relation δ ⊆ Q × Φ(X ) × Q: (cont.)
Smrčka, Vojnar (FIT BUT, CZ)
Hardware Design → Counter Automaton
Model → CA :: Transition Relation
δ := {}
for q1 , q2 in Q do
actions := {}
for (b : c → v := e) in B do
if c q1 ,q2 6= 0 then
actions := actions ∪ {(c q1 ,q2 , v 0 = eq1 ,q2 )}
δ := δ ∪ transitions(q1 , actions, q2 )
1
2
3
4
5
6
7
q
00
q2
? (line 5) line 7
01
x=0
y=0
x’=0
y’=1
1
c1 ∧ c2 ∧ a1 ∧ a2
00
c1 ∧ ¬c2 ∧ a1
01
¬c1 ∧ c2 ∧ a2
lines 3-6
actions = {(c1q1 ,q2 , a1 ), (c2q1 ,q2 , a2 )}
Smrčka, Vojnar (FIT BUT, CZ)
Hardware Design → Counter Automaton
Formal Verification :: Set of Bad States
Only safety properties are taken into account → specification of
bad state(s):
1
One defines the propositional formula over component
signals defining the bad state – ebad
2
A control location qbad ∈ Q representing the bad states is
created
3
From every control location, create a transition to qbad if
there is possible true evaluation of ebad
for q in Q do
q
6= 0 then
if ebad
q
δ := δ ∪ {(q, ebad
, qbad )}
Smrčka, Vojnar (FIT BUT, CZ)
Hardware Design → Counter Automaton
Transformation :: Summary
Counter automaton A = hX , Q, q0 , ϕ0 , δi
1
2
Divide variables to 1-bit variables
and multiple-bit ones (X )
Extract the behaviour from the
VHDL source code
1
2
3
Visualisation
Create the set of control
locations (Q)
Create the transition relation (δ)
Specification of the initial state
and the initial evaluation
Evaluation of 1-bit variables
represents the initial location
(q0 )
4
Create the bad state and the
transitions to that state
Smrčka, Vojnar (FIT BUT, CZ)
Hardware Design → Counter Automaton
Transformation :: Summary
Counter automaton A = hX , Q, q0 , ϕ0 , δi
1
2
Divide variables to 1-bit variables
and multiple-bit ones (X )
Extract the behaviour from the
VHDL source code
1
2
3
Create the set of control
locations (Q)
Create the transition relation (δ)
Specification of the initial state
and the initial evaluation
Evaluation of 1-bit variables
represents the initial location
(q0 )
4
Visualisation
Create the bad state and the
transitions to that state
Smrčka, Vojnar (FIT BUT, CZ)
Hardware Design → Counter Automaton
Transformation :: Summary
Counter automaton A = hX , Q, q0 , ϕ0 , δi
1
2
Divide variables to 1-bit variables
and multiple-bit ones (X )
Extract the behaviour from the
VHDL source code
1
2
3
Create the set of control
locations (Q)
Create the transition relation (δ)
Specification of the initial state
and the initial evaluation
Evaluation of 1-bit variables
represents the initial location
(q0 )
4
Visualisation
Create the bad state and the
transitions to that state
Smrčka, Vojnar (FIT BUT, CZ)
Hardware Design → Counter Automaton
Transformation :: Summary
Counter automaton A = hX , Q, q0 , ϕ0 , δi
1
2
Divide variables to 1-bit variables
and multiple-bit ones (X )
Extract the behaviour from the
VHDL source code
1
2
3
Create the set of control
locations (Q)
Create the transition relation (δ)
Specification of the initial state
and the initial evaluation
Evaluation of 1-bit variables
represents the initial location
(q0 )
4
Visualisation
ϕ0 XX
XX
Create the bad state and the
transitions to that state
Smrčka, Vojnar (FIT BUT, CZ)
Hardware Design → Counter Automaton
Transformation :: Summary
Counter automaton A = hX , Q, q0 , ϕ0 , δi
1
2
Divide variables to 1-bit variables
and multiple-bit ones (X )
Extract the behaviour from the
VHDL source code
1
2
3
Create the set of control
locations (Q)
Create the transition relation (δ)
Specification of the initial state
and the initial evaluation
Evaluation of 1-bit variables
represents the initial location
(q0 )
4
Visualisation
ϕ0 Z
XX
Z
XX
Z
PP Z PPZ
P
Create the bad state and the
transitions to that state
Smrčka, Vojnar (FIT BUT, CZ)
Hardware Design → Counter Automaton
Formal Verification :: Experiments
Pentium4 2.8Ghz, 512MB, Python interpreter for translator.
Component
Counter
Register
SynLIFO
AsFIFO (Status)
AsFIFO (FE)
|Q|
5
9
65
65
65
|δ|
13
45
985
5484
5075
|X |
1
1
1
11
11
Trans.
< 1s
1s
1m13s
3m51s
3m31s
ARMC [1]
< 1s
< 1s
2.7s
26m58s
1h17m
Safety properties like:
bad = ¬RESET ∧ CLK ∧ EN ∧ (OUT 6= DATA)
[1] A. Podelski, A. Rybalchenko. ARMC: The Logical Choice for
Software Model Checking with Abstraction Refinement. PADL 2007.
Smrčka, Vojnar (FIT BUT, CZ)
Hardware Design → Counter Automaton
Conclusions
We have proposed the method of FV of parametrised HW
components through the counter automata.
Future work/ideas:
Reduction of a size of generated automaton
Allow bit-wise operations on integers (often used in HW
design)
Experiments with more components and more tools
Smrčka, Vojnar (FIT BUT, CZ)
Hardware Design → Counter Automaton
Model :: Appendix A
ε → v := v
ε → v := ¬v
For a simpler construction of CA from InterBM,
if T (v ) = bool:
c → v := e
=⇒
c, v 0 = e → v := e
Environment: In the case of T (v ) = bool:
ebad : using references to current variable values (with no
v 0 , ↑v , or ↓v reference)
Example of Behavioural rules
res0
¬res , ↑clk , (addr 6= max − 1)
¬res0 , ↑clk , (addr = max − 1)
¬res0 , ¬↑clk
0
Smrčka, Vojnar (FIT BUT, CZ)
→
→
→
→
addr
addr
addr
addr
:= 0
:= addr + 1
:= 0
:= addr
Hardware Design → Counter Automaton
Model :: Appendix B
Behavioural rules: B ⊆ C ∗ × V × E
1
2
Transparent × synchronous mode: For the path from root
to leaf: If there is no ↑v (transparent mode): all variable
references point to their future values. If there is ↑v
(synchronous mode): all variable references in expressions
of subsequent nodes point to their current values
Transform such a tree to the set of behavioural rules
Example
if c1 then
v := e1;
else
if c2 then
v := e2;
end if;
end if;
v0 =
c1
@1
0
@
c2
0 @1
e1
c1 → v := e1
¬c1 , c2 → v := e2
¬c1 , ¬c2 → v := v
@
v
Smrčka, Vojnar (FIT BUT, CZ)
e2
Hardware Design → Counter Automaton