Hardware verification using ANSI-C programs as a reference

Author

Clarke, Edmund ; Kroening, Daniel

Author_Institution

Dept. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA

fYear

2003

fDate

21-24 Jan. 2003

Firstpage

308

Lastpage

311

Abstract

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.

Keywords

C language; computability; cryptography; formal verification; hardware description languages; ANSI-C programs; SAT based bounded model checking; Verilog; bit vector logic decision problem; data encryption standard; equivalence problem; hardware verification; Algorithm design and analysis; Circuit testing; Computer science; Contracts; Cryptography; Debugging; Electronic mail; Hardware design languages; Logic; Software standards;

fLanguage

English

Publisher

ieee

Conference_Titel

Design Automation Conference, 2003. Proceedings of the ASP-DAC 2003. Asia and South Pacific

Print_ISBN

0-7803-7659-5

Type

conf

DOI

10.1109/ASPDAC.2003.1195033

Filename

1195033

Link To Document

https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=3399236