Modeling Algorithms in SystemC and ACL2
| Autor: | O'Leary, John W., Russinoff, David M. |
|---|---|
| Rok vydání: | 2014 |
| Předmět: | |
| Zdroj: | EPTCS 152, 2014, pp. 145-162 |
| Druh dokumentu: | Working Paper |
| DOI: | 10.4204/EPTCS.152.12 |
| Popis: | 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. Comment: In Proceedings ACL2 2014, arXiv:1406.1238 |
| Databáze: | arXiv |
| Externí odkaz: |
|