title: Rigorously modeling self-stabilizing fault-tolerant circuits: An ultra-robust clocking scheme for systems-on-chip.
abstract: We present the first implementation of a distributed clock generation scheme for Systems-on-Chip that recovers from an unbounded number of arbitrary transient faults despite a large number of arbitrary permanent faults. We devise self-stabilizing hardware building blocks and a hybrid synchronous/asynchronous state machine enabling metastability-free transitions of the algorithm's states. We provide a comprehensive modeling approach that permits to prove, given correctness of the constructed low-level building blocks, the high-level properties of the synchronization algorithm (which have been established in a more abstract model). We believe this approach to be of interest in its own right, since this is the first technique permitting to mathematically verify, at manageable complexity, high-level properties of a fault-prone system in terms of its very basic components. We evaluate a prototype implementation, which has been designed in VHDL, using the Petrify tool in conjunction with some extensions, and synthesized for an Altera Cyclone FPGA.
authors.affiliation: School of Engineering and Computer Science, The Hebrew University of Jerusalem, Edmond Safra Campus, 91904 Jerusalem, Israel.
authors.forename: Danny
authors.initials: D
authors.lastname: Dolev
authors.affiliation: Department of Computer Engineering, Vienna University of Technology, Treitlstrasse 3, 1040 Vienna, Austria.
authors.forename: Matthias
authors.initials: M
authors.lastname: Függer
authors.affiliation: Department of Computer Engineering, Vienna University of Technology, Treitlstrasse 3, 1040 Vienna, Austria.
authors.forename: Markus
authors.initials: M
authors.lastname: Posch
authors.affiliation: Department of Computer Engineering, Vienna University of Technology, Treitlstrasse 3, 1040 Vienna, Austria.
authors.forename: Ulrich
authors.initials: U
authors.lastname: Schmid
authors.affiliation: Department of Computer Engineering, Vienna University of Technology, Treitlstrasse 3, 1040 Vienna, Austria.
authors.forename: Andreas
authors.initials: A
authors.lastname: Steininger
authors.affiliation: Computer Science and Artificial Intelligence Laboratory, Massachusetts Institute of Technology, 32 Vassar Street, 02139 Cambridge, MA, USA.
authors.forename: Christoph
authors.initials: C
authors.lastname: Lenzen
keywords: Byzantine fault-tolerance; Clock synchronization; Dependability; Experiments; Hardware implementation; Hybrid state machines; Metastability; Modeling framework; Self-stabilization; Theoretical analysis