Rigorously modeling self-stabilizing fault-tolerant circuits: An ultra-robust clocking scheme for systems-on-chip

Danny Dolev; Matthias Függer; Markus Posch; Ulrich Schmid; Andreas Steininger; Christoph Lenzen

doi:10.1016/j.jcss.2014.01.001

Rigorously modeling self-stabilizing fault-tolerant circuits: An ultra-robust clocking scheme for systems-on-chip

J Comput Syst Sci. 2014 Jun;80(4):860-900. doi: 10.1016/j.jcss.2014.01.001.

Authors

Danny Dolev¹, Matthias Függer², Markus Posch², Ulrich Schmid², Andreas Steininger², Christoph Lenzen³

Affiliations

¹ School of Engineering and Computer Science, The Hebrew University of Jerusalem, Edmond Safra Campus, 91904 Jerusalem, Israel.
² Department of Computer Engineering, Vienna University of Technology, Treitlstrasse 3, 1040 Vienna, Austria.
³ Computer Science and Artificial Intelligence Laboratory, Massachusetts Institute of Technology, 32 Vassar Street, 02139 Cambridge, MA, USA.

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.

Keywords: Byzantine fault-tolerance; Clock synchronization; Dependability; Experiments; Hardware implementation; Hybrid state machines; Metastability; Modeling framework; Self-stabilization; Theoretical analysis.