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.
The user specifies a location within the HLM where initialization is
finished. The HLM is executed, with procedure calls related to memory
allocation intercepted and allocation information collected. The
initialization techniques can be used with any formal analysis tool
operating on representations derived from an HLM.