Combining several paradigms for circuit validation and verification

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.