Edge-Streett/Edge-Rabin Automata Environment for Formal Verification Using Language Containment
R. Hojatic, 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{Hojatic:M94/12,
Author = {Hojatic, R. and Singhal, V. and Brayton, Robert K.},
Title = {Edge-Streett/Edge-Rabin Automata Environment for Formal Verification Using Language Containment},
Institution = {EECS Department, University of California, Berkeley},
Year = {1994},
URL = {http://www.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 Hojatic, 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://www.eecs.berkeley.edu/Pubs/TechRpts/1994/2511.html %F Hojatic:M94/12