file.pdf (63.85 kB)

Hardware Verification using ANSI-C Programs as a Reference

Download (63.85 kB)
journal contribution
posted on 01.01.1976 by Edmund M Clarke, Daniel Kroening
We describe an algorithm to verify a hardware design given in Verilog using an ANSI-C program as a specification. We use SAT based BoundedModel Checking [1] 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.

History

Publisher Statement

All Rights Reserved

Date

01/01/1976

Exports

Exports