Predicate learning and selective theory deduction for a difference logic solver

Chao Wang, Aarti Gupta, Malay Ganai

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 Scopus citations

Abstract

Design and verification of systems at the Register-Transfer (RT) or behavioral level require the ability to reason at higher levels of abstraction. Difference logic consists of an arbitrary Boolean combination of propositional variables and difference predicates and therefore provides an appropriate abstraction. In this paper, we present several new optimization techniques for efficiently deciding difference logic formulas. We use the lazy approach by combining a DPLL Boolean SAT procedure with a dedicated graph-based theory solver, which adds transitivity constraints among difference predicates on a "need-to" basis. Our new optimization techniques include flexible theory constraint propagation, selective theory deduction, and dynamic predicate learning. We have implemented these techniques in our lazy solver. We demonstrate the effectiveness of the proposed techniques on public benchmarks through a set of controlled experiments.

Original languageEnglish (US)
Title of host publication2006 43rd ACM/IEEE Design Automation Conference, DAC'06
Pages235-240
Number of pages6
DOIs
StatePublished - Dec 1 2006
Externally publishedYes

Publication series

NameProceedings - Design Automation Conference
ISSN (Print)0738-100X

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Control and Systems Engineering

Keywords

  • Decision procedure
  • Difference logic
  • SAT
  • SMT solver

Fingerprint Dive into the research topics of 'Predicate learning and selective theory deduction for a difference logic solver'. Together they form a unique fingerprint.

Cite this