Name
Abstract | ||
|---|---|---|
A c-slow netlist N is one which may be retimed to another netlist N ’, where the number of latches along each wire of N ’ is a multiple of c. Leiserson and Saxe [1, page 54] have shown that by increasing c (a process termed slowdown) and retiming, any design may be made systolic, thereby dramatically decreasing its cycle time. In this paper we develop
a new fully-automated abstraction algorithm applicable to the verification of generalized c-slow flip-flop based netlists; the more generalized topology accepted by our approach allows applicability to a fairly large
class of pipelined netlists. This abstraction reduces the number of state variables and divides the diameter of the model
by c; intuitively, it folds the state space of the design modulo c. We study the reachable state space of both the original and reduced netlists, and establish a c-slow bisimulation relation between the two. We demonstrate how CTL* model checking may be preserved through the abstraction
for a useful fragment of CTL* formulae. Experiments with two components of IBM’s Gigahertz Processor demonstrate the effectiveness
of this abstraction algorithm.
|
Year | DOI | Venue |
|---|---|---|
2000 | 10.1007/10722167_5 | CAV |
Keywords | Field | DocType |
generalized c-slow designs,abstraction algorithm,model checking,cycle time,state space | Kripke structure,Abstraction model checking,Retiming,Netlist,Model checking,Computer science,Algorithm,Theoretical computer science,Bisimulation,State space,Formal verification | Conference |
ISBN | Citations | PageRank |
3-540-67770-4 | 8 | 1.02 |
References | Authors | |
9 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jason Baumgartner | 1 | 9 | 1.39 |
| Anson Tripp | 2 | 8 | 1.02 |
| Adnan Aziz | 3 | 1778 | 149.76 |
| Vigyan Singhal | 4 | 961 | 86.42 |
| Flemming Andersen | 5 | 8 | 1.02 |