| Summary: | 碩士 === 國立中山大學 === 電機工程學系研究所 === 92 === High-level finite-state-machine is a behavioral level hardware system design specification method. Each of its state transitions is tagged with a description of an expression executed during the corresponding state transition. In order to verify the equivalence between a high-level finite-state-machine and its deriving low-level finite-state-machine, we can extract expressions executed in state transition sequences from an annotated state to another. Then, the extracted expression can be checked against the corresponding expression in the high-level finite-state-machine for their equivalence.
Past research adopted a simulation-based validation technique to examine expression equivalence. Due to its combinatorial complexity, it can not guarantee hundred percent equivalence for expression passing the test. In this research, we designed software of our expression equivalence verification method applied on the extracted expressions. It consists of software design tasks of tree system functionalities :
1. By applying a normalization method on commutative, associative, and distributive laws, we can transform each expression into an equivalent reduced expression graph. It can reduce the size of the equivalence space to be explored in the equivalence verification process and thus reduce computation time and storage size of explored equivalent expressions.
2. For equivalent expression s explored during the verification process, we can share the common sub-expression structures and form a formal shared expression graph. We can furthermore reduce the storage size of the evolved expressions and facilitate isomorphism checking between them to improve performance.
3. In the shared expression graph, we can match its sub-expressions against axiom patterns and derive corresponding unification. Then, substitute the matched sub-expression with the corresponding axiom template with unified variable values and form a new equivalent expression graph from axiom transformation.
We carried out experiments of this expression equivalence verification method. Experimental results shows that this method obtains the equivalence verification capability to be applied between a hardware system design and its low level design.
|
|---|
