Modeling Algorithms in SystemC and ACL2
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 A...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2014-06-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1406.1565v1 |
| _version_ | 1811218016038289408 |
|---|---|
| author | John W. O'Leary David M. Russinoff |
| author_facet | John W. O'Leary David M. Russinoff |
| author_sort | John W. O'Leary |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-12T07:04:02Z |
| format | Article |
| id | doaj.art-92a4966af949466b8eafcb3842168e35 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-12T07:04:02Z |
| publishDate | 2014-06-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-92a4966af949466b8eafcb3842168e352022-12-22T03:42:56ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802014-06-01152Proc. ACL2 201414516210.4204/EPTCS.152.12:15Modeling Algorithms in SystemC and ACL2John W. O'Leary0David M. Russinoff1 Intel Corp. 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.http://arxiv.org/pdf/1406.1565v1 |
| spellingShingle | John W. O'Leary David M. Russinoff Modeling Algorithms in SystemC and ACL2 Electronic Proceedings in Theoretical Computer Science |
| title | Modeling Algorithms in SystemC and ACL2 |
| title_full | Modeling Algorithms in SystemC and ACL2 |
| title_fullStr | Modeling Algorithms in SystemC and ACL2 |
| title_full_unstemmed | Modeling Algorithms in SystemC and ACL2 |
| title_short | Modeling Algorithms in SystemC and ACL2 |
| title_sort | modeling algorithms in systemc and acl2 |
| url | http://arxiv.org/pdf/1406.1565v1 |
| work_keys_str_mv | AT johnwoleary modelingalgorithmsinsystemcandacl2 AT davidmrussinoff modelingalgorithmsinsystemcandacl2 |