file.pdf (26.64 kB)
Download file

System Modeling and Verification with UCLID

Download (26.64 kB)
journal contribution
posted on 01.01.1988, 00:00 by Randal E. Bryant
Formal verification has had a significant impact on the semiconductor industry, particularly for companies that can devote significant resources to creating and deploying internally developed verification tools. Most existing verifiers model system operation at a detailed bit level. We have developed UCLID, a prototype verifier for infinite-state systems. The UCLID modeling language extends 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 expressive enough to model a wide range of systems, but it still permits a decision procedure where we transform the formula into propositional logic and then use either binary decision diagrams (BDD) or a Boolean satisfiability (SAT) solver.

History

Publisher Statement

All Rights Reserved

Date

01/01/1988

Usage metrics

Exports