Digital hardware circuit logical error diagnosis mechanism

Abstract

The invention discloses an improved digital hardware circuit diagnosis mechanism. According to the digital hardware circuit diagnosis mechanism, an equivalence checking method based on satiable increment is applied to error diagnosis, certain candidate areas are excluded by means of similarity of internal structures of candidate areas, and then processing speed of error checking is improved. According to the digital hardware circuit diagnosis mechanism, the stability and reliability of design are systematically improved by means of the combination of various formalized methods such as the increment equivalence checking method, a logic simulation method and a Boolean satisfiability method.

Description

technical field [0001] The invention relates to a formal verification method belonging to a digital hardware circuit, in particular to a logic error diagnosis mechanism of a digital hardware circuit. Background technique [0002] Digital hardware circuits need to be constantly inspected and tested during the design process. Check whether the process design satisfies the given specification. Once the inspection tool finds a design error, it is necessary to diagnose and debug the design error in order to obtain a correct version that meets the design specification. When the inspection tool finds that the design specification is inconsistent with the implemented function, it is necessary to perform error diagnosis, that is, to identify or minimize the suspected error area in the design implementation, and then reduce the potential error area as much as possible through a specific algorithm, that is, the candidate area . [0003] Existing error diagnosis methods can be divided...

AI Technical Summary

Problems solved by technology

There are many studies on simulation-based error diagnosis methods. This type of method has good scalability and can handle large circuits, but it is not accurate enough.

Most formal diagnosis methods based on BDD are limited by the shortcomings of BDD. Although they can identify error areas more accurately, their processing capabilities are very limited. Therefore, a compromise between accuracy and processing capabilities is required.

Images