Conference Program    Technical Session

TUESDAY, July 25, 2006, 4:30 PM - 6:30 PM | Room: 304
TOPIC AREA:  SYNTHESIS AND FPGA


   SESSION 14
  Advances in Formal Solvers
  Chair: Jeremy Levitt - Mentor Graphics Corp., San Jose, CA
  Organizers: Alan Hu, Anmol Mathur

  The session focuses on advances in Boolean and word-level solvers at the heart of formal verification tools. The first paper describes a distributed approach to dynamic variable ordering for BDDs. The next paper describes the use of SAT for redundancy removal using output don't-cares for simplifying circuit descriptions for simplifying Boolean reasoning. The third paper presents word-level techniques for efficient solution of difference logic. The final paper in this session proposes a novel framework for extracting illegal states of a sequential circuit and using them during SAT-based induction.

  14.1   Distributed Dynamic BDD Reordering
  Speaker(s): Ziv Nevo - IBM Corp., Haifa, Israel
  Author(s): Ziv Nevo - IBM Corp., Haifa, Israel
Monica C. Farkash - IBM Corp., Austin, TX
  14.2  SAT Sweeping with Local Observability Don't-Cares
  Speaker(s): Qi Zhu - Univ. of California, Berkeley, CA
  Author(s): Qi Zhu - Univ. of California, Berkeley, CA
Nathan B. Kitchen - Univ. of California, Berkeley, CA
Andreas Kuehlmann - Cadence Berkeley Labs, Berkeley, CA
Alberto Sangiovanni-Vincentelli - Univ. of California, Berkeley, CA
  14.3  Predicate Learning and Selective Theory Deduction for a Difference Logic Solver
  Speaker(s): Chao Wang - NEC-Labs America, Princeton, NJ
  Author(s): Chao Wang - NEC-Labs America, Princeton, NJ
Aarti Gupta - NEC-Labs America, Princeton, NJ
Malay Ganai - NEC-Labs America, Princeton, NJ
  14.4  Fast Illegal State Identification for Improving SAT-Based Induction
  Speaker(s): Vishnu C. Vimjam - Virginia Tech., Blacksburg, VA
  Author(s): Vishnu C. Vimjam - Virginia Tech., Blacksburg, VA
Michael S. Hsiao - Virginia Tech., Blacksburg, VA