Constrained symbolic simulation with mathematica and ACL2

G. Al Sammane, D. Toma, J. Schmaltz, P. Ostier, D. Borrione

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    2 Citations (Scopus)

    Abstract

    We use symbolic simulation for the verification of high level circuit specifications. We combine Mathematica for algebraic computation and ACL2 for branching decision to increase the efficiency of the method.
    Original languageEnglish
    Title of host publicationCorrect Hardware Design and Verification Methods (12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L’Aquila, Italy, October 21-24, 2003. Proceedings)
    EditorsD. Geist, E. Tronci
    Place of PublicationBerlin
    PublisherSpringer
    Pages150-157
    ISBN (Print)978-3-540-20363-6
    DOIs
    Publication statusPublished - 2003

    Publication series

    NameLecture Notes in Computer Science
    Volume2860
    ISSN (Print)0302-9743

    Fingerprint Dive into the research topics of 'Constrained symbolic simulation with mathematica and ACL2'. Together they form a unique fingerprint.

  • Cite this

    Al Sammane, G., Toma, D., Schmaltz, J., Ostier, P., & Borrione, D. (2003). Constrained symbolic simulation with mathematica and ACL2. In D. Geist, & E. Tronci (Eds.), Correct Hardware Design and Verification Methods (12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L’Aquila, Italy, October 21-24, 2003. Proceedings) (pp. 150-157). (Lecture Notes in Computer Science; Vol. 2860). Springer. https://doi.org/10.1007/978-3-540-39724-3_14