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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Al Sammane, G., Toma, D., Schmaltz, J., Ostier, P., Borrione, D.: Constrained Symbolic Simulation with Mathematica and ACL2. ISRN TIMA-RR–03/07-03–FR, http://tima.imag.fr/publications/files/rr/css_177.pdf
Borrione, D., Georgelin, P., Moraes Rodrigues, V.: Symbolic Simulation and Verification of VHDL with ACL2. In: Ashenden, P.J., Mermet, J.P., Seepold, R. (eds.) System-on-chip Methodologies and Design Languages, pp. 59–70. Kluwer, Dordrecht (2001)
1076.6-1999 IEEE Standard for VHDL Register Transfer Level (RTL) Synthesis. IEEE (1999)
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided reasoning: ACL2 An approach. Kluwer Academic Publishers, Dordrecht (2000)
Maeder, R.: Term Rewriting and Programming Paradigms. In: Keränen, V.(ed): Mathematics with a Vision: Proceedings of the First International Mathematica Symposium, Computational Mechanics Publications (1995)
Moore, J.S.: Symbolic Simulation: An ACL2 Approach. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 334–350. Springer, Heidelberg (1998)
Shankar, N., Owre, S., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Prover Guide Computer Science Laboratory, SRI International, Menlo Park, CA, USA (1999)
Wolfram, S.: The Mathematica Book. Cambridge University Press and Wolfram Research, 100 Trade Center Drive, Champaign, IL 61820-7237, USA (2000)
Yang, J., Seger, C.I.: Generalized Symbolic Trajectory Evaluation Abstraction in Action. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 70–87. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sammane, G.A., Toma, D., Schmaltz, J., Ostier, P., Borrione, D. (2003). Constrained Symbolic Simulation with Mathematica and ACL2. In: Geist, D., Tronci, E. (eds) Correct Hardware Design and Verification Methods. CHARME 2003. Lecture Notes in Computer Science, vol 2860. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39724-3_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-39724-3_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20363-6
Online ISBN: 978-3-540-39724-3
eBook Packages: Springer Book Archive