Sequential Circuits for Relational Analysis

11 years 11 months ago
Sequential Circuits for Relational Analysis
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 propositional 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 t...
Fadi A. Zaraket, Adnan Aziz, Sarfraz Khurshid
Added 09 Dec 2009
Updated 09 Dec 2009
Type Conference
Year 2007
Where ICSE
Authors Fadi A. Zaraket, Adnan Aziz, Sarfraz Khurshid
Comments (0)