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...

• Type: Conference
• Year: 2007
• Where: ICSE
• Authors: Fadi A. Zaraket, Adnan Aziz, Sarfraz Khurshid
• Keywords: Alloy Analyzer, ICSE 2007, Sequential Circuit Analyzer, Sequential Circuits, Software Engineering