Title :
On the verification of state-coding in STGs
Author :
Lin, K.-J. ; Lin, C.-S.
Author_Institution :
Dept. of Electr. Eng., Nat. Taiwan Univ., Taipei, Taiwan
Abstract :
Theoretical foundations and a verification procedure based on the transitive lock relation are developed to solve the state coding problem wholly on the signal transition graph (STG) domain for STGs containing multicycle signals and conditional behaviors. The problem considered is realizable state coding, which is a more relaxed requirement than unique state coding. For STGs with multicycle signals, single-cycle transformation is proposed to transform the problem into one with single-cycle signals. For STGs with conditional behaviors, two operations, branch reversing and self-loop unfolding, are proposed to significantly simplify the verification process. The proposed algorithmic approaches have been shown to be successful on over 30 examples from academia and industry.<>
Keywords :
asynchronous sequential logic; circuit CAD; directed graphs; encoding; formal verification; sequential circuits; branch reversing; conditional behaviors; multicycle signals; realizable state coding; self-loop unfolding; signal transition graph; single-cycle transformation; transitive lock relation; verification procedure; Design automation; Directed graphs; Encoding; Sequential logic circuits;
Conference_Titel :
Computer-Aided Design, 1992. ICCAD-92. Digest of Technical Papers., 1992 IEEE/ACM International Conference on
Conference_Location :
Santa Clara, CA, USA
Print_ISBN :
0-8186-3010-8
DOI :
10.1109/ICCAD.1992.279388
