Formal verification of an SoC platform protocol converter

In this paper we investigate the formal verification of the memory manager block of a system-on-a-chip platform protocol converter using the FormalCheck tool of Cadence. The memory manager represents the main block of the protocol converter and is responsible for the reception of packets and their treatment for conversion. For the verification, we first 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. Though extensive verification under the defined set of constraints, we have been able to find a few bugs in the design that were omitted by simulation. This experience demonstrates the usefulness of formal verification as complement to traditional verification by simulation.