Edge-Streett/Edge-Rabin Automata Environment for Formal Verification Using Language Containment

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

EECS Department
University of California, Berkeley
Technical Report No. UCB/ERL M94/12
March 1994

http://www2.eecs.berkeley.edu/Pubs/TechRpts/1994/ERL-94-12.pdf

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},
    Institution = {EECS Department, University of California, Berkeley},
    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