Abstract
The early validation of components specifications requires a proven correct formalization of the functional behavior. We use the ACL2 theorem prover the establish safety properties on it. After the first design step, we automatically translate the synthesizable VHDL into a functional form. The combination of symbolic simulation, automatic transfer function extraction, and theorem proving is used to show that the VHDL design is functionally compliant to the specification. The approach is demonstrated on a SHA-1 cryptographic circuit.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
National Institute of Standards and Technology: Secure Hash Standard. Federal Information Processing Standards Publication 180–2 (2002)
Toma, D., Borrione, D.: SHA Formalization. In: Proc. ACL2 Workshop, Boulder, USA, July 13-14 (2003)
IEEE CS: 1076.6-1999 IEEE Standard for VHDL Register Transfer Level (RTL) Synthesis, New York (March 2000)
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided reasoning: ACL2 An approach (vol. 1) and ACL2 Case Studies (vol. 2). Kluwer Academic Press, Dordrecht (2000)
Roesner, W.: What Is Beyond The RTL Horizon for Microprocessor and System Design? In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, p. 1. Springer, Heidelberg (2003)
Coudert, O., Berthet, C., Madre, J.C.: Verification of synchronous sequential machines based on symbolic execution. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 365–373. Springer, Heidelberg (1990)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L.: Sequential circuits verification using symbolic model checking. In: Proc. 27th Design Automation Conf. IEEE CS Press, Los Alamitos (1990)
Déharbe, D.: Vérification formelle de propriétés temporelles: étude et application au langage VHDL, PhD, Université Josph Fourier, Grenoble, November 15 (1996) (in French)
Delgado Kloos, C., Breuer, P.T. (eds.): Formal Semantics for VHDL. International Series in Engineering and Computer Science, vol. 307. Kluwer, Dordrecht (1995)
Damm, W., Josko, B., Schlor, R.: Specification and Verification of VHDL-based System-level Hardware Designs. In: Berger, E. (ed.) Specification and validation methods for programming languages and systems, pp. 331–410. Oxford University Press, Oxford (1995)
Gajski, D., Ramachandran, L.: Introduction to High-level Synthesis. IEEE Design and Test of Computers, 44–54 (Winter 1994)
Borrione, D., Dushina, J., Pierre, L.: A Compositional Model for the Functional Verification of High-level Synthesis Results. IEEE. Trans. on VLSI 8(5), 526–530 (2000)
Darringer, J.: Application of Program Verification Techniques to Hardware Verification. In: Proc. IEEE-ACM Design Automation Conference, pp. 375–381 (1979)
Bryant, R.E., Seger, C.J.H.: Formal Verifcation by Symbolic Evaluation of Partially-ordered Trajectories. Formal Methods in System Design 6(2), 147–189 (1995)
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)
Greve, D.: Symbolic Simulation of the JEM1 Microprocessor. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 321–333. Springer, Heidelberg (1998)
Wilding, M., Greve, D., Hardin, D.: Efficient Simulation of Formal Processor Models. Formal Methods in System Design (2001)
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)
Georgelin, P.: Vérification formelle de systémes digitaux synchrones, basée sur la simulation symbolique. PhD Univ. Joseph Fourier, Grenoble, France (2001) (in French)
Al Sammane, G., Borrione, D.: Formal Validation of High Level Specification of Data-path Digital Circuits by Symbolic Simulation. In: Proc. DDECS 2003, Poznan, Poland (April 2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Toma, D., Borrione, D., Al Sammane, G. (2005). Combining Several Paradigms for Circuit Validation and Verification. In: Barthe, G., Burdy, L., Huisman, M., Lanet, JL., Muntean, T. (eds) Construction and Analysis of Safe, Secure, and Interoperable Smart Devices. CASSIS 2004. Lecture Notes in Computer Science, vol 3362. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30569-9_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-30569-9_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-24287-1
Online ISBN: 978-3-540-30569-9
eBook Packages: Computer ScienceComputer Science (R0)