Carnegie Mellon University
Browse

System Modeling and Verification with UCLID

Download (26.64 kB)
journal contribution
posted on 1988-01-01, 00:00 authored 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

1988-01-01

Usage metrics

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC