Author :
Sinha, S. ; Kuehlmann, A. ; Brayton, R.K.
Author_Institution :
California Univ., Berkeley, CA, USA
Abstract :
SPFDs are a mechanism to express flexibility in Boolean networks. Introduced by Yamashita et al. in the context of FPGA synthesis [1996], they were extended later to general combinational networks. We introduce the concept of sequential SPFDs and provide an algorithm to compute them based on a partition of the state bits. The SPFDs, of each component in the partition are used to generate equivalence classes of states. We provide a formal relation between the resulting state classification and the equivalence classes produced by classical state minimization of completely specified machines. The SPFDs, associated with the state bits can be applied for re-encoding the state space. For this, we give an algorithm to re-synthesize the sequential circuit using sequential SPFDs and the new state re-encoding.
Keywords :
Boolean functions; formal verification; logic CAD; logic partitioning; sequential circuits; state-space methods; Boolean networks; equivalence classes; formal relation; partition; sequential SPFDs; sequential circuit; sets of pairs of functions to be distinguished; state bits; state classification; state space re-encoding; Automata; Cows; Explosions; Field programmable gate arrays; Minimization; Network synthesis; Observability; Partitioning algorithms; Sequential circuits; State-space methods;
Conference_Titel :
Computer Aided Design, 2001. ICCAD 2001. IEEE/ACM International Conference on
Conference_Location :
San Jose, CA, USA
Print_ISBN :
0-7803-7247-6
DOI :
10.1109/ICCAD.2001.968602
