Formal Verification of a Protocol Converter Memory
Manager using FormalCheck
Jounaidi Ben Hassen, and Sofiene Tahar
ABSTRACT
We present in this report the formal specification and verification results
of the Memory Manager block of a System-on-a-Chip (SoC) platform Protocol
Converter using the model checking
tool FormalCheck. The Memory Manager represents the main block of the
protocol converter
system and is made of five modules, namely, a Memory Manager Controller,
an Address Counter
Register, a Data Counter Register, a Packet Counter Register and a
Packet Assembler. First,
we extracted some constraints to define the environment for the Memory
Manager. Then we
specified a number of relevant liveness and safety properties expressible
in FormalCheck and
accomplished their verification under the defined set of constraints.
Through extensive verifica-
tion, we have been able to find a number of bugs in the design that
were omitted by simulation.
This experience demonstrates the usefulness of formal verification
techniques to complement
traditional verification by simulation..
Download PDF file (PDF File)