Paper Info
Title
Sequential Circuits for Relational Analysis
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 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 ofmagnitude. 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.
Year
DOI
Venue
2007
10.1109/ICSE.2007.75
ICSE
Keywords
Field
DocType
conjunctive normal form,first order,universe of discourse,encoding,sequential analysis,circuit analysis,relational analysis,system testing,software systems,boolean functions,sequential circuits,logic design
Boolean function,Logic synthesis,Sequential logic,Computer science,Alloy Analyzer,Correctness,Satisfiability,Algorithm,Conjunctive normal form,Network analysis
Conference
ISSN
ISBN
Citations 
0270-5257
0-7695-2828-7
5
PageRank 
References 
Authors
0.43
20
3
Name
Order
Citations
PageRank
Fadi A. Zaraket1429.93
Adnan Aziz21778149.76
Sarfraz Khurshid32892152.88