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. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Toma, D., Borrione, D., & Al Sammane, G. (2005). Combining several paradigms for circuit validation and verification. In Lecture Notes in Computer Science (Vol. 3362, pp. 229–249). Springer Verlag. https://doi.org/10.1007/978-3-540-30569-9_12
Mendeley helps you to discover research relevant for your work.