links
SixthSense Formal Verification - Publications
-
"Optimal redundancy removal without fixedpoint computation"
M. L. Case, J. Baumgartner, H. Mony and R. L. Kanzelman
Formal Methods in Computer Aided Design, 2011.
[pdf]
-
"Approximate reachability with combined symbolic and ternary simulation"
M. L. Case, J. Baumgartner, H. Mony and R. L. Kanzelman
Formal Methods in Computer Aided Design, 2011.
[pdf]
-
"Hybrid verification of a hardware modular reduction engine"
J. Sawada, P. Sandon, V. Paruthi, J. Baumgartner, M. L. Case and H. Mony
Formal Methods in Computer Aided Design, 2011.
[pdf]
-
"Coping with Moore's Law (and More): Supporting Arrays in State-of-the-Art Model Checkers"
J. Baumgartner, M. L. Case and H. Mony
Formal Methods in Computer Aided Design, 2010.
-
"Enhanced Verification by Temporal Decomposition"
M. L. Case, H. Mony, J. Baumgartner and R. Kanzelman
Formal Methods in Computer Aided Design, 2009.
-
"Scalable Conditional Equivalence Checking: An Automated Invariant-Generation Based Approach"
J. Baumgartner, H. Mony, M. Case, J. Sawada and K. Yorav
Formal Methods in Computer Aided Design, 2009.
-
"Scalable Liveness Checking via Property-Preserving Transformations"
J. Baumgartner and H. Mony,
Design Automation and Test in Europe, 2009.
-
"Speculative-Reduction based Scalable Redundancy Identification"
H. Mony, J. Baumgartner, A. Mishchenko and R. K. Brayton,
Design Automation and Test in Europe, 2009.
-
"Optimal Constraint-Preserving Netlist Simplification"
J. Baumgartner, H. Mony and A. Aziz,
Formal Methods in Computer-Aided Design, 2008.
-
"Invariant Strengthened Elimination of Dependent State Elements"
M. L. Case, A. Mishchenko, R. K. Brayton, J. Baumgartner and H. Mony,
Formal Methods in Computer-Aided Design, 2008.
-
"Merging Nodes Under Sequential Observability"
M. L. Case, V. N. Kravets, A. Mishchenko and R. K. Brayton,
Design Automation Conference, 2008.
-
"Formal Verification of Partial Good Self-Test Fencing Structures"
A. Seigler, G. V. Huben and H.Mony,
Formal Methods in Computer-Aided Design, 2007.
-
"Enabling Large-Scale Pervasive Logic Verification through Multi-Algorithmic Formal Reasoning."
J. Baumgartner,
T. Gloekler,
D. Shanmugam,
R. Seigler,
G. V. Huben,
H. Mony,
P. Roessler, and
B. Ramanandray,
Formal Methods in Computer-Aided Design, San Jose, CA. November 2006.
-
"Scalable Sequential Equivalence Checking across Arbitrary Design Transformations."
-
"Automatic Verification of Fused-Multiply-Add FPUs."
C. Jacobi, K. Weber, V. Paruthi, and J. Baumgartner,
Design Automation and Test in Europe, 2005.
-
"Maximal Input Reduction of Sequential Netlists via Synergistic Reparameterization and Localization Strategies."
J. Baumgartner and H. Mony,
Correct Hardware Design and Verification Methods, 2005.
-
"Exploiting Constraints in Transformation-Based Verification."
H. Mony, J. Baumgartner and A. Aziz,
Correct Hardware Design and Verification Methods, 2005.
-
"Efficient Symbolic Simulation via Dynamic Scheduling, Don't Caring,
and Case Splitting."
V. Paruthi, C. Jacobi and K. Weber,
Correct Hardware Design and Verification Methods, 2005.
-
"Scalable Compositional Minimization via Static Analysis."
F. A. Zaraket, J. Baumgartner and A. Aziz,
International Conference on Computer-Aided Design, 2005.
-
"Exploiting Suspected Redundancy without Proving It"
H. Mony, J. Baumgartner, V. Paruthi, R. Kanzelman,
Design Automation Conference , 2005.
-
"Scalable Automated Verification via Expert-System Guided Transformations."
H. Mony, J. Baumgartner, V. Paruthi, R. Kanzelman and A. Kuehlmann,
Conference on Formal Methods in Computer-Aided Design, 2004.
-
"Enhanced Diameter Bounding via Structural Transformation."
J. Baumgartner and A. Kuehlmann,
Design Automation and Test in Europe, 2004.
-
"An Abstraction Algorithm for Verification of Level-Sensitive Latch-Based Netlists."
J. Baumgartner, T. Heyman, V. Singhal, and A. Aziz,
Journal of Formal Methods in System Design, Volume 23, pp. 39-65, 2003.
-
"Robust Boolean Reasoning for Equivalence Checking and Functional
Property Verification."
A. Kuehlmann, V. Paruthi, F. Krohm and M.K. Ganai,
IEEE Transactions on Computer-Aided Design of Integrated Circuits
and Systems, Volume 21, pp. 1377-1394, December 2002.
-
"Property Checking via Structural Analysis."
J. Baumgartner, A. Kuehlmann, and J. Abraham,
Conference on Computer-Aided Verification, 2002.
-
"Circuit Based Boolean Reasoning."
A. Kuehlmann, M.K. Ganai, and V. Paruthi,
Design Automation Conference, 2001.
-
"Design of a Pointerless BDD Package."
Geert Janssen,
International Workshop on Logic & Synthesis, 2001.
-
"Transformation-Based Verification Using Generalized Retiming."
A. Kuehlmann and J. Baumgartner,
Conference on Computer-Aided Verification, 2001.
-
"Min-Area Retiming on Flexible Circuit Structures."
J. Baumgartner and A. Kuehlmann,
International Conference on Computer-Aided Design, 2001.
-
"An Abstraction Algorithm for Verification of Generalized C-Slow Designs."
J. Baumgartner, A. Tripp, A. Aziz, V. Singhal, and F. Andersen,
Conference on Computer-Aided Verification, 2000.
-
"Equivalence Checking combining a Structural SAT-solver, BDDs and
Simulation."
V. Paruthi and A. Kuehlmann,
International Conference on Computer Design, 2000.
-
"On-the-Fly Compression of Logical Circuits."
M.K. Ganai and A. Kuehlmann,
International Workshop on Logic & Synthesis, 2000.
-
"Model Checking the IBM Gigahertz Processor: An
Abstraction Algorithm for High-Performance Netlists."
J. Baumgartner, T. Heyman, V. Singhal, and A. Aziz,
Conference on Computer-Aided
Verification, 1999.
-
"Equivalence Checking using Cuts and Heaps."
A. Kuehlmann and F. Krohm,
Design Automation Conference, 1997.
-
"The Use of Random Simulation in Formal Verification."
F. Krohm, A. Kuehlmann, and A. Mets,
International Conference on Computer Design, 1996.
-
"On Invariants to Characterize the State Space for Sequential Logic Synthesis and Formal Verification Invariant-Strengthened Elimination of Dependent State Elements"
Michael L Case,
PhD Thesis. The University of California, Berkeley, CA, 2009.
-
"Sequential Redundancy Identification using Transformation-Based Verification"
Hari Mony,
PhD Thesis. The University of Texas, Austin, TX, 2008.
-
"Automatic Structural Abstraction Techniques for Enhanced
Verification."
J. Baumgartner,
PhD Thesis. The University of Texas, Austin, TX, 2002.