JTAG, an IEEE-standard test protocol, is widely used for testing commercial and experimental CMOS chips but appears unused for testing superconducting chips. The test-access-port (TAP) controller described here facilitates the use of JTAG to reduce the cost – in time and effort – of testing superconductive circuits. Our RSFQ-based TAP controller shifts data serially through a scan chain that transfers data in parallel to and from a circuit under test. Suitably designed scan chains can provide initial values to superconducting circuits and retrieve results to explore circuit behavior. A control computer or an internet connection can operate our TAP controller through a simple five-wire interface. Our TAP controller implements the TAP part of IEEE standard 1149.8.1-2012 in an area of only 580 × 280 micrometers, less area than two bonding pads. Our TAP Controller design information and MIT SFQ5ee layout will be freely available.
We present means to initialize, to propagate, and to examine states in an RSFQ circuit that are useful for design as well as for functional test and analysis. Our RSFQ test strategy distinguishes states by the information they carry from computation to computation, and saves costs by ignoring information-free states. To start, stop, and stall operations that are asynchronous, we developed a new variety of RSFQ stateholder, called MrGO after its CMOS counterpart. We include two simulated examples, a clocked pipelined adder for which we test functionality, and an asynchronous ring FIFO for which we analyze throughput.
Self-timed circuits can be modeled in a link-joint style using a formally defined hardware description language. It has previously been shown how functional properties of these models can be formally verified with the ACL2 theorem prover using a scalable, hierarchical method. Here we extend that method to parameterized circuit families that may have loops and non-deterministic outputs. We illustrate this extension with iterative self-timed circuits that calculate the greatest common divisor of two natural numbers, with circuits that perform arbitrated merges non-deterministically, and with circuits that combine both of these.
This chapter explores the design and test of high-speed complementary metal oxide semiconductor (CMOS) self -timed circuits. Section 7.1 describes how the properties of CMOS technology itself limit how fast a self -timed circuit can run. Section 7.2 presents our Link and Joint model, a unified point of view of self -timed circuits that allows reasoning about them independently of circuit families and handshake protocols. The model separates communication and storage, done in Links, from computation and fl ow control, done in Joints. The model also separates actions from states. Special go signals enable or disable Joint actions on an individual basis. The individual go signals make it possible to initialize, start, and stop self -timed operations reliably, which is crucial for design as well as for at -speed test, debug, and characterization. Section 7.3 examines design and test aspects of the Weaver, a self -timed nonblocking 8 x 8 crossbar switch designed using the Link and Joint model. We report measured test results from a working Weaver chip in 40 nm CMOS with speeds up to 6 Giga data items per second. With 72 bit wide data items, this amounts to 3.5 Tera bits per second for the full crossbar.
Granting access to a shared self-timed resource requires a mutual exclusion circuit to resolve contention. All such circuits contain cross-coupled logic gates to decide contested cases on a first-come-first-served basis. An end-of-metastability detector grants a decision only after metastability, if any, ends. This brief contrasts two previously published mutual exclusion designs and offers previously unavailable guides to achieving least uncontested grant delay for each design. The faster design integrates its cross-coupled gates and end-of-metastability detector into a single stage. The slower design pays a time penalty by isolating these two functions in separate sequential logic stages.
This paper presents a methodology for formally verifying the functional correctness of self-timed circuits whose data flows are free of feedback loops. In particular, we formalize the relationship between their input and output sequences. We use the DE system, a formal hardware description language built using the ACL2 theorem-proving system, to specify and verify finite-state-machine representations of self-timed circuit designs. We apply a link-joint paradigm to model self-timed circuits as networks of computations that communicate with each other with protocols. Our approach exploits hierarchical reasoning and induction to support scalability. We demonstrate our methodology by modeling and verifying several data-loop-free self-timed circuits.
Self-timed systems divide nicely into two kinds of components: communication links that transport and store data, and computation joints that apply logic to data. We treat these two types of self-timed components as equally important. Putting communication on a par with computation acknowledges the increasing cost of data transport and storage in terms of energy, time, and area. Our clean separation of data transport and storage from logic simplifies the design and test of self-timed systems. The separation also helps one to grasp how self-timed systems work. We offer this paper in the hope that better understanding of self-timed systems will engage the minds of compiler, formal verification, and test experts.
Formal verification of asynchronous circuits is known to be challenging due to highly non-deterministic behavior exhibited in these systems. One of the main challenges is that it is very difficult to come up with a systematic approach to establishing invariance properties, which are crucial in proving the correctness of circuit behavior. Non-determinism also results in asynchronous circuits having a complex state space, and hence makes the verification task much more difficult than in synchronous circuits. To ease the verification task by reducing non-determinism, and consequently reducing the complexity of the set of execution paths, we impose design restrictions to prevent communication between a module M and other modules while computations are still taking place that are internal to M. These restrictions enable our verification framework to verify loop invariants efficiently via induction and subsequently verify the functional correctness of asynchronous circuit designs. We apply a link-joint paradigm to model asynchronous circuits. Our framework applies a hierarchical verification approach to support scalability. We demonstrate our framework by modeling and verifying the functional correctness of a 32-bit asynchronous serial adder.
This paper introduces ARCtimer, a framework for modeling, generating, verifying, and enforcing timing constraints for individual self-timed handshake components. The constraints guarantee that the component's gate-level circuit implementation obeys the component's handshake protocol specification. Because the handshake protocols are delay-insensitive, self-timed systems built using ARCtimer-verified components are also delay-insensitive. By carefully considering time locally, we can ignore time globally. ARCtimer comes early in the design process as part of building a library of verified components for later system use. The library also stores static timing analysis (STA) code to validate and enforce the component's constraints in any self-timed system built using the library. The library descriptions of a handshake component's circuit, protocol, timing constraints, and STA code are robust to circuit modifications applied later in the design process by technology mapping or layout tools. In addition to presenting new work and discussing related work, this paper identifies critical choices and explains what modular timing verification entails and how it works.
We "naturalize" the handshake communication links of a self-timed system by assigning the capabilities of filling and draining a link and of storing its full or empty status to the link itself. This contrasts with assigning these capabilities to the joints, the modules connected by the links, as was previously done. Under naturalized communication, the differences between Micropipeline, GasP, Mousetrap, and Click circuits are seen only in the links -- the joints become identical; past, present, and future link and joint designs become interchangeable. We also "naturalize" the actions of a self-timed system, giving actions status equal to states -- for the purpose of silicon test and debug. We partner traditional scan test techniques dedicated to state with new test capabilities dedicated to action. To each and every joint, we add a novel proper-start-stop circuit, called MrGO, that permits or forbids the action of that joint. MrGO, pronounced "Mister GO," makes it possible to (1) exit an initial state cleanly to start circuit operation in a delay-insensitive manner, (2) stop a running circuit in a clean and delay-insensitive manner, (3) single- or multi-step circuit operations for test and debug, and (4) test sub-systems at speed.
Sixty-five years ago, Alan Turing produced a proposal for the construction of a general-purpose computer, the Automatic Computing Engine, or ACE. Subsequently built at the U.K. National Physical Laboratory, it was briefly the fastest computer in the world. Although its architecture was quite different from the arrangement proposed by Von Neumann and others that eventually came to dominate the computing landscape, examining it gives us a chance to understand some of the tradeoffs that early computer architects explored. The panel will examine the ACE to provide a setting for the discussions that follow, in which they will explore some of the architectural tradeoffs that have been made in the past, are still being made today, and which will shape the direction of computing in the future. What would Alan Turing have thought about the impact that computers have had on society? What would he have thought about the warehouse-scale computing that makes possible a realization of Vannevar Bush's 1945 Memex vision? What about the possibility of quantum computing? The panelists will discuss these topics as well as the progress and future of academic computer architecture research.
Promoting a clock-free paradigm that fits everything learned about programming since Turing.
We are trapped in a sequential prison. We use sequential character strings to write sequential programs to control sequential computers. No wonder concurrency remains elusive. How did we come to be here? The high cost of vacuum tube logic forced sequence upon early computer builders. Sequential character strings were the economic way to describe what sequential computers should do. Sequential programs controlled the expensive part of the machine, namely logic. The lethargic pace of logic circuits masked the cost of moving data over distance, allowing programming languages to ignore the cost of communication. Today, the time delay and energy cost of communicating over distance dominate modern computers; logic is essentially free. Why then, do programming languages continue to control logic and largely ignore communication? It will take a broad effort to escape our sequential prison, requiring changes in hardware, programming notations and the ways in which they are expressed. Most importantly, it will require recognizing that we are in sequential prison, and planning for an escape.
GasP circuit modules communicate handshake signals in two directions over a single state wire. The 2008 Infinity test chip demonstrated GasP in 90 nm CMOS operating at four giga data items per second, but revealed that state wires about 5000 lambda long retard operation by about 10%. Simulations reported in this paper show that GasP modules will tolerate surprisingly long state wires, albeit at reduced throughput. The modules appear to operate correctly with state wires whose delay exceeds the drive time. With such long wires, the receiving module waits until passive distribution of charge brings the wire within range of the receiver's switching threshold. Having put enough charge into the wire, or vice-versa removed enough charge from it,the sending module may proceed with its next task. This result applies equally to other single-track signaling methods.This behavior calls for a new kind of relative timing constraint to address when the wire charging or discharging process may cease rather than when the signal reaches the far end of the wire.
This paper reports spreadsheet calculations intended to verify the timing of 6-4 GasP asynchronous Network on Chip (NoC) control circuits. The Logical Effort model used in the spreadsheet estimates the delays of each logic gate in the GasP control. The calculations show how these delays vary in response to differing environmental conditions. The important environmental variable is the physical distance from one GasP module to adjacent modules because longer wires present greater capacitance that retards the operation of their drivers. Remarkably, the calculations predict correct operation over a large range of distances provided the difference in the distances to predecessor and successor modules is limited, and predict failure if the distances differ by too much. Experimental support for this view comes from the measured behavior of a test chip called "Infinity" built by Sun Microsystems in 90 nanometer CMOS circuits fabricated at TSMC.