- 2011 - present: Employed by Calypto Design Systems where I work on their sequential equivalence checking tool SLEC.
- 2007 - 2011: Employed by IBM to work on a formal verification tool (SixthSense) in Austin, Texas.
- 2004 - 2009: Earned my PhD from UC Berkeley. I was advised by Robert Brayton and studied Computer Aided Design. In 2009 I authored my PhD thesis describing advances in sequential logic synthesis and formal verification.

Alan Mishchenko, Niklas Een, Robert Brayton, Michael Case, Pankaj Chauhan, and Nikhil Sharma.
DATE 2013.

In numerous EDA flows, time-consuming computations are repeatedly applied to sequential
circuits. This motivates developing methods to determine what circuits have been processed already
by a tool. This paper proposes an algorithm for semi-canonical labeling of nodes in a sequential
AIG, allowing problems or sub-problems solved by an EDA tool to be cached with their computed
results. This can speed up the tool when applied to designs with isomorphic components or design
suites exhibiting substantial structural similarity.

Alan Mishchenko, Niklas Een, Robert Brayton, Michael Case, Pankaj Chauhan, and Nikhil Sharma.
IWLS 2012.

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.

The conference presentation is available.

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. 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.

The conference presentation is available.

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.

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

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.

The conference presentation is available.

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

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.

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.

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.

The conference presentation is available.

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.

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.

The conference presentation is available.

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.

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.

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.

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.

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.

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.

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.