Formal Verification of a Protocol Converter Memory
Manager using FormalCheck
Jounaidi Ben Hassen, and Sofiene Tahar
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
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..