SixthSense Formal Verification     

links

Geert Janssen photo

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.