Logic design error diagnosis and correction

Logic verification tools are often used to verify a gate-level implementation of a digital system in terms of its functional specification. If the implementation is found not to be functionally equivalent to the specification, it is important to correct the implementation automatically. This paper describes a formal method for the diagnosis and correction of logic design errors in an incorrect gate-level implementation. We use Boolean equation techniques to search for potential error locations. An efficient search and pruning algorithm is developed by introducing the notion of immediate dominator set. Two correction procedures are proposed. Gate correction corrects errors such as wrong gate type, missing inverters, etc.; line correction corrects errors such as missing wires and wrong connections. Our method is robust and covers all, simple design errors described by Abadir et al. (1988). Experimental results for a set of ISCAS and MCNC benchmark circuits demonstrate the effectiveness of the proposed techniques.<>