For clock and data transitions in close temporal proximity, synchronous memory elements potentially enter metastability, which leads to unintended output behavior. Although respective analyses in literature have already derived suitable explanations, almost all of them modeled the control (clock) signal transition with negligible rise/fall time. In modern circuits this assumption is, however, not reasonable any more. In fact, due to a finite slope, intermediate clock signal values have to be considered during a large share of the storage process, while their concrete impact is not yet sufficiently explored. In this paper we thus use static and dynamic considerations to thoroughly investigate the behavior of a latch for arbitrary analog control, data and output values, i.e., during the storage process. Basic circuit considerations allow us to derive a unified model which identifies the latch as a Schmitt Trigger with vastly varying hysteresis. We verify the correctness of our predictions by comparison to analog SPICE simulations. Finally we are able to generalize our findings and thus provide explanations for yet unexplained behavior reported in literature.

Formal verification plays an important role in the quality assurance of digital circuits. Apart from the now standard equivalence checking between design steps, functional correctness can be proven with model checking. In one approach, a Boolean satisfiability (SAT) problem describing the circuit’s implementation and expected properties is generated for each of a bounded number of time steps and fed to a SAT solver. In synchronous circuits, the time steps correspond to cycles of the global clock. The execution of asynchronous, specifically speed-independent (SI) circuits, however, relies on local handshakes instead of a global time reference. This absence of a global clock requires a different approach for choosing time steps for the SAT problem.This paper presents how bounded, SAT-based model checking can be used on SI asynchronous circuits. We aim to give a general and accessible introduction to this topic, highlight the inherent computational complexity and show that setting up a basic model checker for SI circuits is possible with quite simple means, without any reliance on (expensive) commercial tools. For our reference implementation used in the provided examples we use the open source Z3 solver.

Experimental fault injection is an essential tool in the assessment and verification of fault-tolerance properties. Often, in these experiments it is impossible to reasonably cover the huge parameter space spanned by target state and fault parameters, and compromises or restrictions must be made. This is even more pronounced for asynchronous circuits where a convenient discretization of time through a synchronous clock is not possible. In this paper we present a fault-injection toolset that allows for a very efficient injection and data processing, thus bringing studies with many billions of meaningful injections into asynchronous targets within reach. The key ingredients of our solution are an auto-setup feature capable of optimizing parameter values, seamless distribution of the simulation load to many host computers, and efficient arrangement of the important settings and readings in a database. We will use the example of a comparative study of different asynchronous pipeline styles to motivate the need for such an approach and illustrate its benefits.

Függer et al. (2016) proved that no existing digital circuit model, including those based on pure and inertial delay channels, faithfully captures glitch propagation: for the short-pulse filtration (SPF) problem similar to that of building a one-shot inertial delay, they showed that every member of the broad class of bounded single-history channels either contradicts the unsolvability of SPF in bounded time or the solvability of SPF in unbounded time in physical circuits. In this article, we propose binary circuit models based on novel involution channels that do not suffer from this deficiency. Namely, in sharp contrast to bounded single-history channels, SPF cannot be solved in bounded time with involution channels, whereas it is easy to provide an unbounded SPF implementation. Hence, binary-valued circuit models based on involution channels allow to solve SPF precisely when this is possible in physical circuits. Additionally, using both SPICE simulations and physical measurements of an inverter chain instrumented by high-speed analog amplifiers, we demonstrate that our model provides good modeling accuracy with respect to real circuits as well. Consequently, our involution channel model is not only a promising basis for sound formal verification but also allows to seamlessly improve existing dynamic timing analysis.

Accurate delay models are important for static and dynamic timing analysis of digital circuits, and mandatory for formal verification. However, Függer et al. [IEEE TC 2016] proved that pure and inertial delays, which are employed for dynamic timing analysis in state-of-the-art tools like ModelSim, NC-Sim and VCS, do not yield faithful digital circuit models. Involution delays, which are based on delay functions that are mathematical involutions depending on the previous-output-to-input time offset, were introduced by Függer et al. [DATE'15] as a faithful alternative (that can easily be used with existing tools). Although involution delays were shown to predict real signal traces reasonably accurately, any model with a deterministic delay function is naturally limited in its modeling power. In this paper, we thus extend the involution model, by adding non-deterministic delay variations (random or even adversarial), and prove analytically that faithfulness is not impaired by this generalization. Albeit the amount of non-determinism must be considerably restricted to ensure this property, the result is surprising: the involution model differs from non-faithful models mainly in handling fast glitch trains, where small delay shifts have large effects. This originally suggested that adding even small variations should break the faithfulness of the model, which turned out not to be the case. Moreover, the results of our simulations also confirm that this generalized involution model has larger modeling power and, hence, applicability.

Schmitt-Trigger stages are the method of choice for robust discretization of input voltages with excessive transition times or significant noise. However, they may suffer from metastability. Based on the experience that the cascading of flip-flop stages yields a dramatic improvement of their overall metastability hardness, in this paper we elaborate on the question whether the cascading of Schmitt-Trigger stages can obtain a similar gain. We perform a theoretic analysis that is backed up by an existing metastability model for a single Schmitt-Trigger stage and elaborate some claims about the behavior of a Schmitt-Trigger cascade. These claims suggest that the occurrence of metastability is indeed reduced from the first stage to the second which suggests an improvement. On the downside, however, it becomes clear that metastability can still not be completely ruled out, and in some cases the behavior of the cascade may be less beneficial for a given application, e.g. by introducing seemingly acausal transitions. We validate our findings by extensive HSPICE simulations in which we directly cover our most important claims.

The significant PVT variations seen with modern technologies make synchronous design inefficient. Asynchronous design with its flexible timing is a promising alternative, but prototyping is difficult on the available FPGA platforms which are clock centric and do not provide the required functional primitives like mutual exclusion or Muller C-elements. The solutions proposed in the literature work nicely in principle, but cannot safely handle metastability issues that are inevitable at interfaces even in asynchronous designs. In this paper we propose a reliable implementation of a Schmitt-trigger, which allows to safely convert potential intermediate voltage levels that result from metastability into late transitions that can be reliably handled in the asynchronous domain. Beyond the actual circuit we also discuss the associated routing constraints to make the circuit work properly in spite of the uncertain routing within FPGAs. Furthermore we propose a procedure for an "in situ reliability assessment" of the specific Schmitt-trigger element under consideration, which also applies to metastability containment with high-or low-threshold inverters only. Our proof of concept is based on experimental results for both Xilinx and Altera FPGA platforms.

Fast digital timing simulations based on continuous-time, digital-value circuit models are an attractive and heavily used alternative to analog simulations. Models based on analytic delay formulas are particularly interesting here, as they also facilitate formal verification and delay bound synthesis of complex circuits. Recently, Függer et al. (arXiv:1406.2544 [cs.OH]) proposed a circuit model based on so-called involution channels. It is the first binary circuit model that realistically captures solvability of short-pulse filtration, a non-trivial glitch propagation problem related to building one-shot inertial delays.

Credit schemes are used to establish flow control in NoCs without blocking the communication channel. In traditional implementations one credit is transmitted per data flit, so the credit channel conveys as many messages as the data channel. Our proposed multi-credit scheme transmits credits in bundles of M, yielding one credit transmission per M flits. This saves transitions on the credit channel and promises a slower, more energy efficient implementation. We investigate requirements, options and benefits of this approach; first in theory, and then in a concrete application example, in which we propose a specifically beneficial implementation. Our study confirms that, with a negligible increase in area, our scheme can reduce dynamic energy as well as bandwidth requirements for the credit channel.