Modeling Algorithms in SystemC and ACL2

John W. O'Leary
(Intel Corp.)
David M. Russinoff
(Intel Corp)

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.

In Freek Verbeek and Julien Schmaltz: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2014), Vienna, Austria, 12-13th July 2014, Electronic Proceedings in Theoretical Computer Science 152, pp. 145–162.
Published: 4th June 2014.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: