MASARYK UNIVERSITY B R N O

FACULTY OF INFORMATICS

Formal Verification
of Hardware Design

MASTER THESIS

Tomáš Kratochvíla

Brno, M a y 2005
Declaration

Hereby I declare, that this paper is my original authorial work, which I have worked out by
my own. All sources, references and literature used or excerpted during elaboration of this
work are properly cited and listed in complete reference to the due source.

Advisor: Mgr. David Šafránek

11
Thanks

I am very thankful to my adviser, David Šafránek, for his great help with my awful English.
Thanks are also due to all members of our ParaDiSe laboratory staff.
Abstract

The thesis presents an approach of using a formal verification method, the model checking,
to verify whether a particular component of hardware design matches its specification. We
have applied this approach in the Liberouter project, which is aimed to develop an FPGA
based high-speed router. The thesis is focused on formal verification of selected components
and its results.

IV
Keywords

formal verification, model checking, Cadence SMV, Liberouter, SMV language, Verilog HDL,
VHDL, XML

v
Contents

1 Introduction 2
1.1 Structure of the Thesis 3
2 Formal Verification 4
2.1 Temporal Logics 4
2.2 Model Checking 6
2.2.1 Use of Model Checking 7
2.3 Liberouter Project
2.4 Cadence SMV 8
2.5 Translation from VHDL to SMV Language 8
2.5.1 Empty modules 9
3 FIFO BRAM Component 10
3.1 Specifícation 10
3.2 Abstraction 11
3.3 Modelled Environment 12
3.4 Verified Properties 12
3.4.1 Generic Properties 12
3.4.2 Specific Properties 14
3.5 Evolution of the Component 15
3.5.1 Earliest Versions 15
3.5.2 Wrong Block Size 17
3.5.3 Delayed Clock 18
4 Other Components 19
4.1 Edit Engine 20
4.1.1 DRAM Communication Unit 20
4.2 Payload Checker 22
4.3 Sampling Unit 22
4.3.1 Mutual Exclusion of Flags 24
4.3.2 Write Mutual Exclusion 24
4.3.3 Mutual Exclusion of Control Signals 24
4.4 General notes 25
5 Verification Reports 27
5.1 XML structure 27
5.2 Additional Processing 29
6 Conclusion 30
A Different Assertion Approaches 31
B Verification Report DTD 33
C XSLT transformation from XML to XHTML 35
Bibliography 42

1
Chapter 1

Introduction

To maximize efficiency of hardware development process it is necessary to detect the most of

errors in the design as soon as possible. In addition to classical simulation and testing meth-
ods, which detects presence of bugs rather than guaranteeing their absence, we successfully
use the state-of-the-art automatic formal verification methods. There are three main formal
verification methods: equivalence checking, theorem proving, and model checking. Equiva-
lence checking method decides whether system is equivalent to its specification with respect
to some notion of behavioural equivalence. The main problem is absence of detailed speci-
fication. Theorem proving is a technique where both the system and its desired properties
are expressed as formulas in some mathematical logic. Afterwards, theorem proving con-
tinues by finding a proof of the properties. Unfortunately, this process is not yet been fully
automatized.
We use the model checking method [CGP99]. Model checking is a method for deciding
whether a given system satisfies its specification or not. Instead of simulation and testing
methods model checking takes into account all the possible behaviour of the design. The
other advantages of this technique are simple reusability in newer versions of the design
and counterexample generation showing wrong behaviour which helps to fix bugs in the
design. With respect to the nature of hardware systems design, we have chosen a tool based
on the symbolic model checking algorithms
The essential prerequisite of the model checking technique is formal specification of ver-
ified properties. For this purpose, suitable temporal logics are used [Eme90]. These logics
allow us to express all the typical requirements on the component behaviour. An example of
such a requirement can be that every request for writing will be eventually acknowledged.
Unfortunately, a nontrivial effort is required to use model checking tools to verify such
requirements on a very complex design. A lot of expert work has to be done manually to
suitably simplify the design - sophisticated abstractions have to be employed. For this rea-
son, model checking is not yet the standard method of verification in projects of this kind.
By contrast, in projects which use formal methods the percentage of bugs found by model
checking increases at the expense of bugs found by simulation and testing methods.
This thesis describes our approach of utilizing the model checking method to verify se-
lected components of a particular hardware design. Especially, we focus on FIFO compo-
nent - the process of its verification, detected errors, and the way of their correction. More-
over, the important facts of specification of three other components are formally checked
and the results are described. The components make a part of an FPGA-based PCI card

2
 1.1. STRUCTURE OF THE THESIS

developed in the Liberouter project. The main aim of the Liberouter project is to develop
a high-performance PC-based router with entirely open-source hardware and software de-
sign [AFN03].

1.1 Structure of the Thesis

The rest of the thesis is structured as follows. In Chapter 2, "Formal Verification", tempo-
ral logics and a model checking are defined and the model checking tool appropriate for
Liberouter project is presented. In the next Chapter 3, "FIFO BRAM Component", the spec-
ification, modelling details, and detected errors of the FIFO component are described. In
the Chapter 4, "Other Components", verification of three other components is described.
Finally, the Chapter 5, "Verification Reports", suggests the way of reusing the verification
framework each time the new version of the component is developed and presents the sys-
tem of verification reports.

3
Chapter 2

Formal Verification

The principal verification methods for hardware systems are simulation, testing, and formal
verification. Simulation and testing both involve making experiments before deploying the
system in the field. While simulation is performed on a hardware system design, testing
is performed on its implementation. These methods are commonly used as a cost-effective
way to find many errors. However, checking all the possible behaviour of hardware systems
using simulation and testing methods is rarely possible [CGP99].
We use formal verification, particularly model checking to check whether hardware sys-
tem satisfies a given property. In contrast to simulation and testing method, model checking
allows checking the behaviour of system for all the possible input. We aim to support hard-
ware designers in creating clear and correct systems with guaranteed behaviour.
Companies like Cadence Design Systems, IBM, Mentor Graphics develop tools support-
ing so called functional verification which targets the same goals. They use the Assertion-
Based Verification (ABV) approach for early detection of bugs in the hardware design. In
our approach it is also possible to write assertions in hardware design source codes, but we
found this method difficult for most hardware developers. Nevertheless, hundreds of asser-
tions are included in Liberourer hardware design source codes. The comparison of assertion
languages can be found in Appendix A.
The following section shows how formal specification can be represented in the form of
temporal logic formulas and in the next section the model checking method will be briefly
mentioned.

2.1 Temporal Logics

Formal specification consists of one or more properties which can be encoded as formulas
of LTL (Linear Temporal Logic) or CTL (Computational Tree Logic) [Eme90]. We begin with
describing the temporal logic CTL*, which can express both linear time (LTL) and branching
time (CTL) properties. In this logic, a path quantifier, either A (for all computation paths)
or E (for some computation paths) can prefix an assertion composed of arbitrary combi-
nations of the usual linear-time operators G (always), F (sometimes), X (next time), and U
(until). Both Linear Temporal Logic LTL and Computation Tree Logic CTL are included in
CTL* [CGH94].
There are two types of formulas in CTL*: state formulas (which are true in a specific
state) and path formulas (which are true along a specific path). Let AP be the set of atomic

4
 2.1. TEMPORAL LOGICS

propositions. The syntax of state formulas is given by the following rules:

• If p G AP then p is a state formula.

• If / and g are state formulas, then ->/ , / A g , and / V g are state formulas.

• If / is a path formula, then E / and A / are state formulas.

Two additional rules are needed to specify the syntax of path formulas:

• If / is a state formula, then / is also a path formula.

• If / and g are path formulas, then -if, ff\g,f\/g,Xf,Gf,Yf,f\]g, and / R g are

path formulas.

CTL* is the set of state formulas generated by the above rules.

The semantics of CTL* with respect to a finite-state concurrent system represented for-
mally as a kind of state transition graph called a Kripke structure. The Kripke structure is a
triple (S, R, L), where S is the set of states; R C S x S is the transition relation, which must
be total; and L : S —> 2AP is a function that labels each state with a set of atomic propositions
being true in that state. A path in (S, R, L) is an infinite sequence of states, IT = so, s i , . . . such
that for every i > 0, («j, Si+i) G R.
To denote the suífíx of a path TT starting at Si the symbol IT1 is used. If / is a state formula,
the notation M, s \= f means that / holds at state s in the Kripke structure M. Similarly, if
g is a path formula, the notation M, ir \= g means that g holds along path ir in the Kripke
structure M. When the Kripke structure M is clear from the context, we will usually omit
it. Assuming that f i are state formulas and gi are path formulas, the relation |= is defined
inductively as follows:

1. M, s \=p<^p G L(s).

2. M,s\=^h<*M,s)£h.
3. M, s\=hVh& (M, s |= h) V (M, s |= h).

4. M, « h / i A / 2 « (M, s |= h) A (M, s |= / 2 ) .

5. M, s |= E g\ <^ there is a path TT from s such that M, TT \= g\.

6. M, s |= A g\ <^ for every path TT starting from s, M, TT \= g\.

7. M, Tľ |= / i 4^ s is the first state of n and M, s |= f\.

8. M,7T | = ^ l ^ M , 7 T ^ 5 i .

9. M, TT |= 51 V g2 «• (M, 7T |= 5 i ) V (M, 7T |= 0 2 ).

10. M , 7 r | = 5 i A 5 2 ^ ( M , 7 r | = 5 i ) A(M,vr | = 5 2 ) .

5
 2.2. MODEL CHECKING

11. M,TT 1

1 F g\ 4^ there exists a Ä; > 0 such that M, TTk |= g\.

12. M,TT |=

13. M, TT\=Ggi^
1 for all i>0,M, TT1 |= #I

14. M, TT|=1gi U #2 ^ 3fc > 0 such that M, TTU |= g2 and for all 0 < j < k, M, TTJ \= g\.

15. M, TT 1g\ R (j2 ^ for all j > 0 , if for every í < j , M, TT% \/= g\ than M,•3 TT
I— 92 •

Computation Tree Logic (CTL) is a restricted subset of CTL* in which each of the tempo-
ral operators X, F, G, U, and R must be immediately preceded by a path quantifier.
Linear Temporal Logic (LTL), on the other hand, consists of formulas which have a form
A / where / is a path formula in which the only state subformulas permitted are atomic
propositions.

2.2 Model Checking

Model checking is formal verification method for automatic verifying finite-state and infinite-
state concurrent systems. Verification of infinite-state systems is not the subject of this thesis
because hardware systems have finite-state nature. The procedure normally uses an exhaus-
tive search of the state space of the system to determine if it satisfies the specification or not.
The model checking inputs and two possible outputs are depicted in Figure 2.1.

property in LTL/CTL model of a system

Model Cheking

~z v
Satisfied Not satisfied

Counterexample

Figure 2.1: The scheme of model checking

Moreover, given sufficient resources, the procedure will always terminate with an an-
swer whether the system satisfies the property or not [CGP99].
The model checking problem for a given Kripke structure (S, R, L) that represents a
finite-state concurrent system and a temporal logic formula / expressing some desired spec-
ification, is to find the set of all states in S that satisfy / , formally, {s G S \ M, s \= / } .

6
 2.3. LIBEROUTER PROJECT

Normally, some states of the concurrent system are designated as initial states. The system
satisfies the specification provided that all of the initial states are in this set.
The early algorithms for solving the model checking problem used an explicit represen-
tation of the Kripke structure in the form of a labelled, directed graph with arcs given by
pointers. In that representation, the nodes stands for the states in S, the arcs in the graph
give the transition relation R and labels associated with the nodes describe the function
L : S —>• 2AP. The problem of this so called explicit model checking is that in a hardware
system, the number of states in the global state transition graph may rise exponentially
with the number of concurrently executing components. Hence the size of the state space
is usually too large to be tractable. This problem is referred as the state space explosion
problem [BCM+90].
Therefore, the symbolic method of the state space representation is used. The symbolic
model checking algorithm is based on the manipulation of Boolean formulas using Ordered
Binary Decision Diagrams (OBDD) [Bry86]. The algorithms for solving the model checking
problem are in detail described in [CGP99].

2.2.1 Use of Model Checking

Typically, it is difficult to find some bugs in the design but it is an essential task. Rarely
incident bugs are almost undetectable by classic simulation or testing methods, but they can
be detected by model checking. On the one hand, when a property is proved to be false,
model checking returns an example of behaviour of the system in which the property is
violated, so called counterexample. On the other hand, when model checking for a given
property returns true, the property is satisfied by all the possible behaviour of the system.
In general, it is thought that it is possible to formally verify some system and guarantee
its correctness. The reality is that it is impossible to find all the possible errors in the system.
In other words, model checking cannot guarantee that the design is completely correct, but
it can only guarantee that some explicitly given properties are satisfied.

2.3 Liberouter Project

Liberouter project aims at developing a high-speed router with entirely open design [1 ].
Performance is reached by processing most of the IPv6 and IPv4 network traffic in hardware.
The router is based on Field-Programmable Gate Array (FPGA) technology [AFN03].
The hardware design source codes are written mainly in general-purpose VHSIC Hard-
ware Description Language (VHDL) [IEEE93]. The VHDL language was chosen because of
its support for universality and hierarchy instead of the competitive language Verilog Hard-
ware Description Language (VerilogHDL) [IEEE95].
Unfortunately, as VHDL is not an input language of any model checker available to us
at this moment, we have to translate VHDL to some model checker input language. More-
over, the sufficiently large subset of VHDL needs to be translated. The Cadence SMV model
checking tool brings the solution of this problem as it is described in next section.

7
 2.4. CADENCE SMV

2.4 Cadence SMV

The Cadence SMV model checker [McM] comes equipped with two modelling languages,
extended SMV and synchronous Verilog HDL. In the SMV language the hierarchical finite-
state concurrent systems could be described. The Cadence SMV allows several forms of
property specification, including the temporal logics CTL and LTL, finite automata, embed­
ded assertions, and refinement specifications. It also includes a graphical user interface and
source level debugging capabilities. The acronym SMV stands for Symbolic Model Verifier.
The Cadence SMV extracts a transition system represented as an OBDD from a program
in the SMV language and uses an OBDD-based state space search algorithm to determine
whether the system satisfies its specification. If the system does not satisfy the given spec­
ification, the model checker produces an execution trace which shows the reason why the
specification has been proved to be false [CGP99].

2.5 Translation from VHDL to S M V Language

Input for the verification is taken from the source codes of the design components written
in VHDL. These source codes are then automatically translated into the input language of
the Cadence SMV model checker. Using the Mentor Graphics LeonardoSpectrum or Preci­
sion tools [Men], VHDL source codes are synthesized into the Verilog HDL. The Cadence
SMV includes translator of Verilog HDL source codes into its native SMV language. In
essence, Verilog HDL and SMV languages are syntactically very similar. The scheme of the
translation process is depicted in Figure 2.2 and more detailed information can be found
in [HKR+04].

Cadence SMV script,

vl2smv
S M V language
Verilog HDL module DFFRS (set, reset, in,
VHDL module DFFRS (set, reset, in, elk, out)
input set : boolean resolve;
input reset: boolean resolve;
input set, reset, in, elk; output out; input in : boolean resolve;
library ieee; reg out;
use ieee.std_logic_1164.all; input elk : boolean resolve;
always 0 (posedge set or reset or elk) output out : boolean resolve;
entity D_FF_RS is begin
port {D, Clock, Reset, Set :in std_ulogic; do { if (set) init(out) := 1;
if (set) out = 1; else if (reset) init(out) := 0 ]
Q :out std_ulogic); else if (reset) out = 0;
end entity D_FF_RS; do í if (next(set)) next(out) 1;
else begin out = in; end else if (next(reset)) next(out)
end else if (~clk & next(elk)) next(out)
arichitecture behavioural of D_FF_RS is end
begin I
endmodule
pO: process (Clock, Reset, Set) is
begin
if (Ser = '0') then Q <= ' ľ ;
elsif (Reset = '0') then Q <= '0';
elsif (Clock = •1* and Clock"event) then Q <=
end if;
end process pO;
end architecture behavioural;

Figure 2.2: Translation from VHDL to SMV language

Both VHDL and Verilog HDL are very complex languages and the translation on their
high level is possible only in trivial cases. We have to use low level source codes because
Cadence SMV model checker does not accept complete Verilog HDL. Therefore, we have to
synthesize VHDL to low level Verilog HDL. After the synthesis, some signals are renamed

8
 2.5. TRANSLATION FROM VHDL TO SMV LANGUAGE

or even dismissed during optimalization process. This problem can be suppressed using
- h i e r a r c h y p r e s e r v e and some other specific options during synthesis. Further, the
important option is -downto PRIMITIVES which forces synthesiser to write down also
the behavioural descriptions of basic entities from the library P r i m i t i v e s (e. g. LATRS,
DFFRS, GND). After all our effort some other refinements have to be employed, for more
details see [KRS03].
In general, we specify the properties of verified components using the SMV language.
The properties are taken mostly from the specification of the component behaviour. Other
properties are given by VHDL designers - either verbal descriptions or assertions written
as comments in VHDL source codes. For VHDL designers which want to write assertions
as comments in VHDL source codes we have written the Verification Cookbook [Kra03].
Verification Cookbook contains the description of the method of writing properties in easier
form than the full LTL or CTL.
Once we have obtained an SMV source code, its verification can be performed. Results
of the verification are then reported to developers in the form of verification reports. More
details on such reports will be given in Chapter 5, "Verification Reports". In the next chapter,
formal verification of a particular FIFO component will be presented.

2.5.1 Empty modules

Since LeonardoSpectrum and Precision software are not capable to synthesise full Verilog
HDL, the translation process may hence produce empty modules. Empty modules have
correctly defined interface but there is no logic inside them. Every possible output of an
empty module is taken into account in the model checking tool. Empty modules are mainly
modules representing some kind of RAM memory which is in most cases acceptable. The
reason is that saving the state space of memory modules in the physical memory is unfea-
sible and the properties are typically not involved on these modules. Unfortunately, also
some other modules remain empty after the translation. These are typically latch register
modules. However, those empty modules have to be manually modelled. After the transla-
tion, we use automatic substitutions to replace the important empty modules with their full
versions [KRS03].
When the state space of verified system is larger than available physical memory, making
some module empty can be helpful abstraction. Such an abstraction is correct when the
result of verified property does not depend on functionality of that module. Sometimes, it is
even better when the property is satisfied for every output of the empty module rather than
only for outputs generated by the full version of that module. More particularly, the change
of implementation of that module cannot violate the property. In contrary, if the property
referring a particular output signal of some empty module is not satisfied then it might be
satisfied in the full version of that module.
There are many ways of fighting with state space explosion problem but the way men-
tioned above may affect the result of formal verification. Therefore, all changes from the
original VHDL source codes have to be specified in verification results.

9
Chapter 3

FIFO BRAM Component

Data buffering and queuing are common challenges in high-speed network systems. FIFOs
are commonly used to connect components to increase the overall performance. This chapter
shows the verification of a particular design component, FIFO BRAM, with respect to its
specification.
The presented results on FIFO BRAM verification have been also submitted to FPL 2005
conference [KRS05].

3.1 Specification

The FIFO BRAM component implements a FIFO queue using internal Virtex™-II block RAM
memories [Xil05]. The size of the FIFO is parameterized by the generic parameter ITEMS.
Items in the FIFO are divided into blocks and the component allows detection of the sit-
uation when only the last free block of the FIFO is available. The number of items in one
block is set by the BLOCKSIZE constant. For details, see the documentation of the LSTBLK
component [Mar].
The component is shown as a black box with input and output ports in Figure 3.1.

> CLK
RESET

WR FULL
DI LSTBLK

RD DV
DO EMPTY

Figure 3.1: FIFO BRAM component

There are the following four regular input ports in the component interface:

• CLK is a port of the Clock signal

10
 3.2. ABSTRACTION

• RESET is a port of the Reset signal

• WR is the Write Request port

• RD is the Read Request port

The data ports of the component are the following:
• DO is 16bit data output port

• DI is 16bit data input port

And the output ports are defined below:
• EMPTY transmits the signal which is active if and only if the FIFO is empty.

• FULL transmits the signal which is active if and only if the FIFO is full.

• LSTBLK transmits the last block detection signal which is active if and only if the FIFO
contains just BLOCKS IZE or less than BLOCKS IZE number of free items.

• DV transmits the data valid signal which is active as soon as the valid output data are
available on the DO port.

3.2 Abstraction

With respect to the size of the address space, we have verified smaller versions of the
FIFO BRAM component than is the version described in the Liberouter CVS [ ] directory
l i b e r o u t e r / v h d l _ d e s i g n / u n i t s / c o m m o n / f i f o_bram/. In this subsection we would
like to mention the reasons for such an abstraction.
In earliest versions, the 5bit long address of each block RAM was considered instead of
the original lObit long address. This fact implied the upper limit of 31 items for each BRAM.
The reason for this abstraction was that the state space of the full version of FIFO BRAM
would be too large.
The main purpose of such an abstraction was to decrease the size of the component. The
functionality of the component has not been changed, and hence the abstraction was correct.
All changes are very carefully considered and documented in our verification reports. The
size of components is often parameterized and the output of the verification is some subset
of possible parameter values for which the property is satisfied.
In actual versions, the FIFO BRAM component is also parameterized. It has four generic
parameters (ITEMS, BLOCK.SIZE, BRAM_TYPE, and DATA_WIDTH). We have verified VHDL
codes for each purposeful combination of these parameters. To save our computational re-
sources while covering almost all the hardware designer needs, we have considered the
ITEMS parameter restricted. The restricted ITEMS parameter puts a limit to other param-
eters. This limitation is necessary because the verification process cannot be executed for
infinitely many values of the parameters.

11
 3.3. MODELLED ENVIRONMENT

Most importantly, all the parameters used in every implementation of FIFO BRAM com-
ponent in Liberouter project are verified firstly.

3.3 Modelled Environment

To verify the component, a process which represents behaviour of the component environ-
ment has to be modelled. An environment process was modelled using the SMV language.
The main function of the environment process is generation of all possible component in-
puts. In our verification we focus mainly on the values of the control signals EMPTY, FULL,
and LSTBLK. To enable checking of these signals behaviour, the environment contains the
variable c o u n t e r which saves the actual number of items in the FIFO. Moreover, the envi-
ronment process is able to detect when the FIFO items are being read or written.
Two registers, MINUS and PLUS, have been defined to manage the value of c o u n t e r .
The MINUS register is defined to become active just after the moment in which an item has
been successfully read from the FIFO. This situation is emerged when the signal RD is active
and the EMPTY signal is not active. Similarly, the PLUS register is defined to become active
when an item has been successfully written to the FIFO. This situation corresponds to the
behaviour of the WD and FULL signals.

3.4 Verified Properties

In this section, the properties of the FIFO, which we have verified, are described. Each prop-
erty is presented here as a natural language sentence followed with its formalization in the
form of CTL or LTL formula.
We categorize the verified properties into two groups - generic properties and specific
properties. The generic properties are general requirements on the FIFO behaviour. The spe-
cific properties are derived from the component specification.

3.4.1 Generic Properties

Some common properties are applicable to any FIFO equipped with FULL and EMPTY sig-
nals and with the c o u n t e r of items.
The generic properties we have considered are the following:
• The FIFO is always eventually full:
AG EF ( counter = ITEMS )

• The FIFO is always eventually empty:

AG EF ( c o u n t e r = 0 )

• The FIFO is full if and only if the FULL signal is active:

AG( ( f u l l <-> c o u n t e r = ITEMS ))

12
 3.4. VERIFIED PROPERTIES

The FIFO is empty if and only if the EMPTY signal is active:

AG( ( empty <-> c o u n t e r = 0 ))

The c o u n t e r does not overflow:

AG( ( counter ITEMS 1 ))

The c o u n t e r does not underflow:

AG( ! ( c o u n t e r = - 1 ))

It is not possible to read from and write to the same address at the same time:
AG( ( MINUS & PLUS
& fifo.reg_write_ addr_0_ = fifo.reg_read_addr_0_
& fifo.reg_write_ addr_l_ = fifo.reg_read_addr_l_
& fifo.reg_write_ addr_2_ = fifo.reg_read_addr_2_
& fifo.reg_write_ addr_3_ = fifo.reg_read_addr_3_
#if ITEMS < 33
fifo.reg_write_addr_4_ fifo.reg_read_addr_4_
#elif ITEMS < 65
& ( fifo.reg_write_ addr_4_ = fifo.reg_read_addr_4_
& ( fifo.reg_write_ addr_5_ = fifo.reg_read_addr_5_
#elif ITEMS < 129
& fifo.reg_write_ addr_4_ = fifo.reg_read_addr_4_
& fifo.reg_write_ addr_5_ = fifo.reg_read_addr_5_
& fifo.reg_write_ addr_6_ = fifo.reg_read_addr_6_
#elif ITEMS < 257
& fifo.reg_write_ addr_4_ = fifo.reg_read_addr_4_
& fifo.reg_write_ addr_5_ = fifo.reg_read_addr_5_
& fifo.reg_write_ addr_6_ = fifo.reg_read_addr_6_
& fifo.reg_write_ addr_7_ = fifo.reg_read_addr_7_
#elif ITEMS < 513
& fifo.reg_write_ addr_4_ = fifo.reg_read_addr_4_
& fifo.reg_write_ addr_5_ = fifo.reg_read_addr_5_
& fifo.reg_write_ addr_6_ = fifo.reg_read_addr_6_
& fifo.reg_write_ addr_7_ = fifo.reg_read_addr_7_
& fifo.reg_write_ addr_8_ = fifo.reg_read_addr_8_
#elif ITEMS < 1025
& fifo.reg_write_ addr_4_ = fifo.reg_read_addr_4_
& fifo.reg_write_ addr_5_ = fifo.reg_read_addr_5_
& fifo.reg_write_ addr_6_ = fifo.reg_read_addr_6_
& fifo.reg_write_ addr_7_ = fifo.reg_read_addr_7_
& fifo.reg_write_ addr_8_ = fifo.reg_read_addr_8_
& fifo.reg_write_ addr_9_ = fifo.reg_read_addr_9_
#elif ITEMS < 2049
& ( fifo.reg_write_ addr_4_ = fifo.reg_read_addr_4_
& ( fifo.reg_write_ addr_5_ = fifo.reg_read_addr_5_
& ( fifo.reg_write_ addr_6_ = fifo.reg_read_addr_6_

13
 3.4. VERIFIED PROPERTIES

& ( fifo.reg_write_addr_7_ fifo.reg_read_addr_7_ )

& ( fifo.reg_write_addr_8_ fifo.reg_read_addr_8_ )
& ( fifo.reg_write_addr_9_ fifo.reg_read_addr_9_ )
& ( fifo.reg_write_addr_10 fifo.reg_read_addr_10_ )
ttendif
) )

The last property is not satisfied only when the read and write addresses are the same
(the read registers of the form reg_write_addr_*_ equals to the write registers of the form
reg_read_addr_*_) and an item is read from and written to the FIFO at the same time
(which corresponds to the formula MINUS & PLUS). The last property is written to verify
FIFO components with ITEMS parameter up to 2048. These generic properties are used also
for verification of other FIFO components (e. g. [MP]). We have successfully verified that all
these generic properties hold in every version of the FIFO BRAM component.

3.4.2 Specific Properties

An important liveness property of the FIFO is that it should eventually reach the state, in
which the LSTBLK signal is active. To check whether the signal LSTBLK satisfies at least this
functionality the following property has to be employed:

• The LSTBLK signal is always eventually active:

AG EF ( LSTBLK )

This property was satisfied in every version of the FIFO BRAM component. The following
"last free block" property is taken from the specification (as it has been already stated in

The LSTBLK signal is asserted if and only if the FIFO contains BLOCK_SIZE or
less then BLOCK_SIZE free items.

This property should be more formally formulated as:

In every possible execution of the system, the number of free items in the FIFO
is less or equal than the size of a block if and only if the LSTBLK signal is active.

The number of free items in the FIFO is the value of the expression (ITEMS - c o u n t e r ) .
Then the corresponding formula in the CTL form is the following:

AG( ( (ITEMS - counter) <= BLOCK_SIZE ) <-> LSTBLK )

Using Cadence SMV it has been shown that this formula holds in the actual version of the
component. In the previous versions, its validity was violated. In the next section, the expla-
nation of what kind of errors were found and how they were corrected will be delivered.

14
 3.5. EVOLUTION OF THE COMPONENT

3.5 Evolution of the Component

In this section, the evolution of the FIFO BRAM component is presented. Moreover, we
show the consequences of the fact that the specification of this hardware component was
not originally implemented correctly.
In general, it is a harder task to achieve the required functionality in the hardware than
in the software. The main reason is that concurrency, speed, and sophisticated resource con-
sumption are very critical properties of such a hardware system. More particularly, it is
usually very difficult to instantly change the value of a simple signal such as LSTBLK before
the next clock tick comes.

3.5.1 Earliest Versions

The LSTBLK signal in the FIFO BRAM component could not be directly computed in the
hardware without a significant increase in resource consumption. In the earliest versions
of the component, the block referred by the read or write address register was being deter-
mined using the highest bits of the address. The LSTBLK signal was raised whenever the
read address was referring to the block placed just next to the block referred by the write
address (modulo the number of blocks). This FIFO implementation is illustrated on a simple
example which follows.
Assume, e.g., that BLOCK-SIZE = 4. In other words, we suppose the number of items
in one block to be set to 4. In this situation, when the number of free items in the FIFO is
lower than or equal to 4, the LSTBLK signal should be active according to the specification.
This example is illustrated in Figure 3.2.

block of items

X X X X X X X X X

write address I I read address

Figure 3.2: Read and write address registers refer to items in FIFO with blocks of size 4.

The part of the FIFO is shown there with the engaged items marked with X and the free
items represented as empty boxes. Read and write address registers are depicted as arrows
referring to the relevant items.
The implementation described above is simple and saves a lot of hardware resources.
But we have encountered an inaccuracy which has later turned to be a significant problem.
The LSTBLK signal was not being generated just when the last BLOCK-SIZE number of free
items was remaining in the FIFO. The intended behaviour was verified using the following
properties which restrict the interval when the LSTBLK signal should be raised.
The VHDL designers focused mainly to save the hardware resources at the expense of

15
 3.5. EVOLUTION OF THE COMPONENT

accuracy. They believed that the LSTBLK signal was raised when at most 2 * BLOCK_SIZE
and at least BLOCK-SIZE number of free items was remaining. The following two formulas
to verify the behaviour of the LSTBLK signal have been set up:

• (i) The LSTBLK signal is not active if the number of empty items is greater than the
size of two blocks.
AG( (ITEMS - counter) > (2 * BLOCK_SIZE)
-> "LSTBLK

(ii) The LSTBLK signal is active if the number of empty items is smaller than the size
of one block.
AG( (ITEMS - counter) < BLOCK_SIZE
-> LSTBLK

The formula (i) has been satisfied in every version of the FIFO BRAM component which
means that the LSTBLK is never active when there are more than two free blocks.
On the contrary, a critical error has been found using the formula (ii). This formula did
not hold in the earliest versions of the FIFO. More specifically, the LSTBLK signal turned to
zero when the number of empty items became smaller than the size of one block.

1\ 1\ i1
CLK

LSTBLK

FULL

read address < 1011 X 1011 \< 1011 \< 1011 \{ 1011 X 1011 \< 1011 X 1011 )<

»rite address < 0100 X 0101 \< 0110 \< 0111 \< 1000 X 1001 \< 1010 X 1011 )<

1 2 3

Figure 3.3: Timing diagram showing the wrong behaviour of the FIFO component.

16
 3.5. EVOLUTION OF THE COMPONENT

Only the signals LSTBLK, CLK, and FULL and the read and write address registers are
significant for the observed anomaly. The read address register refers to the same item all
the clock ticks while the write address register is increased with each rising CLK edge. The
content of the FIFO is observed in three different instants indicated in Figure 3.3.
In the first instant, the FIFO contains seven free items. At the same time, the highest bits
of the write address, incremented by one, equal to the highest bits of the read address, and
hence the LSTBLK signal is changed by the next rising CLK edge. In the next four clock ticks,
four items are written to the FIFO.
Subsequently, the second indicated instant comes. At this instant, the highest bits of the
write address equal to the highest bits of the read address. This makes the LSTBLK signal
to be changed to zero with the next rising CLK edge. This is the incorrect behaviour which
contradicts the formula (ii).
The last indicated instant is reached just after the next three items are written to the FIFO.
In that moment, the FULL signal is raised while the LSTBLK signal is still not active. Now
the FIFO is in the state in which, with respect to the LSTBLK signal, it is able to accept some
block of items, but in fact it cannot accept any.
A necessary precondition for correctness of this implementation is expressed by the fol-
lowing property:

• (Hi) The LSTBLK signal is active before the number of empty items is smaller than the
size of one block. The formula checks whether the FIFO can reach the state in which
less than one free block is available without the rising of LSTBLK signal. The operators
G, U, and | stand for globally, until, and or respectively.
( (ITEMS - counter) >= BLOCK_SIZE U LSTBLK )
I
G (ITEMS - counter) >= BLOCK_SIZE
The formula (Hi) has been satisfied in earliest versions. In further versions, the validity of
this formula has been violated as it is shown in the next subsection.

3.5.2 Wrong Block Size

The hardware designers have reimplemented the component. Unfortunately, the improve-
ment has been achieved at the expense of consumption of more hardware resources. In more
detail, the register c n t . d i f f, showing the difference between the read and write address
registers, has been added. Hence, in this register the number of free items is being stored.
The LSTBLK signal is controlled in the way very similar to the previous case - it is active
when the highest bits of the c n t _ d i f f register are equal to zero. When the implementation
was changed we verified the new VHDL sources using the same properties.
The last block formula (ii) was not satisfied again and, moreover, the last block formula
(Hi) was not satisfied in spite of that it had been satisfied before. The Cadence SMVtool gen-
erated the counterexample which showed that the behaviour of the new FIFO implementa-
tion corresponded to the case of the FIFO with the block size one item smaller. More par-

17
 3.5. EVOLUTION OF THE COMPONENT

ticularly, the highest bits were equal to zero when the c n t . d i f f register value was smaller
than or equal to 2 M , where k = log2 BLOCKS IZE.

3.5.3 Delayed Clock

During correction of the previously mentioned errors, another error was discovered by
model checking. The LSTBLK signal was not being set exactly at the instant when the last
free block was remaining but after the next rising CLK edge - the LSTBLK signal was being
generated after some delay. It has forced a change of the specification in which the informa-
tion about the LSTBLK signal has been now fixed just with respect to this delayed behaviour.
The following sentence has been added to the specification: "in current implementation, this
signal is one clock cycle delayed. "This note is necessary for designers who will use this FIFO
component as a black box in some other projects.
We reuse the established verification framework each time a change in source codes or in
the specification appears. This process is in most cases very easy and quick (it typically takes
minutes of manual work plus time spent on automatic computation). When the specification
is changed the corresponding properties have to be changed too. More precisely, in this case
all the formulas describing the last free block property were changed to handle the delayed
clock.

18
Chapter 4

Other Components

In this chapter, verification of three components, as highlighted in Figure 4.1, will be pre-
sented. Edit Engine component is a part of the main Liberouter project. Sampling Unit and
Payload Checker are components of Scampi project [ ]. The Scampi project aims to de-
velop a scalable monitoring platform for the Internet. The hardware part of the Scampi
project is supported by the Liberouter project team.

r
Unified Header FIFO Look up Processor Replicator ^ Priority Queue

I i
Header Field Extractor DRAM scheduler Edit Engine
>

Time Stamp Unit

mo«
FIFO Look up Processor -> Sort Unit SFIFO Statistic Unit

10 BUF Unified Header FIFO Sampling Unit Payload Checker

I
Header Field Extractor PFIFO _^ Dispatcher DRAM scheduler

Figure 4.1: Components of Liberouter and Scampi projects.

The components were selected with respect to hardware developer needs and priorities.

19
 4.1. EDIT ENGINE

We are able to translate entire projects (e.g. Scampi) to SMV language and also verify the
specific properties of such a complex system. (Synthesis of huge projects may take about
one hour of CPU time.) Unfortunately, the state space generated by Cadence SMV cannot
exceed 4 GB of physical memory (yet only 32-bit version is available). Therefore most of
inter-component properties cannot be verified without abstractions.
For most components and their specifications similar actions to employ formal verifica-
tion have to be done. Actions like finding corresponding signals of specification after trans-
lation VHDL codes into SMV language, setting of common preconditions on clocks or resets,
or abstracting from irrelevant modules will be described in the following sections.

4.1 Edit Engine

Edit Engine is a component of the Liberouter project which performs output packets pro-
cessing. Edit Engine is capable of changing L2 header, decrementation of Hop Limit (Time
To Live in IPv4), Routing Header processing, ICMPvó manipulation and encapsulation or
decapsulation of packet throw tunnel [Mar03].
The properties verified in Edit Engine would not be satisfied without the following pre-
condition that clock CLK is ticking:

G ( F (CLK) & F (!CLK) )

Without this limitation on the execution of the system the properties will not be satisfied
and the counterexample will be the infinite execution of the system where clock signals are
still on same level. Many signals are updated with the positive or negative clock edge and
hence the execution of the system without ticking clocks should be excluded.
The basic property we have considered is the read-write mutual exclusion of signals
p l x _ r d and plx_wr in LTL form:

G (! ( plx_wr & p l x _ r d ) )

This mutual exclusion was satisfied in every version of the design with the precondition on
the clock (verified in 0.66 seconds). Other properties relate to DRAM communication unit,
the part of Edit Engine, are described in the following subsection.

4.1.1 DRAM Communication Unit

DRAM communication unit is a part of Edit Engine and is responsible for data transfer from
DRAM memory. Communication with DRAM memory is supported by DRAM Scheduler
and data are transffered by 32 bytes large blocks.
Specification of the DRAM communication unit for Write Request Finite State Machine
(WR REQ FSM) is the following: When the DRAM communication unit obtains some of
DRAM_RD_REQ, DRAM_DEC_REQ or DRAM_WR_REQ r e q u e s t s i g n a l s a n d EN is n o t active, the
DRAM_A.CK acknowledge signal has to be active.

20
 4.1. EDIT ENGINE

G ( ((DRAM_RD_REQ | DRAM_DEC_REQ | DRAM_WR_REQ) & !EN)

->
DRAM_ACK )

This formula was satisfied in every version of Edit Engine with the precondition on the clock
(verified in 0.09 seconds).
Also other part of the DRAM communication unit specification was verified: When 11
highest bits of the input and output pointers (INP_PTR and OUT.PTR) differ, the i n p j n e q . o u t
signal of the DRAM communication unit has to be active in the next step. The corresponding
LTL formula should be the following:

G ( !(OUT_PTR = INP_PTR) -> X i n p _ n e q _ o u t )

Unfortunately, the INP_PTR and OUT.PTR pointers have been synthesized into single bits
of the form i n p _ c o u n t e r J i i g h _ * _ and OUT_PTR_int_*_. And then every single bit of the
input and output pointers has to be compared with respect to its significance. Moreover, the
inp_neq_out signal is updated only with the positive clock edge and during the time the
RESET signal may not be active (the RESET signal is active low.) This requisite on the RESET
signal can be also written as a precondition.
With these additional actualities the resulting LTL formula is:

G ( RESET & X RESET & !CLK & X CLK

->
(
!(
OUT_PTR_int_0_ + 2*OUT_PTR_int_l_ + 4*OUT_PTR_int_2_ +
8*OUT_PTR_int_3_ + 16*OUT_PTR_int_4_ + 3 2*OUT_PTR_int_5_ +
64*OUT_PTR_int_6_ + 12 8*OUT_PTR_int_7_ + 256*OUT_PTR_int_8_ +
512*OUT_PTR_int_9_ + 1024*OUT_PTR_int_10_

inp_counter_high_0_ + 2*inp_counter_high_l_ +
4*inp_counter_high_2_ + 8*inp_counter_high_3_ +
16*inp_counter_high_4_ + 32*inp_counter_high_5_ +
64*inp_counter_high_6_ + 12 8*inp_counter_high_7_ +
2 56*inp_counter_high_8_ + 512*inp_counter_high_9_ +
1024*inp_counter_high_10_
)
->
X inp_neq_out
)
)

This formula was satisfied in every version of Edit Engine with the precondition on the clock
(verified in 1.25 seconds).

21
 4.2. PAYLOAD CHECKER

4.2 Payload Checker

Payload checker is a component for Intrusion Detection System (IDS) using FPGA and
Ternary Content Address Memory (TCAM). FPGA is used only for data control and buffer-
ing. TCAM is used for fast pattern matching. Payload checker allows to search up to 512
patterns, each 16 bytes long. Patterns are shifted against the TCAM word, so more then
only one row is used to store one pattern. But it enables to achieve high performance up
to 3,2 Gbps. Patterns can be divided into 8 groups and matching can be performed in any
combination of those groups [PCK].
The property which hardware designers need to verify is: "When the valid data comes
to Payload Checker then Payload Checker signals VALID in future." The unmentioned pre-
condition in that Payload Checker has to be also ready (the READY signal has to be active).
Moreover, the RESET signal has to be activated first and in the future the RESET signal may
not be active. The formula corresponding to this property is:
G ( RESET
->
F ( !RESET & READY & INP_DATA_VLD & INP_EOP
->
F VALID )
) ;

This formula was satisfied and the verification took 2900 seconds and 2315 MB of memory.
During verification more than 75 millions of BDD nodes were allocated.
Since this property does not depend on functionality of lbconn_mem_983 04 0_12_notri
module which causes large increase of state space generated by model checker, it was con-
sidered as an empty module.
In order to see a progress of memory consumed by model checker the following graph
was created. Since Cadence SMV shows only total time consumed by verification and total
number of allocated BDD nodes, the external measurement of actual real memory consumed
during the verification time had to be employed. The graph representing the actual memory
consumed in time during verification of the last property is shown in Figure 4.2
Using the graph of resource consumption for a given parameters one can predict the
time and space consumed by verification for another parameters. Moreover, from shape of
complexity graph for given parameters the amount of memory consumed during time for
another parameters can be predicted.

4.3 Sampling Unit

The Scampi project contains 16 Sampling Units [Smo04]. Each can be configured to provide:

• probability sampling - the packet is passed through the unit with the probability 1/n,

• deterministic sampling - each n-th packet is passed through,

22
 4.3. SAMPLING UNIT

10000

1000

<Do 100
ro
o.
</>

10

1
1 10 100 1000 10000
time [s]

Figure 4.2: The graph shows resources consumed by verification of the Payload Checker
formula.

• byte deterministic sampling - packet containing each n-th byte is passed through.

The packet can be processed simultaneously in more than one Sampling Unit. If the
packet is not passed through any of these units, it is discarded. The required processing
of the packet is coded in the control word. First half of 32-bit control word is SAMASK -
Sampling Unit Assignment. Each Sampling Unit has one bit in this bit array and positive
value means that packet will be processed by corresponding Sampling Unit. The SAMASK
field is masked by the result of Sampling Unit processing. The positive value remains only
if the packet is passed through the corresponding Sampling Unit.
Special configuration of Sampling Unit is the case of deterministic sampling with n = 1.
This case represents the situation, when all specified packets are required to be passed to the
target application.
Properties obtained from hardware developers which Sampling Unit should satisfy are
the following:

• Mutual exclusion of flags (signals) c o n t r o l _ f l a g and data_f l a g .

23
 4.3. SAMPLING UNIT

• Write mutual exclusion of signals mode_wr and i n i t _ w r _ v e c .

• Mutual exclusion of four control signals CONTROLS, CONTROL_B, CONTROL_C, and

CONTROL_D.

4.3.1 Mutual Exclusion of Flags

First of all, both RESET and LRESET reset signals may not be active. The signals c o n t r o l - f l a g
and data_f l a g from SALLINSjiotrimodule have been synthesized into negative signals
NOT_control_f l a g and NOT_data_f l a g . Hence, mutual exclusion of c o n t r o l - f l a g and
d a t a . f l a g is formulated in the following way:
G! ( ! SAU_INS_notri.RESET &
! LRESET &
SAU_INS_notri.NOT_control_flag &
SAU_INS_notri.NOT_data_flag )

Many similar versions of this formula have been verified to find all the dependencies be-
tween signals. In addition, it was analyzed which of preconditions are necessary and which
other signals are influenced.

4.3.2 Write Mutual Exclusion

Mutual exclusion of the write signal mode_wr and the write vector i n i t _ w r _ v e c was the
next challenge. Since the signal mode_wr was synthesized to signal nx72 and the vector
i n i t _ w r _ v e c was synthesized to signals nx57, nx58,... n x 7 1 , and nx73 the resulting for-
mula is quite compact:
G ! ( SAU_INS_notri.nx57 & SAU_INS_notri.nx58 & SAU_INS_notri.nx5 9 &
SAU_INS_notri.nx6 0 & SAU_INS_notri.nx61 & SAU_INS_notri.nx62 &
SAU_INS_notri.nx63 & SAU_INS_notri.nx64 & SAU_INS_notri.nx6 5 &
SAU_INS_notri.nx6 6 & SAU_INS_notri.nx6 7 & SAU_INS_notri.nx6 8 &
SAU_INS_notri.nx6 9 & SAU_INS_notri.nx7 0 & SAU_INS_notri.nx71 &
SAU_INS_notri.nx72 & SAU_INS_notri.nx73 )

4.3.3 Mutual Exclusion of Control Signals

T h e m u t u a l e x c l u s i o n of the s i g n a l s CONTROL_A, CONTROL_B, CONTROL_C, a n d CONTROL_D
was the hardest property in Sampling Unit. The reset signal LRESET may not be active. No
pair of these four control signals can be active at the same time. The formula corresponding
to this setting is the following:
G !( ! LRESET &
(
( SAU_INS_notri.sau_cores_0_U_SAU_CORE.CONTROL_A &
SAU INS notri.sau cores 0 U SAU CORE.CONTROL B )

24
 4.4. GENERAL NOTES

| ( SAU__INS_ notri sau__cores__0__U__SAU__CORE CONTROL__A

SAU__INS_ notri sau__cores__0__U__SAU__CORE CONTROL__C
| ( SAU__INS_ notri sau__cores__0__U__SAU__CORE CONTROL__A
SAU__INS_ notri sau__cores__0__U__SAU__CORE CONTROL__D
| ( SAU__INS_ notri sau__cores__0__U__SAU__CORE CONTROL__B
SAU__INS_ notri sau__cores__0__U__SAU__CORE CONTROL__C
| ( SAU__INS_ notri sau__cores__0__U__SAU__CORE CONTROL__B
SAU__INS_ notri sau__cores__0__u__SAU__CORE CONTROL__D
| ( SAU__INS_ notri sau__cores__0__u__SAU__CORE CONTROL__C
SAU INS notri sau cores 0 u SAU CORE CONTROL D

4.4 General notes

The formal verification of the three components has been presented and the procedures in
common use to obtain results have been outlined. Preconditions on every clock and reset
signals have to be assumed - only such executions of the system where the clocks are tick-
ing and no reset signal interrupts it are usually considered. When the verification exceeds
available physical memory or the patience of the user, the irrelevant modules can be care-
fully substituted with their empty versions and this substitution has to be documented. In
the rest of this section analysis of time and space consumed by Cadence SMV model checker
will be given.
We were looking for the best platform for fast verification process. For this purpose the
test source code was created and the time and space consumed by Cadence SMV with the
test verification as input was analyzed. Cadence SMV model checker is freely available for
the following platforms: HP/UX, IRIX, Linux, S o l a r i s , and Windows. The latest version
of Cadence SMV is only available on the Linux, Windows, and S o l a r i s platforms.
The time and memory consumption on different platforms is shown in logarithmic scale
in Figure 4.3. We found only small differences between Cadence SMV versions on differ-
ent platforms considering memory consumption. The only problem was that on Windows
platform the test verification had not been finished within 600 MB of free physical memory.
Running times of Cadence SMV with the testing verification as input on several differ-
ent computers are shown in Figure 4.4. Each row stands for average running time of two
verifications performed on one computer.
For efficient usage of Cadence SMV we recommend to use Linux or Solaris operating
system. Only the single process version of Cadence SMV is available, therefore single pro-
cessor machine is sufficient. The size of physical memory should be as large as possible, but
at most 4 GB, since only the 32-bit version is available.

25
 4.4. GENERAL NOTES

1000
Comparison test on Linux — :
Comparison test SunOS
Comparison test on IRIX64
•

151 MB
126 MB 129 MB
100
J ^ '' -
: j ;/--''

10
, r/ •

10 100 1000 10000

time [si

Figure 4.3: The memory consumption of Cadence SMV during the time on different plat-
forms.

Average time of test verification

Athlon 64 1,9 Ghz, Linux 1092
Pentium 4 3 Ghz, Linux 1243
Pentium 4 3 Ghz, Linux 1252
Pentium 4 2,6 Ghz, Linux 1343
Pentium 4 2,6 Ghz, Linux 13.54
Pentium 4 Xeon 3 Ghz, Linux

UltraSPARC III 750 Mhz, SunOS

MIPS R12000 350 Mhz, IRIX64

Athlon 850 Mhz, Windows XP

Athlon 6 4 1,9 Ghz, Windows XP

1000 2000 3000 4000 5000 6000 7000

Time in seconds (lower is better).

Figure 4.4: The graph compares running time of Cadence SMV on different platforms.

26
Chapter 5

Verification Reports

The verification process is applied incrementally, i.e., the results achieved after changing
some steps of the process are compared with the previous results. For this purpose, a lot of
information is included in each verification result - VHDL code used, parameters of transla-
tion to SMV, and preconditions of the verified properties. To be able to do effective verifica-
tion a verification report has been defined using XML [KRS03]. The formulas are extracted
from verification report to standalone file with extension . f o r m u l a s and this file is auto-
matically included to generated SMV source code.
However, it has appeared very inefficient to write the XML documents by hand. There-
fore, an user-friendly verification environment called Verunka has been developed [HKR+04a].
The main features of this environment are proper calling of the Cadence SMVmodel checker
and automatic generation of XML verification reports.

5.1 XML structure

For each version of verified design the element v e r is created. Element v e r contains all
important information about performed verification, so it can be reproduced. Every v e r
element consists of:

• The list of source files

• The list of preconditions, which can be assumed by formulas.

• The list of formulas, where each formula contains the following:

- LTL or CTL code

- description of property expressed by the formula
- subset of preconditions assumed by the formula
- result of formal verification of formula can be:
* none - the property is not yet verified.
* true - the property is satisfied.
* false - the property is not satisfied.
* unfinished - the verification takes a lot of time or memory. The limit given
for unfinished formulas is 1 day or 2GB of memory.

27
 5.1. XML STRUCTURE

- CPU time consumed by verification (optionally)

- differences from the original source code (if any)
- note (optionally)
- counterexample (optionally when formula is false)

Every verification report has to be valid according to v e r i f i c a t i o n . d t d which listed in

Appendix B. The following example of source code of a verification report describes a part
of Edit Engine verification.

<!DOCTYPE v e r i f i c a t i o n SYSTEM " v e r i f i c a t i o n . d t d " >

<verification>
<ver mainmodule="ee" t o p l e v e l = " E d i t Engine"
date="2005-01-03 12:10" synchronous="yes"
author="Tomas Kratochvila">
< v h d l s o u r c e l i s t exportdate="2005-01-03 12:10"
src="CVS: l i b e r o u t e r / v h d l _ d e s i g n / u n i t s / e e / c o m p / e e _ u n i t / "
url="http://www.liberouter.org/cgi-bin2/cvsweb.cgi/
liberouter/vhdl_design/units/ee/comp/ee_unit/"
author="Tomas Martinek">
< f i l e name="comp/dram_unit/dram_u_fsm_mem.vhd" type="vhdl" />
< f i l e name="comp/dram_unit/dram_u_fsm.vhd" type="vhdl" />
< f i l e name="comp/dram_unit/dram_u.vhd" type="vhdl" />
< f i l e name="comp/send_unit/send_u.vhd" type="vhdl" />
< f i l e name="comp/control_unit/control_u_fsm_mem.vhd" type="vhdl" />
< f i l e name="comp/control_unit/control_u_fsrn.vhd" type="vhdl" />
< f i l e name="comp/control_unit/control_u.vhd" type="vhdl" />
< f i l e name="comp/output_unit/output_u_fifo.vhd" type="vhdl" />
< f i l e name="comp/output_unit/output_u.vhd" type="vhdl" />
< f i l e name="comp/alu/alu.vhd" type="vhdl" />
< f i l e name="pd_block.vhd" type="vhdl" />
< f i l e name="ep_block.vhd" type="vhdl" />
< f i l e name="pp_block.vhd" type="vhdl" />
< f i l e name="im_block.vhd" type="vhdl" />
< f i l e name="addr_dc_pc.vhd" type="vhdl" />
< f i l e name="ee.vhd" type="vhdl" />
</vhdlsourcelist>
<preconditions>
< p r e c o n d i t i o n name="preCLK_RUNNING">
<code> G ( F (CLK) & F (!CLK) )</code>
< d e s c r i p t i o n > P r e c o n d i t i o n t h a t clock CLK i s t i c k i n g . < / d e s c r i p t i o n >
</precondition>
</preconditions>
<formulas>
<formula preconditions="preCLK_RUNNING" name="RW_mutual_exclusion"
r e s u l t = " t r u e " logic="LTL">
<code> G (! ( plx_wr && plx_rd ) )</code>

28
 5.2. ADDITIONAL PROCESSING

<description>Simple read-write mutual exclusion formula.</description>

<time>0.66 s</time>
</formula>
<formula preconditions="preCLK_RUNNING" name="DRAM_communication_WR"
result="true" logic="LTL">
<code>
G ( ( !DRAM_COM_U.RESET && DRAM_COM_U.START )
->
( X DRAM_WR_REQ ) )
</code>
<description>
DRAM scheduler communication for
WR REQ FSM (Write Request Finite State Machine)
</description>
<time>19.68 s</time>
</formula>
</formulas>
</ver>
</verification>

5.2 Additional Processing

We have created an XSLT transformation from verification report XML to XHTML for web
presentation. The XSLT source code is listed in Appendix C. Actually, 15 components are
presented in this fashion on Liberouter [Lib] project on formal verification group web pages
and are available for hardware developers.
The more elegant way to add an appearance to the verification report XML provides cas-
cade style sheets. For this purpose, the v e r i f i c a t i o n x m l . e s s which is referenced from
each verification report has been written. The problem is that some current web browsers
does not support CSS version 2, which is necessary with respect to the compact nature of
the verification report.
A web guidepost to every presented verification report is generated from d i a g r a m . s v g
and is transformed to d i a g r a m . png click-able image map. In this diagram the components
under formal verification are darkened boxes and clicking on a selected component leads to
displaying of the relevant verification results.

29
Chapter 6

Conclusion

In this thesis we have chosen the Cadence SMV symbolic model checker and we have cre-
ated the translation framework to be able to verify VHDL source code. The formal verifica-
tion of selected components has been presented and the way of finding a very significant
bug in the FPGA design has been demonstrated. It is worth noting that it could be very un-
likely to discover such a bug using standard simulation or testing methods. Moreover, the
verification framework established as a side effect of every verification process (i.e., the LTL
formulas) is suitably reused in future verification of new versions of component. For exam-
ple, formulas used for FIFO BRAM verification were already used in other FIFO components
and can be reused even in queue or buffer components.
Furthermore, it often leads to backward refinement of component specification, which is
contributive to future reuse of the design. From our experience, it is very useful to guarantee
some properties of the system. Moreover, these properties improve the documentation of the
system. Properties like "the maximal time in which the component process the request is 7
clock ticks," are important for inter component design and can be hardly guaranteed by
other methods.
There is another way of using formal verification in projects of this kind. An extensive
method is creation of an abstract model of the design. We also apply this approach in our
project [ARK04]. The problem of this approach is to insure the abstract model to be sound.
In comparison, the low-level way of verification presented in this thesis has the advantage
of being fast and very accurate. The abstract model approach should be used in early design
stages when no source codes are available anyway. Our current experiences show that it is
useful to combine both approaches.
We have created many tools for translation process management, absolute reproducibil-
ity of verification, easier manipulation with counterexamples, more formal documentation,
easy specification of properties, and reporting verification results. We aim to create fully
automatic formal verification environment for acceleration of hardware developing and de-
bugging process.

30
Appendix A

Different Assertion Approaches

In this appendix the simple example will illustrate the different approaches to write asser­
tions in hardware design source codes. The property is expressed informally English and
formally in various source codes as an assertion. The example is taken from [Yeu04].
The example property is as following:

"When DMA buffer is full, write should not happen."

Similarly:

"The DMA buffer should not overflow."

LTL formula in Cadence SMV:

dma_buffer_never_overflow: assert
G ! (fifo_full & fifo_write & !dma_clk & X dma_clk);
prove dma_buffer_never_overflow;

Assertion in comment in VHDL (have to be manually translated):

-- Assert exclusion f i f o _ f u l l , fifo_write

Assertion in VHDL:
process (dma_clk) begin
if dma_cIk'event and dma_clk = ' ľ then
assert not (fifo_full and fifo_write)
report "DMA buffer overflow" severity FAILURE;
end if;
end process;

Assertion in Verilog:
//synopsys translate_off
always @(posedge dma_clk) begin
if (fifo_full && fifo_write)
$display("DMA buffer overflow at time %d", $time);
end
//synopsys translate_on

Assertion in SystemVerilog:

31
 A. DIFFERENT ASSERTION A P P R O A C H E S

property dma_buffer_overflow;
©(posedge dma_clk)
not (fifo_full && fifo_write);
endproperty
assert property (dma_buffer_overflow);

Assertion in PSL:

property dma_buffer_overflow =
never (fifo_full and fifo_write) @ (posedge dma_clk);
assert dma_buffer_overflow;
OVL Assertion:
dma_buffer_overflow assert_fifo_index
#(4, 16) // severity level, depth
(dma_clk, dma_rst, push, pop);

CheckerWare Assertion:

/ * Oin f i f o -enq push -deq pop - d e p t h 16 - s e v e r i t y 4

-name dma_buffer_overflow * /

32
Appendix B

Verification Report DTD

Every verification report has to be valid according to v e r i f i c a t i o n . d t d listed bellow.

The up to date version can be found at: < h t t p : //www. l i b e r o u t e r . o r g / c g i - b i n 2 /
cvsweb.cgi/"checkout~/liberouter/ver/reports/verification.dtd>
<! --
Program name: DTD for verification *_ver.xml files.
Copyright (C) 2003 CESNET
Author(s): Tomáš Kratochvíla <[email protected]>

$Id: verification.dtd,v 1.10 2005/03/29 14:38:29 krata Exp $

-->

-- root element -->

ELEMENT verification (note?, ver*)>

-- common elements -->

<!ELEMENT note (#PCDATA)>

<!ELEMENT code (#PCDATA)>

-- each ver element -->

<!ELEMENT ver (description*, note?,diff?,

vhdlsourcelist,preconditions,formulas)>
<IATTLIST ver
author CDATA #REQUIRED
toplevel CDATA #REQUIRED
date CDATA #IMPLIED
mainmodule CDATA #REQUIRED
synchronous (yes|no) "yes">

<!-- vhdl source list -->

<!-- Use URL attribute only with SRC attribute. -->

<!ELEMENT vhdlsourcelist (file+)>

<IATTLIST vhdlsourcelist
author CDATA #IMPLIED

33
 B. VERIFICATION REPORT DTD

src CDATA #IMPLIED

url CDATA #IMPLIED
exportdate CDATA #REQUIRED>

ELEMENT file EMPTY>

ATTLIST file
type (vhdl|verilog) "vhdl"

name CDATA #REQUIRED>

-- preconditions -->

ELEMENT preconditions (precondition*)>

ELEMENT precondition (code,description?,note?)>

ATTLIST precondition

name CDATA #REQUIRED>

-- formulas -->

ELEMENT formulas (formula*)>

ELEMENT formula (code,description?,counterexample?,diff?,note?,time?)>

-- The _result_ of formal verifiation of formula could be
<blue> none The property is not yet verified.
<green> true The property is satisfied.
<red> false The property is not satisfied.
<gray> unfinished The verification takes much time or memory.
The official limit for unfinished formulas
is 1 day or 2GB of memory.-->
<!ATTLIST formula
logic (LTL|CTL) "LTL"
name CDATA #REQUIRED
preconditions CDATA #IMPLIED
result (true I false I none I unfinished) "none">
ELEMENT description (#PCDATA)>
-- Diffrence from original source codes for each element <formula> -->
ELEMENT diff (#PCDATA)>
ELEMENT time (#PCDATA)>
<!ELEMENT counterexample (#PCDATA)>

34
Appendix C

XSLT transformation from XML to XHTML

The XML verification report can be transformed to XHTML for web presentation using XSLT
transformation listed bellow. The up to date version of XSLT transformation can be found at:
<http://www.liberouter.org/cgi-bin2/cvsweb.cgi/~checkout~/liberouter/
ver/reports/verification2xhtml.xsl>

<! --

Program name: XSLT for converting verification XML files to XTML files.
Copyright (C) 2003 CESNET
Author(s): Tomáš Kratochvíla <[email protected]>

-->
<xsl:stylesheet version="2.0"
xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
xmlns="http://www.w3.org/1999/xhtml">
<xsl:output method="xhtml" encoding="utf-8"
doctype-public="-//W3C//DTD XHTML 1.1//EN"
doctype-system=
"http://www.w3.org/TR/xhtmlll/DTD/xhtmlll.dtd"/>
<xsl:template match="verification">
<html>
<head>
<title>Verification Reports</title>
<link rel="stylesheet"
href="http://www.liberouter.org/screen.ess"
type="text/css" />
<link rel="stylesheet"
href="http://www.liberouter.org/
formal_verification/verification.ess"
type="text/css" />
</head>
<body>
<div id="text">
<div class="header">Verification Reports</div>
<div class="text">
<xsl:if test="note"><pxi>
<xsl:value-of select="note"/>
</ix/px/xsl: if >

35
 C. XSLT TRANSFORMATION FROM XML TO XHTML

<ul id="menu-left">
<xsl:apply-templates select="ver" mode="header"/>
</ul>
< p x x s l :apply-templates select="ver" mode="full"/x/p>
</div>
</div>
</body>
</html>
</xsl:tempiate>

<xsl:template match="ver/@toplevel">
< p x x s l : value-of select="ver/@toplevel"/x/p>
</xsl:tempiate>

< x s l : t e m p l a t e match="ver" mode="header">

<lixa>
< x s l : a t t r i b u t e name="href">#<xsl:value-of s e l e c t = " @ t o p l e v e l " />
-<xsl:value-of select="position()" /></xsl:attribute>
<xsl:value-of select="@toplevel"/>
< x s l : i f test="@date"> - ( < x s l : v a l u e - o f s e l e c t = " @ d a t e " / > ) < / x s l : i f >
</ax/li>
</xsl:tempiate>

< x s l : t e m p l a t e match="ver" mode="full">

<hlxa>
< x s l : a t t r i b u t e name="name"xxsl :value-of s e l e c t = " @ t o p l e v e l " />
-<xsl:value-of select="position()" /></xsl:attribute>
<xsl:value-of select="@toplevel"/>
<xsl:if test="date"> - (<xsl:value-of select="@date"/>)</xsl:if>
</ax/hl>
Author: < x s l : v a l u e - o f s e l e c t = " @ a u t h o r " / x b r / >
<xsl:apply-tempiates select="description"/>
<xsl:if test="note"><i>
<xsl:value-of select="note"/>
< / i x b r / x / x s l : if >
<h2>VHDL source l i s t
<xsl:if test="vhdlsourcelist/@src">from
<xsl:if test="vhdlsourcelist/@url">
< a x x s l : a t t r i b u t e name="href">
<xsl:value-of select="vhdlsourcelist/@url"/>
</xsl:attribute>
<xsl:value-of select="vhdlsourcelist/@src"/>
</a>
</xsl:if>
<xsl:if test="not(vhdlsourcelist/@url)">
<xsl:value-of select="vhdlsourcelist/@src"/>
</xsl:if>
</xsl:if>

36
 C. XSLT TRANSFORMATION FROM X M L TO X H T M L

(date: <xsl:value-of select="vhdlsourcelist/@exportdate"/>)</h2>

<xsl:apply-tempiates select="vhdlsourcelist"/>
<h2>Preconditions</h2>
<xsl:apply-tempiates select="preconditions/precondition"/>
<h2>Formulas</h2>
<xsl:apply-tempiates select="formulas/formula"/>
</xsl:tempiate>

<xsl:template match="description">
<pxxsl :value-of select=". "/></p>
</xsl:tempiate>

<xsl:template match="vhdlsourcelist">
<p>
<xsl:if test="directory">
<xsl:apply-tempiates select="directory"/>
</xsl:if>
<xsl:if test="file">
<xsl:apply-tempiates select="file"/>
</xsl:if>
</p>
</xsl:tempiate>

<xsl:template match="directory">
<xsl:apply-tempiates select="directory"/>
<xsl:apply-tempiates select="file"/>
</xsl:tempiate>

<xsl:template match="file">
<tt>
<xsl:if test="(../../../©name) and not(../../../../©name)">
<xsl:value-of select="concat(../../../©name,'/',
. .I. ./©name,'/',../©name,'/',©name)"/>
</xsl:if>
<xsl:if test="(../../©name) and not(../../../©name)">
<xsl:value-of select="concat(../../©name,'/',
../©name,'/',©name)"/>
</xsl:if>
<xsl:if test="(../©name) and not(../../©name)">
<xsl:value-of select="concat(../©name,'/',@name)"/>
</xsl:if>
<xsl:if test="not(../©name)">
<xsl:value-of select="@name"/>
</xsl:if>
<xsl:if test="@type">
(<xsl:value-of select="@type"/>)
</xsl:if>
</ttxbr/>

37
 C. XSLT TRANSFORMATION FROM XML TO XHTML

</xsl:template>

<xsl:template match="precondition">
• c t t x b x x s l : v a l u e - o f select="@name"/> : </b>
<xsl : v a l u e - o f s e l e c t = " c o d e " / x / t t >
<xsl:if test="description">
<xsl : v a l u e - o f s e l e c t = " d e s c r i p t i o n " / x b r / >
</xsl:if>
<xsl:if test="note"><br/xi>
<xsl:value-of select="note"/>
</ix/xsl: if ><br/>
</xsl:tempiate>

<xsl:template match="formula">
<xsl:choose>
<xsl:when test="@result='true'">
<h3 class="true">
<xsl:value-of select="@name"/>
</h3>
</xsl:when>
<xsl:when test="@result='false'">
<h3 class="false">
<xsl:value-of select="@name"/>
</h3>
</xsl:when>
<xsl:when test="@result='unfinished'">
<h3 class="unfinished">
<xsl:value-of select="@name"/>
</h3>
</xsl:when>
<xsl:otherwise>
<h3>
<xsl:value-of select="@name"/>
</h3>
</xsl:otherwise>
</xsl:choose>
<pre>
<xsl:value-of select="code"/>
</pre>
<xsl:if test="description">
<xsl:value-of select="description"/>
< b r / x / x s l : if >
<xsl: if test="©preconditions"><pxb>Preconditions :
< / b x b r / x t t x x s l :value-of select="@preconditions"/>
< / t t x / p x / x s l : if >
< x s l : i f t e s t = " counterexample" ><pxb>Count er example :
< / b x b r / x x s l :value-of select="counterexample"/>
< / p x / x s l : if >

38
 C. XSLT TRANSFORMATION FROM XML TO XHTML

< x s l : i f t e s t = " d i f f" > < p x b > D i f f e r e n c e s from t h e o r i g i n a l d e s i g n

code: < / b x b r / x x s l : v a l u e - o f s e l e c t = " d i f f "/></p></xsl: if >
<xsl:if t e s t = " n o t e " x p x i x x s l :value-of select="note"/>
< / i x / p x / x s l : if >
< x s l : i f t e s t = " t i m e " > < p x i > V e r i f i e d in
<xsl:value-of select="time"/>.
< / i x / p x / x s l : if >
</xsl:tempiate>

</xsl:stylesheet>

39
Bibliography

[AFN03] Jiří Novotný, Otto Fučík, and David Antoš: Projed of IPv6 Router with
FPGA Hardware Accelerator, Field-Programmable Logic and Applications,
volume 2778 of LNCS, Springer, 964 - 967, 2003. 1, 2.3

[ARK04] David Antoš, Vojtěch Řehák, and Jan Kořenek: Hardware Router's Lookup
Machine and its Formal Verification, 0-86341-325-0, ICN'2004 Conference
Proceedings, Gosier, Guadeloupe, French Caribbean, 1002 - 1007, 2004. 6

[BBK+02] Jiří Barnat, Tomáš Brázdil, Pavel Krčál, Vojtěch Řehák, and David Šafránek:
Model Checking in IPv6 Hardware Router Design, Technical Report 8/2002,
CESNET, 2002, URL: < h t t p : / / w w w . c e s n e t . c z / d o c / t e c h z p r a v y /
2002/ipv6hwdesign/> .

[BCM+90] J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang: Symbolic Model

Checking: 1020 States and Beyond, Proceedings of the Fifth Annual Sympo­
sium on Logic in Computer Science, IEEE Computer Society Press, Wash­
ington, 1 - 33,1990. 2.2

[Bry86] Randal Bryant: Graph-Based Algorithms for Boolean Function Manipula­

tion, IEEE Transactions on Computers, 677 - 691,1986. 2.2

[CGH94] Edmund Clarke, Orna Grumberg, and Kiyoharu Hamaguchi: Another Look
at LTL Model Checking, CAV '94: Proceedings of the 6th International Con­
ference on Computer Aided Verification, Springer-Verlag, London, UK, 415
-427,1994. 2.1

[CGP99] E. Clarke, O. Grumberg, and D. Peled: Model Checking, MIT Press, Cam­
bridge, 1999. 1, 2,2.2, 2.4

[EVD90] P. Eijk, C. Vissers, and M. Diaz: VHDL Cookbook, Dept. of Computer Sci­
ence, University of Adelaide, South Australia, 1990.

[Eme90] E. Emerson: Handbook of Theoretical Computer Science: Formal Models

and Semantics, 0-444-88074-7, Volume B, MIT Press, 995 - 1072,1994. 1,2.1

[HKR+04] Jan Holeček, Tomáš Kratochvíla, Vojtěch Řehák, David Šafránek, and Pavel
Šimeček: Verification Results in Liberouter Projed, URL: < h t t p : //www.
cesnet.cz/doc/techzpravy/2004/verificationresults/> ,
Technical Report 3/2004, CESNET, 2004. 2.5

[HKR+04a] Jan Holeček, Tomáš Kratochvíla, Vojtěch Řehák, David Šafránek, and
Pavel Šimeček: Verification Process of Hardware Design in Liberouter
Projed, URL: <http://www.cesnet.cz/doc/techzpravy/2004/
v e r i f p r o c e s s / > , Technical Report 5/2004, CESNET, 2004. 5

40
[HKR+04b] Jan Holeček, Tomáš Kratochvíla, Vojtěch Řehák, David Šafránek, and Pavel
Šimeček: How to Formalize FPGA Hardware Design, URL: < h t t p : / /
www.cesnet.cz/doc/techzpravy/2004/formal-fpga-design/> ,
Technical Report 4/2004, CESNET, 2004.

[IEEE93] IEEE: Standard VHDL Language Reference Manual, IEEE Standard 1076 -
1993, Institution of Electrical and Electronics Engineers, 1993. 2.3

[IEEE95] IEEE: Verilog HDL Language Reference Manual, IEEE Draft Standard 1364,
Institution of Electrical and Electronics Engineers, 1993. 2.3

[KRS03] Tomáš Kratochvíla, Vojtěch Řehák, and Pavel Šimeček: Verification

of COMB06 VHDL Design, URL: < h t t p : / / w w w . c e s n e t . c z / d o c /
t e c h z p r a v y / 2 0 0 3 / t r a n s l a t i o n v e r / > , Technical Report 17/2003,
CESNET, 2003. 2.5, 2.5.1,5

[KRS05] Tomáš Kratochvíla, Vojtěch Řehák, and David Šafránek: Formal Verification
of a FIFO Component in FPGA Design, Submission, International Confer­
ence on Field Programmable Logic and Applications, 2005. 3

[Kra03] Tomáš Kratochvíla: Verification Cookbook (Liberouter policy WWW

Pages), 2003. 2.5

[Lib] Liberouter: Liberouter project, URL: < h t t p : //www. l i b e r o u t e r . o r g / >

. 2.3,3.2,5.2

[MP] Tomáš Martínek and Tomáš Pečenka: Generic FIFO Documentation,

URL: <http://www.liberouter.org/vhdl_design/generated/
l i b e r o u t e r / c o m m o n _ f i f o _ h w . p h p > . 3.4.1

[Mar] Tomáš Martínek: Basic Documentation and Schemes of FIFO BRAM

Component, URL: < h t t p : / / w w w . l i b e r o u t e r . o r g / v h d l _ d e s i g n /
g e n e r a t e d / l i b e r o u t e r / c o m m o n _ f i f o _ b r a m _ h w . p h p > . 3.1

[Mar03] Tomáš Martínek: Edit Engine Implementation in FPGA (Czech), Master

Thesis, Brno University of Technology, Faculty of Information Technology,
2003. 4.1

[McM] Ken McMillan: Cadence SMV, URL: <http://www-cad.eecs.

b e r k e l e y . e d u / ~ k e n m c m i l / > . 2.4

[McM93] Ken McMillan: Symbolic Model Checking, Kluwer Academic Publishers,

Norwell, MA, USA, 1993.

[Men] Mentor Graphics, URL: < h t t p : //www. m e n t o r . com/> . 2.5

41
[PCK] Jan Kořenek, Martin Mikušek, and Jiří Tobola: Payload Checker Docu­
mentation, URL: <http://www.liberouter.org/vhdl_design/
g e n e r a t e d / s c a m p i _ p h 2 / s c a m p i _ p h 2 _ p c k _ h w . p h p > . 4.2

[Sea] Scampi, A Scaleable Monitoring Platform for the Internet, URL: < h t t p :
//www.ist-scampi.org/> . 4

[Smo04] Vladimir Smotlacha: Design of the VHDL structure of SCAMPI adapter,

URL: <http://www.liberouter.org/cgi-bin2/cvsweb.cgi/
liberouter/vhdl_design/projects/scampi_phl/doc/VHDL_
s t r u c t u r e . p s > , 2004. 4.3

[Xil05] XAPP258 - FIFOs Using Virtex-II Block RAM Application Note, 2005,
URL: < h t t p : / / d i r e c t . x i l i n x . c o m / b v d o c s / a p p n o t e s / x a p p 2 5 8 .
pdf > . 3.1

[Yeu04] Ping Yeung: The Four Pillars of Assertion-Based Verification, Mentor

Graphics Corporation, 2004. A

42