Technical Report

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
Send comments and suggestions to: jounaidi@ece.concordia.ca