Ensuring trust of third-party hardware design with constrained sequential equivalence checking

Globalization of semiconductor design and manufacturing has led to a concern of trust in the final product. The effect of any modifications made by an adversary can be catastrophic in critical applications. Because of the stealthy nature of such insertions, it is extremely difficult to detect them using traditional testing and verification methods. In this paper, we propose a novel technique for detection of malicious alteration(s) in a third party soft intellectual property (IP) using a clever combination of sequential equivalence checking (SEC) and test generation. The use of powerful inductive invariants can prune a large illegal state space, and test generation helps to provide a sensitization path for nodes of interest. Results for a set of hard-to-verify designs show that our method can either ensure that the suspect design is free from the functional effect of any malicious change(s) or return a small group of most likely malicious signals.