Proceedings of the ASP-DAC Asia and South Pacific Design Automation Conference, 2003. · 2003 · 13 citations · 3 references
ComputingComputer EngineeringComputer ScienceAlgorithmsComputer ArchitectureFormal MethodsDeductive VerificationEquivalence CheckingModel CheckingVerificationData Encryption StandardsFormal Hardware VerificationHardware Equivalence CheckingHardware Model CheckingHardware VerificationSystem Verilog
We describe an algorithm to verify a hardware design given in Verilog using an ANSI-C program as a specification. We use SAT based bounded model checking in order to reduce the equivalence problem to a bit vector logic decision problem. As a case study, we describe experimental results on a hardware and a software implementation of the data encryption standard (DES) algorithm.
3