Category: CMUTR
Institution: Department of Computer Science, Carnegie
        Mellon University
Abstract: We significantly reduce the complexity of BDD-based symbolic 
        verification by using partitioned transition relations to 
        represent state transition graphs.
        This method can be applied to both synchronous and asynchronous 
        circuits.
        The times necessary to verify a synchronous pipeline and an
        asynchronous stack are both bounded by a low polynomial in the 
        size of the circuit.
        We were able to handle stacks with over 10 50 reachable states 
        and pipelines with over 10 20 reachable states.
Number: CMU-CS-91-195
Bibtype: TechReport
Month: oct
Author: J. B. Burch
        E. M. Clarke
        D. E. Long
Title: Symbolic Model Checking with Partitioned Transition Relations
Year: 1991
Address: Pittsburgh, PA
Super: @CMUTR