Sequential Circuits for Relational Analysis

Fadi A. Zaraket, Adnan Aziz, Sarfraz Khurshid

DOI 10.1109/icse.2007.75 dblp

Abstract

The alloy tool-set has been gaining popularity as an alternative to traditional manual testing and checking for design correctness. Alloy uses a first-order relational logic for modeling designs. The alloy analyzer translates alloy formulas for a given scope, i.e., a bound on the universe of discourse, to Boolean formulas in conjunctive normal form (CNF), which are subsequently checked using prepositional satisfiability solvers. We present SERA, a novel algorithm that compiles a relational logic formula for a given scope to a sequential circuit. There are two key advantages of sequential circuits: they form a more succinct representation than CNF formulas, sometimes by several orders of magnitude. Also sequential circuits are amenable to a range of powerful automatic analysis techniques that have no counterparts for CNF formulas. Our experiments show that SERA, used in conjunction with a sequential circuit analyzer, can check formulas for scopes that are an order of magnitude higher than those feasible with the alloy analyzer.

BibTeX

@inproceedings{Zaraket-al:ICSE07,
  author    = {Fadi A. Zaraket and
               Adnan Aziz and
               Sarfraz Khurshid},
  title     = {Sequential Circuits for Relational Analysis},
  booktitle = {ICSE},
  pages     = {13--22},
  publisher = {{IEEE} Computer Society},
  year      = {2007},
}

Sequential Circuits for Relational Analysis

Abstract

Related papers