Method and apparatus for formally checking equivalence using equivalence relationships

摘要

An equivalency testing system, for formally comparing an RTLM and HLM, is presented. RTLM and HLM are first converted into DFGs RTLM_DFG and HLM_DFG. RTLM_DFG and HLM_DFG are then put into timestep form and are called RTLM_ts and HLM_ts. A test bench CS_ts is selected that couples RTLM_ts and HLM_ts. The combination of RTLM_ts[t], HLM_ts[t] and CS_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 that propagates symbolic values indicative of whether a node carries the same data content as another node. The theorem proving starts from initial conditions for HLM_ts[t] determined by partial execution of the HLM. Propagation to a combinational function output can be determined from equivalence relationships between it and another combinational function. Propagation through a multiplexer can produce a conditional symbolic value.