Name
Abstract | ||
|---|---|---|
Formal verification has had a significant impact on the semiconductor industry, particularly for companies that can devote significant resources to creating and deploying inter- nally developed verification tools. If we look more closely, however, we see that the major industrial applications of formal verification have been either in verifying individ- ual blocks, such as floating-point units and memories, or in verifying an abstracted representation of some aspect of the system, such as a cache coherence protocol. Attempt- ing to verify overall system correctness is beyond the reach of current tools. For example, these tools are not capable of verifying that an out-of-order execution microprocessor correctly replicates the behavior of its sequential instruction set architecture (ISA) model. Most existing verification tools model system operation at a detailed bit level. Using powerful inference engines, such as Binary Decision Diagrams (BDDs) and Boolean satisfiability (SAT) checkers, symbolic model checkers (3, 5) and similar tools can analyze all possible behaviors of very large, finite-state systems. Modeling a system at the bit level makes it difficult to scale formal verification to sys- tems that store and manipulate large amounts of data, such as microprocessors and many forms of embedded software. The many bits of state held in the various memories, queues, and caches lead to state explosion problems that overwhelm even the most advanced model checkers. Taking a cue from the hardware design principle of sepa- rating data from control, we believe that systems should be modeled and verified using a more abstract representation of data. If we assume individual functional units, such as ALUs and instruction decoders can be verified separately, then there is no need to track the value of every bit in the system. Instead, we can represent words of data as sym- bolic term values that are generated by function units, com- municated among different subunits, and stored in different buffers and memories. For some term value x, we need not keep track of its bit width, its encoding, or even its actual value. With this term-level abstraction of data, verification can focus on the behavior of the control logic. Term-level abstraction has long been used by researchers using automatic theorem provers to verify hardware design (10). Burch and Dill (4) were among the first to demonstrate that highly automated tools based on term-level models could be used to verify pipelined microprocessors. Rather than using Boolean inference engines, these tools make use of decision procedures for highly restricted subsets of first- order logic. Over the years, these procedures have improved greatly in their speed (11) and the richness of the logic they can handle (1, 6). We have developed UCLID (2), a prototype verifier for infinite-state systems. The UCLID modeling language ex- tends that of SMV, a bit-level model checker, to include integer and function state variables, addition by constants, and relational operations. The underlying logic is expres- sive enough to model a wide range of systems, but it still permits a decision procedure where we transform the for- mula into propositional logic and then use either BDDs or a SAT solver. Most recently, we have developed powerful predicate abstraction methods that can automatically gen- erate and prove system invariants using techniques similar those used in symbolic model checking (8). UCLID has been used to verify a variety of hardware designs, including out-of-order microprocessors (7) and cache coherency pro- tocols, as well as abstract synchronization protocols such as Lamport's Bakery algorithm (9). |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1109/MEMCOD.2004.1459805 | SECOND ACM AND IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR CO-DESIGN, PROCEEDINGS |
Keywords | Field | DocType |
binary decision diagram,theorem prover,out of order execution,embedded software,first order logic,modeling language,cache coherence,functional unit,system modeling,engines,propositional logic,logic,instruction set architecture,computability,protocols,data structures,floating point unit,hardware,out of order,formal verification,boolean functions,boolean satisfiability,sat solver | Boolean function,Uclid,Model checking,Programming language,Computer science,Boolean satisfiability problem,Propositional calculus,Modeling language,Binary decision diagram,Theoretical computer science,Formal verification | Conference |
Citations | PageRank | References |
0 | 0.34 | 8 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Randal E. Bryant | 1 | 9204 | 1194.64 |