Advertisement

Manipulations of FSMs Represented as Sequential Circuits

  • Tiziano Villa
  • Nina Yevtushenko
  • Robert K. Brayton
  • Alan Mishchenko
  • Alexandre Petrenko
  • Alberto Sangiovanni-Vincentelli
Chapter

Abstract

In many cases, hard computational problems can be reformulated using decomposition and partitioning, which can lead to computational advantages. An example is image computation, which is a core computation in formal verification. In its simplest form, the image of a set of states is computed using the formula:
$$\begin{array}{rcl} Img(ns) = {\exists }_{i,cs}\ [T(i,cs,ns)\,.\,\xi (cs)],& & \\ \end{array}$$
where T(i, cs, ns) is the transition relation, ξ(cs) is the set of current states, i is the set of input variables, and cs(ns) is the set of current (next) state variables. The image, Img(ns), is the set of states reachable in one transition under all possible inputs from the current states, ξ(cs), using the state transition structure given by T(i, cs, ns).

Keywords

Transition Relation Reachable State State Transition Structure Subset State Deterministic Automaton 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Copyright information

© Springer Science+Business Media, LLC 2012

Authors and Affiliations

  • Tiziano Villa
    • 1
  • Nina Yevtushenko
    • 2
  • Robert K. Brayton
    • 3
  • Alan Mishchenko
    • 4
  • Alexandre Petrenko
    • 5
  • Alberto Sangiovanni-Vincentelli
    • 4
  1. 1.Dipartimento D’InformaticaUniversità di VeronaVeronaItaly
  2. 2.Department of EECSTomsk State UniversityTomskRussia
  3. 3.Department of Electrical Engineering and Computer ScienceUniversity of CaliforniaBerkeleyUSA
  4. 4.Department of Electrical Engineering and Computer Science (EECS)University of California, BerkeleyBerkeleyUSA
  5. 5.Computer Research Institute of Montreal (CRIM)MontrealCanada

Personalised recommendations