Constrained symbolic simulation with mathematica and ACL2

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

doi:10.1007/978-3-540-39724-3_14

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 proceeding › Conference contribution › Academic › peer-review

3 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 language	English
Title of host publication	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)
Editors	D. Geist, E. Tronci
Place of Publication	Berlin
Publisher	Springer
Pages	150-157
ISBN (Print)	978-3-540-20363-6
DOIs	https://doi.org/10.1007/978-3-540-39724-3_14
Publication status	Published - 2003

Publication series

Name	Lecture Notes in Computer Science
Volume	2860
ISSN (Print)	0302-9743

Access to Document

10.1007/978-3-540-39724-3_14

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

Al Sammane, G. ; Toma, D. ; Schmaltz, J. et al. / Constrained symbolic simulation with mathematica and ACL2. 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). editor / D. Geist ; E. Tronci. Berlin : Springer, 2003. pp. 150-157 (Lecture Notes in Computer Science).

@inproceedings{0f29b8df066e4241ac8b2bdc83c1c604,

title = "Constrained symbolic simulation with mathematica and ACL2",

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.",

author = "{Al Sammane}, G. and D. Toma and J. Schmaltz and P. Ostier and D. Borrione",

year = "2003",

doi = "10.1007/978-3-540-39724-3_14",

language = "English",

isbn = "978-3-540-20363-6",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "150--157",

editor = "D. Geist and E. Tronci",

booktitle = "Correct Hardware Design and Verification Methods (12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L{\textquoteright}Aquila, Italy, October 21-24, 2003. Proceedings)",

address = "Germany",

}

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). Lecture Notes in Computer Science, vol. 2860, Springer, Berlin, pp. 150-157. https://doi.org/10.1007/978-3-540-39724-3_14

Constrained symbolic simulation with mathematica and ACL2. / Al Sammane, G.; Toma, D.; Schmaltz, J. et al.

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). ed. / D. Geist; E. Tronci. Berlin : Springer, 2003. p. 150-157 (Lecture Notes in Computer Science; Vol. 2860).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Constrained symbolic simulation with mathematica and ACL2

AU - Al Sammane, G.

AU - Toma, D.

AU - Schmaltz, J.

AU - Ostier, P.

AU - Borrione, D.

PY - 2003

Y1 - 2003

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-540-39724-3_14

DO - 10.1007/978-3-540-39724-3_14

M3 - Conference contribution

SN - 978-3-540-20363-6

T3 - Lecture Notes in Computer Science

SP - 150

EP - 157

BT - 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)

A2 - Geist, D.

A2 - Tronci, E.

PB - Springer

CY - Berlin

ER -

Al Sammane G, Toma D, Schmaltz J, Ostier P, Borrione D. Constrained symbolic simulation with mathematica and ACL2. In Geist D, Tronci E, editors, 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). Berlin: Springer. 2003. p. 150-157. (Lecture Notes in Computer Science). doi: 10.1007/978-3-540-39724-3_14

Constrained symbolic simulation with mathematica and ACL2

Abstract

Publication series

Access to Document

Fingerprint

Cite this