R. Hojati and V. Singhal and Robert K. Brayton

EECS Department, University of California, Berkeley

Technical Report No. UCB/ERL M94/12

1994

We present the edge-Street/ edge-Rabin environment for doing verification using language containment. This environment has a number of desirable properties compared with the L-process/L-automaton environment ([Kur87b]), which is a practical language-containment-based formal verification environment: * It contains the L-environment as a subset. * It can be exponentially more compact than the L-environment. * We present BDD-based algorithms for main verification functions in this environment, and argue that they are efficient. Furthermore, if the specifications come from the L-environment, our algorithms reduce to the algorithms of [HTKB92] and [HBK93] for the L-environment. * It is in some sense maximal, i.e. language containment check for the next natural extension to our environment is NP-complete (as opposed to polynomial.) We have implemented our algorithms in our verification tool, and will present a flexible user interface to this environment.

---

BibTeX citation:

@techreport{Hojati:M94/12,
    Author= {Hojati, R. and Singhal, V. and Brayton, Robert K.},
    Title= {Edge-Streett/Edge-Rabin Automata Environment for Formal Verification Using Language Containment},
    Year= {1994},
    Month= {Mar},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/1994/2511.html},
    Number= {UCB/ERL M94/12},
    Abstract= {We present the edge-Street/ edge-Rabin environment for doing verification using language containment.  This environment has a number of desirable properties compared with the L-process/L-automaton environment ([Kur87b]), which is a practical language-containment-based formal verification environment: * It contains the L-environment as a subset. * It can be exponentially more compact than the L-environment. * We present BDD-based algorithms for main verification functions in this environment, and argue that they are efficient.  Furthermore, if the specifications come from the L-environment, our algorithms reduce to the algorithms of [HTKB92] and [HBK93] for the L-environment. * It is in some sense maximal, i.e. language containment check for the next natural extension to our environment is NP-complete (as opposed to polynomial.) We have implemented our algorithms in our verification tool, and will present a flexible user interface to this environment.},
}

EndNote citation:

%0 Report
%A Hojati, R. 
%A Singhal, V. 
%A Brayton, Robert K. 
%T Edge-Streett/Edge-Rabin Automata Environment for Formal Verification Using Language Containment
%I EECS Department, University of California, Berkeley
%D 1994
%@ UCB/ERL M94/12
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/1994/2511.html
%F Hojati:M94/12