The Equivalence Checking For Partial Implementations Of Sequential Circuits

Integrated circuits (ICs) are the base of both informational industry and informational society. With coming of networking and knowledge economy, IC system has conquered a place in almost all areas of our life, and with constantly increasing of the chip complexity, the possibility of design error grows, so it is necessary to validate the IC system. Moreover to design and develop very large scale integrated(VLSI) system needs so much money, material resources and human resources. It would pay too high cost to verify and modify a finished system, so industrial is apt to debug errors earlier in the design process.There are traditional methods (simulation, emulate, testing) and formal verification method, which were proposed in recent years, to verify IC system. As the chip complexity increases year by year, traditional methods cost much system resource but can not insure correctness of the IC system design, so it had pay more attention to the formal verification in both academy and industry.Equivalence checking is one of most useful formal verification methods, which is suit for verify digital circuits system, and which is used to check whether the logic functionality of two circuits are equivalent. With the complexity of the circuits increased, there are unfinished modules and ones ignored by checker, which are called unknown modules. Therefore, it can be divided into two distinct types, complete implemental circuits and partially implemental circuits, based on whether the circuits contain unknown modules; On the other hand, according to the structure of the circuit, it can be divided into combinational circuits and sequential circuits.In this thesis, we give an effective equivalence checking algorithm for partial implementations of sequential circuits. In the algorithm, we first partition the circuit into Logic Cones, do time-frame expansion for sequence cells in Logic Cones, and then convert sequential circuit into combinational circuit, finally use SAT solver to verify the combinational circuit. We used four-valued logic technology to deal with unknown modules in circuits.With the method, we extend the research for equivalence checking of partial implemental sequential circuits, map sequential circuits verification to combinational ones, moreover, the capacity of detecting errors is increased and also the time of verification is reduced.