Mike Case

Optimal Redundancy Removal without Fixedpoint Computation

Michael Case, Jason Baumgartner, Hari Mony, and Robert Kanzelman. FMCAD 2011.

Industrial verification and synthesis tools routinely identify and eliminate redundancies from logic designs. In the former case, redundancy removal yields critical speedups to the overall verification process. In the latter case, redundancy removal constitutes a primary mechanism to optimize the final fabricated circuit. Redundancy identification frameworks often utilize a greatest-fixedpoint iteration, initially postulating a set of candidate redundancies to be conjunctively proved then refining candidates based upon failed proof attempts. Such procedures generally do not yield any soundly-proved redundancies until a fixedpoint is achieved. In this paper, we overcome this drawback by augmenting the fixedpoint procedure with a set of efficient techniques to track dependencies between candidate redundancies. This approach enables the identification of an optimal subset of valid redundancies before the fixedpoint is reached, and may also be used to reduce the number of computations within the fixedpoint procedure. We apply our techniques to enhance $k$-induction as well as a more general transformation-based verification flow. For induction, we demonstrate up to 75% reduction in runtime and 97% reduction in the number of inductive proofs. For the more general flow, we demonstrate up to 90% reduction in runtime and 80% reduction in the total number of proof obligations.

The conference presentation is available.

Approximate Reachability With Combined Symbolic And Ternary Simulation

Michael Case, Jason Baumgartner, Hari Mony, and Robert Kanzelman. FMCAD 2011.

Logic synthesis and formal verification both rely on scalable reachable state characterization for numerous purposes. One popular technique is over-approximate reachability analysis using an iterative ternary simulation. This method trades precision of reachability characterization for a high degree of computational efficiency. Although effective on many industrial designs, it breaks down when the design has registers that have complex initial states or has extremely deep deterministic subcircuits. In this paper, we improve upon the precision of ternary simulation-based approximate reachability while retaining its scalability by representing certain variables as symbols vs. {\em unknowns}, and by selectively saturating subcircuits which would otherwise preclude convergence. These techniques are particularly beneficial for enhancing the scalability of industrial sequential equivalence checking problems, occasionally solving such problems outright with no need for more costly and precise analysis.

The conference presentation is available.

Sequential Equivalence Checking Variants of the Hardware Model Checking Competition 2010 Benchmarks

Michael Case

These are modified versions of the Hardware Model Checking Competition (HWMCC) 2010 benchmarks. Specifically, they are customized to reflect trends we see in industrial SEC problems. These benchmarks are utilized in an FMCAD 2011 paper.

Coping with Moore's Law (and More): Supporting Arrays in State-of-the-Art Model Checkers

Jason Baumgartner, Michael Case, and Hari Mony. Appeared at FMCAD 2010.

State-of-the-art hardware model checkers and equivalence checkers rely upon a diversity of synergistic algorithms to achieve adequate scalability and automation. While higher-level decision procedures have enhanced capacity for problems of amenable syntax, little prior work has addressed (1) the generalization of many critical synergistic algorithms beyond bit-blasted representations, nor (2) the issue of bridging higher level techniques to problems of complex circuit-accurate syntax. In this paper, we extend a variety of bit-level algorithms to designs with memory arrays, and introduce techniques to rewrite arrays from circuit-accurate to verification-amenable behavioral syntax. These extensions have numerous motivations, from scaling formal methods to verify ever-growing design components, to enabling hardware model checkers to reason about software-like systems, to allowing state-of-the-art model checkers to support temporally consistent function- and predicate-abstraction

Enhanced Verification by Temporal Decomposition

Michael Case, Hari Mony, Jason Baumgartner, and Robert Kanzelman. Appeared at FMCAD 2009.

This paper addresses the presence of logic which has relevance only during initial time frames in a hardware design. We examine transient logic in the form of signals which settle to deterministic constants after some prefix number of time frames, as well as primary inputs used to enumerate complex initial states which thereafter become irrelevant. Experience shows that a large percentage of hardware designs (industrial and benchmarks) have such logic, and this creates overhead in the overall verification process. In this paper, we present automated techniques to detect and eliminate such irrelevant logic, enabling verification efficiencies in terms of greater logic reductions, deeper Bounded Model Checking (BMC), and enhanced proof capability using induction and interpolation.

The conference presentation is available.

Scalable Conditional Equivalence Checking: An Automated Invariant-Generation Based Approach

Jason Baumgartner, Hari Mony, Michael Case, Jun Sawada, and Karen Yorav. Appeared at FMCAD 2009.

Sequential equivalence checking (SEC) technologies, capable of demonstrating the behavioral equivalence of two designs, have grown dramatically in capacity over the past decades. The ability to efficiently identify and leverage internal equivalence points to reduce the domain of the overall SEC problem is central to SEC scalability. However, conditionally equivalent designs -- within which internal equivalence may not exist under sequential observability don't care conditions -- are notoriously difficult for automated SEC tools. This paper constitutes one of the first attempts to advance the scalability of SEC for conditionally equivalent designs through automated invariant generation, which enables an inductive solution to an otherwise highly noninductive problem. Through careful software engineering and various heuristics, this technique has been demonstrated capable of yielding orders of magnitude speedup on difficult industrial conditional SEC problems, in cases constituting the only method that we have found to achieve an automated solution

On Invariants to Characterize the State Space for Sequential Logic Synthesis and Formal Verification Invariant-Strengthened Elimination of Dependent State Elements

Michael Case, PhD Thesis, April 2009.

Because of the large size of industrial designs, modern sequential logic synthesis and formal verification techniques cannot afford to accurately characterize the state space of a design. This limits the ability to both optimize designs and to formally prove the the designs behave as required.

Invariants are properties that hold in all reachable states. They can be generated in an automated manner, and the set of generated invariants provides a characterization of the design's state space. This characterization can be utilized sequential logic synthesis and formal verification.

This work provides 1) a framework to efficiently generate invariants, 2) extensions to sequential logic synthesis to make it more capable of reducing the size of complex designs, and 3) extensions to formal verification to increase its scalability on complex industrial designs.

The dissertation presentation is available.

Invariant-Strengthened Elimination of Dependent State Elements

Michael Case, Alan Mishchenko, Robert Brayton, Jason Baumgartner, and Hari Mony. Appeared at FMCAD 2008.

This work presents a technology-independent synthesis optimization that is effective in reducing the total number of state elements of a design. It works by identifying and eliminating dependent state elements which may be expressed as functions of other registers. For scalability, we rely exclusively on SAT-based analysis in this process. To enable optimal identification of all dependent state elements, we integrate an inductive invariant generation framework. We introduce numerous techniques to heuristically enhance the reduction potential of our method, and experiments confirm that our approach is scalable and is able to reduce state element count by 12% on average in large industrial designs, even after other aggressive optimizations such as min-register retiming have been applied. The method is effective in simplifying later verification efforts.
The conference presentation is available.

Cut-Based Inductive Invariant Computation

Michael Case, Alan Mishchenko, and Robert Brayton. Appeared at IWLS 2008.

This paper presents a new way of computing inductive invariants in sequential designs. The invariants are useful for strengthening inductive proofs in difficult unbounded model checking instances. Candidate invariants are derived from a set of m-feasible cuts in the logic network and proved by induction. Thus, the proposed computation is very scalable, and it is possible to flexibly trade computational effort for the expressiveness of the proved invariants. Experimental results on several benchmark families show that the proposed strengthening proves many hard properties that are unsolved by other model checkers. The implementation is publicly available in the synthesis and verification system ABC.

Merging Nodes Under Sequential Observability

Michael L. Case, Victor N. Kravets, Alan Mishchenko, and Robert K. Brayton. Appeared in DAC 2008.

This paper presents a new type of sequential technology independent synthesis. Building on the previous notions of combinational observability and sequential equivalence, sequential observability is introduced and discussed. By considering both the sequential nature of the design and observability simultaneously, better results can be obtained than with either algorithm alone. The experimental results show that this method can reduce the technology-independent gate count up to 10% more than the previously best known synthesis techniques.
The conference presentation is available.

Conflict-Guided Simplification for SAT

Michael L. Case, Sanjit A. Seshia, Alan Mishchenko, and Robert K. Brayton. UC Berkeley Technical Report, 2008.

This paper describes a new method to decompose difficult SAT problems into a simpler problem plus a series of resolution proofs. It was applied to Bounded Model Checking (BMC) and the paper shows impressive speedups. Unfortunately, after this paper was submitted to a conference a major bug was found in the implementation. The speedups observed were a result of this bug. All the basic ideas in this work are sound, but the implementation will need more work.

Automated Extraction of Inductive Invariants to Aid Model Checking

Michael L. Case, Alan Mishchenko, and Robert K. Brayton, Appeared in IWLS 2007 and FMCAD 2007.

In this work I expand on my previous work in approximate reachability analysis. I look at the interpolation formal verification technique, a popular algorithm that is troubled by frequent needs to restart after spurious counterexamples are encountered. These counterexamples can be shown to be unreachable through a tailored reachability approximation that is focused only on this one state. This approach is demonstrated to be highly effective in speeding up interpolation. The IWLS conference presentation, the FMCAD conference presentation, and source code are available.

Maintaining A Minimum Equivalent Graph In The Presence of Graph Connectivity Changes

Michael L. Case and Robert K. Brayton, UC Berkeley Technical Report, 2007.

This is a complete re-write of my WG'06 paper that had been rejected. For this work, I developed algorithms to maintain a minimum equivalent graph to keep track of an implication graph. This technique was previously used in my IWLS 2006 paper, but here I present it in a way that doesn't assume knowledge of logic synthesis, and I include lots more details of the underlying graph theory.

Inductively Finding a Reachable State Space Over-Approximation

Michael L. Case, Alan Mishchenko, and Robert K. Brayton, Appeared in IWLS 2006.

I worked on finding candidate Boolean implications between nodes in a sequential design. I implemented an inductive proof technique that will prove as many of these candidates as possible, and the proved set provides an approximation to the set of truly reachable states. This theme is explored in this paper, and the resulting reachability approximation is applied to sequential optimization.

A Practical Way To Maintain A Transitive Reduction

Michael L. Case, Robert K. Brayton, and Alan Mishchenko, UC Berkeley Technical Report, 2006.

This work describes a graph structure called a transitive reduction. This structure enabled me to store candidate implications in a compact, memory-efficient manner in the application described in my IWLS 2006 paper. Unfortunately, this paper was not accepted for publication.

Online Algorithms To Maintain A Transitive Reduction

Michael L. Case, UC Berkeley Class Project, Fall 2006

This is a re-write of my WG 2006 paper. I've invested a lot of time to carefully prove the correctness of my algorithm and also to very carefully study its complexity. I consider this work to be a great improvement over the WG 2006 version.

A Hybrid Model Checker

Michael L. Case, Kelvin Lwin, UC Berkeley Class Project, Spring 2006

In this work I began to explore model checking. Specifically, I took the idea of an over-approximation to the set of reachable states, as presented at IWLS 2006, and applied it to model checking. In a pre-processing step I extract this approximation and use it to bound the search that a model checker must make across the state space.