On the verification of state-coding in STGs

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.<>