| 摘要 |
An equivalency testing system, for formally comparing an RTLM and HLM, is presented. RTLM and HLM are first converted into DFGs RTLMDFG and HLMDFG. RTLMDFG and HLMDFG are then put into timestep form and are called RTLMts and HLMts. A test bench CSts is selected that couples RTLMts and HLMts. The combination of RTLMts[t], HLMts[t] and CSts[t] can have parts designated as datapath. Parts designated as datapath can be subject to a form of equivalence checking that seeks to prove equivalence by a form of inductive theorem proving. The theorem proving starts from initial conditions for HLMts[t] determined by partial execution of the HLM. CSts can be selected depending upon a classification of RTLMts and HLMts. Techniques for classifying RTLMts and HLMts, and for selecting a suitable CSts, are presented. The classifications can operate on non-DFG representations. The CSts generation techniques can be used with any formal analysis technique.
|
