An equivalency testing system, for formally comparing an RTLM and HLM, is presented. RTLM and HLM are first converted into DFGs RTLM.sub.DFG and HLM.sub.DFG. RTLM.sub.DFG and HLM.sub.DFG are then put into timestep form and are called RTLM.sub.ts and HLM.sub.ts. A test bench CS.sub.ts is selected that couples RTLM.sub.ts and HLM.sub.ts. The combination of RTLM.sub.ts[t], HLM.sub.ts[t] and CS.sub.ts[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 HLM.sub.ts[t] determined by partial execution of the HLM. CS.sub.ts can be selected depending upon a classification of RTLM.sub.ts and HLM.sub.ts. Techniques for classifying RTLM.sub.ts and HLM.sub.ts, and for selecting a suitable CS.sub.ts, are presented. The classifications can operate on non-DFG representations. The CS.sub.ts generation techniques can be used with any formal analysis technique.