Behavioral consistency of C and verilog programs using bounded model checking
Published 2 June 2003Open access
Edmund M. Clarke, Daniel Kroening, Karen Yorav
Citations283
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
This work presents an algorithm that checks behavioral consistency between an ANSI-C program and a circuit given in Verilog using Bounded Model Checking and describes experimental results on various reactive circuits and programs.
Abstract
Abstract: "We present an algorithm that checks behavioral consistency between an ANSI-C program and a circuit given in Verilog using Bounded Model Checking. Both the circuit and the program are unwound and translated into a formula that is satisfiable if and only if the circuit and the code disagree. The formula is then checked using a SAT solver. We are able to translate C programs that make use of side effects, pointers, dynamic memory allocation, and loops with conditions that cannot be evaluated statically. We describe experimental results on various reactive circuits and programs, including a small processor given in Verilog and its Instruction Set Architecture given in ANSI-C."
Keywords
Computer Science
Computer Architecture: A Quantitative Approach
9,536 Citations1989John L. Hennessy, David A. Patterson
This best-selling title, considered for over a decade to be essential reading for every serious student and practitioner of computer design, has been updated throughout to address the most important trends facing computer designers today.
Chaff
2,859 Citations2001Matthew W. Moskewicz, Conor Madigan +3 more
The development of a new complete solver, Chaff, is described which achieves significant performance gains through careful engineering of all aspects of the search-especially a particularly efficient implementation of Boolean constraint propagation (BCP) and a novel low overhead decision strategy.
Lecture notes in computer scienceSymbolic Model Checking without BDDs
2,113 Citations1999Armin Biere, Alessandro Cimatti +2 more
This paper shows how boolean decision procedures, like Stalmarck's Method or the Davis & Putnam Procedure, can replace BDDs, and introduces a bounded model checking procedure for LTL which reduces model checking to propositional satisfiability.
Symbolic model checking using SAT procedures instead of BDDs
688 Citations1999Armin Biere, Alessandro Cimatti +3 more
This paper applies bounded model checking to equivalence and invariant checking and presents several optimizations that reduce the size of generated propositional formulas in hardware verification.
In Transition From Global to Modular Temporal Reasoning about Programs
513 Citations1985Amir Pnueli
The role of Temporal Logic as a feasible approach to the specification and verification of concurrent systems is now widely accepted and a companion paper in this volume defines the area of applicability of Tem temporal Logic as that of reactive systems.
Choice Reviews OnlineThe Verilog hardware description language
502 Citations1991Donald E. Thomas, Philip R. Moorby +1 more
The Verilog Hardware Description Language, Fifth Edition, is a valuable resource for engineers and students interested in describing, simulating, and synthesizing digital systems; the extensive number of simulatable examples and wide range of representation styles covered ensure its quick use in design.
An efficient method of computing static single assignment form
460 Citations1989Ron K. Cytron, Jeanne Ferrante +3 more
This paper presents strong evidence that static single assignment form and the control dependence graph can be of practical use in optimization, and presents a new algorithm that efficiently computes these data structures for arbitrary control flow graph.
Lecture notes in computer scienceBenefits of Bounded Model Checking at an Industrial Setting
185 Citations2001Fady Copty, Limor Fix +5 more
The usefulness of Bounded Model Checking based on propositional satisfiability (SAT) methods for bug hunting has already been proven in several recent work, but two industrial strength systems performing BMC for both verification and falsification are presented.
Lecture notes in computer scienceTuning SAT Checkers for Bounded Model Checking
163 Citations2000Ofer Shtrichman
It is shown that the unique characteristics of BMC formulas can be exploited for a variety of optimizations in the SAT checking procedure, and proved their efficiency in many of the hard test cases, comparing to both the standard SAT procedure and a BDD-based model checker.
Lecture notes in computer scienceVerifying Safety Properties of a PowerPC− Microprocessor Using Symbolic Model Checking without BDDs
132 Citations1999Armin Biere, Edmund M. Clarke +2 more
This paper shows how bounded model checking can take advantage of specialized optimizations and presents a bounded version of the cone of influence reduction, which can bring model checking into the mainstream of industrial chip design.
The Journal of VLSI Signal Processing Systems for Signal Image and Video TechnologyConstructing hardware-software systems from a single description
112 Citations1996Ian Page
The essential unity of the two branches is explored and a common framework within which hardware-software codesigns can be expressed as a single executable specification, reasoned about, and transformed into implementations is pointed to.
Lecture notes in computer scienceFinding Bugs in an Alpha Microprocessor Using Satisfiability Solvers
112 Citations2001Per Bjesse, Tim Leonard +1 more
The techniques used to search for bugs in the memory subsystem of a next-generation Alpha microprocessor are described, and a version of symbolic trajectory evaluation that uses SAT-solvers instead of BDDs, can find as deep bugs, with even shorter runtimes.
Lecture notes in computer scienceEfficient Computation of Recurrence Diameters
98 Citations2002Daniel Kroening, Ofer Strichman
It is shown that the longest initialized loop-free path in the state graph, also known as the recurrence diameter, is sufficient for Fp properties and is a known over-approximation for the threshold of simple safety properties (Gp).
Hardware verification using ANSI-C programs as a reference
82 Citations2003Edmund M. Clarke, Daniel Kroening
Proceedings - ACM IEEE Design Automation ConferenceRTL c-based methodology for designing and verifying a multi-threaded processor
41 Citations2002Luc Sèmèria, Renu Mehra +4 more
A RTL C-based design and verification methodology is presented which enabled the successful high speed validation of a 7 million gate simultaneous multi-threaded (SMT) network processor.
The DLX Instruction Set Architecture Handbook
31 Citations1995Patty M. Sailer, Philip M. Sailer +1 more
This handbook is a valuable supplement for anyone studying from Computer Architecture, whether self-taught or as part of a class, and will also make an informative addition to the library of any computer systems designer or RISC aficionado.