Modeling Algorithms in SystemC and ACL2

TL;DR

This paper introduces MASC, a formal language based on SystemC, enabling modeling, documentation, and formal verification of hardware algorithms, demonstrated through a 32-bit multiplier example.

Contribution

It presents a novel approach to convert SystemC algorithms into a formal language for verification and synthesis, bridging modeling and formal methods.

Findings

Successful translation of SystemC to MASC for documentation

Conversion of MASC to ACL2 for formal verification

Verified correctness of a 32-bit radix-4 multiplier

Abstract

We describe the formal language MASC, based on a subset of SystemC and intended for modeling algorithms to be implemented in hardware. By means of a special-purpose parser, an algorithm coded in SystemC is converted to a MASC model for the purpose of documentation, which in turn is translated to ACL2 for formal verification. The parser also generates a SystemC variant that is suitable as input to a high-level synthesis tool. As an illustration of this methodology, we describe a proof of correctness of a simple 32-bit radix-4 multiplier.