Model checking of safety properties is fundamental in formal verification. When a safety property is found to hold, the model checker provides (at best) a machine-checkable certificate that gives limited insight to users and little confidence that the check passes for the “right” reasons, rather than due to e.g., vacuity or unjustified assumptions. Recently, inductive validity cores (IVCs) have been developed to address this issue. In this paper, we lift several algorithms from the field of UNSAT core extraction in order to compute minimal IVCs of hardware safety checking problems. The MARCO algorithm extracts all minimal cores of an UNSAT formula by efficiently exploring the formula's power set, and has already been applied to compute IVCs in software safety checking. The CAMUS algorithm for UNSAT core extraction exploits a duality between minimal correction subsets (MCSes) of a formula and minimal UNSAT cores. We adapt the algorithms to the hardware IVC context, construct a hybrid algorithm that subsumes both CAMUS and MARCO, and introduce novel domain-specific optimizations. Several instances of the hybrid algorithm are presented (including CAMUS and MARCO themselves, among other novel variants) and evaluated empirically on hardware model checking competition circuits, demonstrating the practicality of the proposed algorithm.

In the modern design cycle, substantial manual effort is required to correct failed liveness properties due to the limited availability of automated tools. To address this limitation, this paper introduces two techniques to diagnose register transfer level errors that manifest in the form of erroneously unreachable states, which represent a common form of liveness property failure. The first uses steps of reachable state-space over-approximation and traditional debugging to compute a subset of the solutions that make a target state reachable. The second solves a series of unbounded model checking problems using an enhanced model of the circuit's transition relation to compute the complete solution set to the problem. The proposed techniques are complementary to each other and present the user with a configurable tradeoff between runtime and resolution of the returned solution set. Empirical results on OpenCores and HWMCC'15 circuits confirm the effectiveness of the approaches and demonstrate the tradeoffs between them.

Automated debugging techniques can significantly reduce the manual effort required to localize RTL errors. These techniques return to the user a set of RTL locations where a change can correct erroneous behavior. However, each location must be manually investigated. This problem is exacerbated by the increasing amount of failures in the modern regression verification cycle. Recent work in clustering-based revision debugging mitigates this cost by ranking revisions based on their likelihood of having introduced an error. This work presents a perceptron based approach to revision debugging that can be extended to leverage the revision history of a design directly. Perceptrons are trained using labeled revisions from the design history. They are then used to predict the probability that a revision has introduced an error. The proposed methodology performs competitively with the state-of-the-art, but can be extended to handle more features. This allows for an automated regression debug flow integrated with Version Control and Issue Tracking Systems.

In recent years, IC3 has enjoyed wide adoption by academia and industry as an unbounded model checking engine. The core algorithm works by learning lemmas that, given a safe property, eventually converge to an inductive proof. As such, its runtime performance is heavily dependent upon “pushing” (or “promoting”) important lemmas, possibly by discovering additional supporting lemmas. More recently, Quip has emerged to be a complementary extension behind the reasoning capabilities of IC3 as it allows it to target particular lemmas for pushing. This also raises the following question: which lemmas should be promoted? To that end, this paper extends the reasoning capabilities of IC3 and Quip using special SAT queries to find support sets that represent fine-grained information on which lemmas are required to push other lemmas. Further, this paper presents an IC3-based algorithm called Truss (Testing Reachability Using Support Sets) that uses support sets to identify sets of lemmas that may be close to forming an inductive proof. The set is targeted for promotion as a cohesive unit. If any of the lemmas cannot be promoted, the entire set is abandoned and a new set excluding that lemma is found. In the presented framework, there are two reasons why a lemma cannot be promoted: either because it blocks a known reachable state (in which case, the lemma is permanently marked as bad), or because lemma promotion exceeds a specified amount of effort (in which case the lemma is temporarily marked as ugly). Intuitively, the proposed approach allows the algorithm to construct a proof more quickly by focusing on the important yet easily-pushed lemmas. Experiments on the HWMCC'15 benchmark set show a significant improvement against existing practices. Compared to Quip, our algorithm solves 17 more problem instances and it offers an impressive 1.77× speedup.

In modern hardware design, substantial manual effort is required to fix a design when verification discovers a state unreachable. This paper addresses this growing pain where given an unreachable target state, a methodology is presented to return all design locations where a change can be implemented to make the target state reachable. In contrast to previous state reachability rectification techniques that use bounded model checking, our approach addresses the issue using unbounded model checking. It first enhances the circuit transition relation by inserting a novel error model construction at each suspect location. An unbounded model checking algorithm is then applied to the enhanced transition relation to find which of the suspect locations can be changed to make the target state reachable. The use of unbounded model checking allows it to identify the complete problem solution set. As an added benefit, it also returns a proof that no further solution(s) exist in the form of an inductive invariant. Empirical results on industrial designs confirm the theoretical and practical gains of this approach.

Research in concurrent in-memory data structures has focused almost exclusively on models where processes are either reliable, or may fail by crashing permanently. The case where processes may recover from failures has received little attention because recovery from conventional volatile memory is impossible in the event of a system crash, during which both the state of main memory and the private states of processes are lost. Future hardware architectures are likely to include various forms of non-volatile random access memory (NVRAM), creating new opportunities to design robust main memory data structures that can recover from system crashes. In this paper we advance the theoretical foundations of such data structures in two ways. First, we review several known variations of Herlihy and Wing's linearizability property that were proposed in the context of message passing systems but also apply in our NVRAM-based model, we discuss the limitations of these properties with respect to our specific goals, and we propose an alternative correctness condition called recoverable linearizability. Second, we discuss techniques for implementing shared objects that satisfy such properties with a focus on wait-free implementations. Specifically, we demonstrate how to achieve different variations of linearizability in our model by transforming two classic wait-free constructions.