Asynchronous circuits are a promising type of digital circuit that still see moderate usage in today’s commercial products, which has often been linked to the adaptation challenges that are posed within industry, e.g. time required to develop new tools and train designers versus using existing synchronous tools to quickly meet market demands. Several formal models were introduced to aid with the design of asynchronous circuits, including Burst-Mode (BM) Specifications and Signal Transition Graphs (STGs). BM specifications resemble synchronous Finite State Machines (FSMs) allowing circuit designers to easily adapt and use them, however their circuit implementations may be limited due to declining tool support. STGs have access to well-established tools that produce optimal hazard-free circuit implementations, but they are seen as too different by the industry. In this paper, we present a new ‘co-design’ methodology that bridges the gap between BM specifications and STGs by using a formal model called Burst Automaton (BA). BA is a generic FSM-like model that acts as a framework for enabling interoperability between many different formal models, and offers several benefits that BM specifications and STGs can leverage. Our ‘co-design’ methodology is implemented in Workcraft, and is evaluated on several benchmarks showing an improved synthesis flow.

Burst-mode (BM) formalism is a variant of an asynchronous finite-state machine (FSM) that operates in “BM” timing assumption and offers simple entry into the asynchronous circuit design. However, some of BM’s well-formedness properties, while useful for implementing BM specifications as circuits, are rather restrictive in some important contexts, e.g., BM’s maximal set property (or its analog, extended BM (XBM) formalism’s distinguishability constraint) forbids nondeterministic specifications that are inherent in some design approaches, input and output bursts must alternate meaning BMs are not a proper extension of FSMs with arcs labeled by single events, and BMs cannot express input-output concurrency whereas FSMs can with interleaving. The latter limitation is particularly problematic when interoperability between several formalisms is desirable. In this article, we propose the burst automation (BA) model that is more powerful and yet simpler than BM, by relaxing BM’s well-formedness properties. BA is a proper extension of FSMs, and can express input-output concurrency and nondeterminism. We define BA’s interleaving semantics via its asynchronous reachability graph that is an FSM, and develop three translations from BAs to signal transition graphs (STGs) that preserve strong bisimulation, weak bisimulation, or the language. Former two translations may be exponential, whereas the latter translation is linear. The resulting STG can then be used for verification and synthesis into speed-independent (SI) or quasi-delay-insensitive (QDI) circuits, or for composition with other STGs. The proposed workflow was implemented in Workcraft, and experimental results show an improved synthesis rate and a significant reduction in the literal count.

Generalised fundamental mode is an important timing assumption for implementing digital circuits, where the environment is assumed to wait for the circuit to stabilise before producing new inputs. In particular, Burst-Mode (BM) timing assumption states that the circuit must wait until a complete input burst has arrived and the environment must wait until a complete output burst is produced. However, this timing assumption may be difficult to enforce in a distributed environment, if each part only observes a subset of the circuit’s output burst.In this paper, we address the above by proposing two formal modelling methodologies: 1) Design by Signal Transition Graphs (STGs), and 2) Design by our new model called Burst Automata (BAs). STGs are flexible as they express many behaviours, while BAs extends the BM methodology and enables interoperability between many different models. Our experimental results show improved synthesis success rates and significant reduction in literal count.

In this paper, we present a new workflow that is based on the conversion of Extended Burst-Mode (XBM) specifications to Signal Transition Graphs (STGs). While XBMs offer a simple design entry to specify asynchronous circuits, they cannot be synthesised into speed-independent (SI) circuits, due to the ‘burst mode’ timing assumption inherent in the model. Furthermore, XBM synthesis tools are no longer supported, and there are no dedicated tools for formal verification of XBMs. Our approach addresses these issues, by granting the XBMs access to sophisticated synthesis and verification tools available for STGs, as well as the possibility to synthesise SI circuits. Experimental results show that our translation only linearly increases the model size and that our workflow achieves a much improved synthesis success rate, with a 33% average reduction in the literal count.

Memristors are intensively proposed in many applications, such as biosensors and machine learning. Regarding their analog characteristics, memristance decoder is, therefore, an essential part for every memristor-based system. As memristor is a temperature sensitive device, this work proposes a memristance decoder circuit with self-temperature calibration. Its main building block is a comparator which is based on current mode circuit to achieve high performance at low power. The design provides configurable precision based on the available energy and supports both synchronous and asynchronous schemes. Moreover, the VTEAM model is modified to include the temperature effect on the memristance in the analysis. The simulation results, based on UMC 65nm low-leakage CMOS technology, show the following comparator's characteristics: 1.70% maximum offset, 2.91ns worst case latency, 343MHz maximum frequency and 48.79fJ maximum energy per comparison. Monte Carlo simulation shows the metastable state in determining the memristor value. This can be solved by extending the clock period or applying a metastability resolver. The proposed memristor model reveals that memristance at high resistive state degrades quadratically with the rise of the temperature and at 85C nearly reaches the memristance of low resistive state.

Analog and mixed signal (AMS) electronics becomes increasingly complex and needs to be digitally enhanced by its own control circuitry. The RTL synthesis flow routinely used for digital logic is, however, optimized for synchronous data processing and produces inefficient control for AMS. In this paper, we demonstrate the evident benefits of asynchronous circuits in the context of AMS systems, and propose an asynchronous design for analog electronics (A4A) flow for their specification, synthesis, and formal verification. A library of specialized analog-to-asynchronous (A2A) components is developed for interfacing analog and asynchronous worlds. A4A flow is automated in the Workcraft framework and evaluated using a multiphase buck converter case study, where A2A components are employed to sanitize analog sensor readings. Timing analysis of asynchronous buck control shows improved response time: 4× reaction to high-load and 7× to under-voltage condition, compared with a 333 MHz clocked controller (to achieve a similar response time, a clocked controller would require ~3 GHz frequency). The simulation results of a 4-phase asynchronous buck demonstrate improved voltage ripple and peak current -16% and 12% reduction, respectively. These benefits lead to the higher efficiency of power conversion, and can be traded off for the cost of analog components, e.g., coils. Moreover, the use of the proposed design flow and tools helps to improve design productivity and overall robustness of AMS circuits.

Pipelining is a widely used approach to the design of high-throughput computation systems, where the slowest component is decomposed into a set of sequentially connected parts that are executed in parallel on successive items of the incoming dataflow. Such dataflow pipelines are often designed to be dynamically reconfigurable to process data items differently depending on their contents and/or to adjust to the application requirements in runtime. Reconfigurable synchronous pipelines are widely used and well studied, and are supported by industrial EDA tools. On the other hand, reconfigurable asynchronous pipelines received much less attention and their industrial adoption is low due to the lack of mature automation support. In this article, we present a model and tool support for the design and verification of reconfigurable asynchronous pipelines. The tool is open source and is available as a plugin for the WORKCRAFT toolset. We validate the presented approach by designing and fabricating a test chip (TSMC 90 nm) that demonstrates the benefits and costs of dynamic reconfigurability, as well as highlights the resilience of asynchronous pipelines.

Dataflow pipelines are widely used in the design of high-throughput computation systems. Real-life applications often require dynamically reconfigurable pipelines to differently process data items or adjust to the current operating mode. Reconfigurable synchronous pipelines are known since 1980s and are well supported by formal models and tools. Reconfigurable asynchronous pipelines on the other hand, have neither a formal behavioural model, nor mature EDA support, making them unattractive to industry. This paper presents a model and an open-source tool for the design and verification of reconfigurable asynchronous pipelines, and validates this approach in silicon.

This paper presents a way to realize a simple yet accurate excitation time model of memristor-based circuits that are in the form of voltage dividers. According to the supported circuit structure, this model is compatible with a wide range of memristor applications, such as delay elements and analog memories. Memristance tuning based on excitation time estimation, i.e. pulse width, instead of using comparators, helps to save area and power. A general-purpose memristance tuning (GMET) circuit is proposed in order to demonstrate the simplicity of the proposed model and to evaluate its accuracy. Our model estimates are compared against the simulation results for the GMET circuit with VTEAM model of the memristor. The results show that the whole-range memristance shifts can be estimated with the worst case average error of 5.49%. They also show the worst case maximum error of 13.25%, which reduces to less than 7% when the operated memristance is higher than 2.5kΩ.

Asynchronous circuits are becoming increasingly important in system design for Internet of Things, where they orchestrate the interface between big synchronous computation components and the analog environment, which is inherently asynchronous and has high uncertainty with respect to power supply, temperature, and long-term aging effects. However, wide adoption of asynchronous circuits by industrial users is hindered by a steep learning curve for asynchronous control models, such as signal transition graphs (STGs), that are developed by the academic community for specification, verification, and synthesis of asynchronous circuits. In this paper, we introduce a novel high-level description language for asynchronous circuits, which is based on behavioral concepts-high-level descriptions of asynchronous circuit requirements, that can be shared, reused, and extended by users, and can be automatically translated to STGs for further processing by conventional asynchronous and synchronous electronic design automation tools, such as Petrify and Mpsat. Our aim is to simplify the process of capturing system requirements in the form of a formal specification, and to promote behavioral concepts as a means for design reuse. The proposed design flow is fully automated in open-source toolsuite Workcraft, and is applied to the development of an asynchronous power regulator.

Analog/mixed-signal (AMS) systems are rapidly expanding in all domains of information and communication technology. They are a critical part of the support for large-scale high-performance digital systems, provide important functionalities in medium-scale embedded and mobile systems, and act as a core organ of autonomous electronics such as sensor nodes. Analog and digital parts are closely intermixed, hence demanding AMS design methods and tools to be more holistic. In particular, the emergence of "little digital" electronics inside or near analog circuitry calls for the increasing use of asynchronous logic. To cope with the growing complexity of AMS designs, formal methods are required to complement traditional simulation approaches. This paper presents an overview of the state-of-the-art in AMS formal verification and asynchronous design that enables the development of analog/asynchronous co-design methods. One such co-design methodology is exemplified by the LEMA-Workcraft workflow currently under development by the authors.

Approximate arithmetic has recently emerged as a promising paradigm for many imprecision-tolerant applications. It can offer substantial reductions in circuit complexity, delay and energy consumption by relaxing accuracy requirements. In this paper, we propose a novel energy-efficient approximate multiplier design using a significance-driven logic compression (SDLC) approach. Fundamental to this approach is an algorithmic and configurable lossy compression of the partial product rows based on their progressive bit significance. This is followed by the commutative remapping of the resulting product terms to reduce the number of product rows. As such, the complexity of the multiplier in terms of logic cell counts and lengths of critical paths is drastically reduced. A number of multipliers with different bit-widths (4-bit to 128-bit) are designed in SystemVerilog and synthesized using Synopsys Design Compiler. Post-synthesis experiments showed that up to an order of magnitude energy savings, and reductions of 65% in critical delay and almost 45% in silicon area can be achieved for a 128-bit multiplier compared to an accurate equivalent. These gains are achieved with low accuracy losses estimated at less than 0.00071 mean relative error. Additionally, we demonstrate the energy-accuracy trade-offs for different degrees of compression, achieved through configurable logic clustering. In evaluating the effectiveness of our approach, a case study image processing application showed up to 68.3% energy reduction with negligible losses in image quality expressed as peak signal-to-noise ratio (PSNR).

Analog and mixed signal (AMS) electronics becomes increasingly complex and needs to be digitally enhanced by its own control circuitry. The RTL synthesis flow routinely used for digital logic is however optimized for synchronous data processing and produces inefficient control for AMS. In this paper we demonstrate the evident benefits of asynchronous circuits in the context of AMS systems, and propose an asynchronous design for analog electronics (A4A) flow for their specification, synthesis, and formal verification. A library of specialized analog-to-asynchronous (A2A) components is developed for interfacing analog signals to asynchronous control. A4A flow is automated in the Workcraft framework and evaluated using a multiphase buck converter case study. The simulation results show improved response time, voltage ripple, and peak current of the buck when controlled asynchronously. These benefits lead to the higher efficiency of power conversion, and can be traded off for the cost of analog components. A4A flow, A2A interfaces, and Workcraft tools are used for development of power converters at Dialog Semiconductor.

In this paper, a novel globally asynchronous locally synchronous (GALS) modeling and verification tool is introduced for xMAS circuits. The tool provides a structured environment for GALS in which organization of the modeling and verification enables it to handle a variety of implementation tasks facilitating a process which would otherwise be difficult for the end user. The tool provides verification techniques at different levels. A new unfolding algorithm is presented that uses structured occurrence nets. A novel representation for deadlocks is introduced using deadlock relations enabling the causality of local and global deadlocks to be visualized. This helps in the investigation of total or partial system shutdown. In particular, the approach enables the visualization of point-to-point causality of problems occurring between different parts of the system which are more difficult to analyze. In addition different types of deadlock related to the synchronizer can be detected. The work presented here provides structured visualization capability facilitating the analysis of complex communication systems.

Asynchronous circuits can be useful in many applications, however, they are yet to be widely used in industry. The main reason for this is a steep learning curve for concurrency models, such Signal Transition Graphs, that are developed by the academic community for specification and synthesis of asynchronous circuits. In this paper we introduce a compositional design flow for asynchronous circuits using concepts - a set of formalised descriptions for system requirements. Our aim is to simplify the process of capturing system requirements in the form of a formal specification, and promote the concepts as a means for design reuse. The proposed design flow is applied to the development of an asynchronous buck converter.

A concurrent system is persistent if throughout its operation no activity which became enabled can subsequently be prevented from being executed by any other activity. This is often a highly desirable (or even necessary) property; in particular, if the system is to be implemented in hardware. Over the past 40 years, persistence has been investigated and applied in practical implementations assuming that each activity is a single atomic action which can be represented, for example, by a single transition of a Petri net. In this paper we investigate the behaviour of GALS (Globally Asynchronous Locally Synchronous) systems in the context of VLSI circuits. The specification of a system is given in the form of a Petri net. Our aim is to re-design the system to optimise signal management, by grouping together concurrent events. Looking at the concurrent reachability graph of the given Petri net, we are interested in discovering events that appear in ‘bundles’, so that they all can be executed in a single clock tick. The best candidates for bundles are sets of events that appear and re-appear over and over again in the same configurations, forming ‘persistent’ sets of events. Persistence was considered so far only in the context of sequential semantics. In this paper, we move to the realm of step based execution and consider not only steps which are persistent and cannot be disabled by other steps, but also steps which are nonviolent and cannot disable other steps. We then introduce a formal definition of a bundle and propose an algorithm to prune the behaviour of a system, so that only bundled steps remain. The pruned reachability graph represents the behaviour of a re-engineered system, which in turn can be implemented in a new Petri net using the standard techniques of net synthesis. The proposed algorithm prunes reachability graphs of persistent and safe nets leaving bundles that represent maximally concurrent steps.

An increasingly large number of safety-critical embedded systems rely on software to prevent and mitigate hazards occurring due to design errors and unexpected interactions of the system with its users and the environment. Implementing a safety instrumented function in the way advocated by the traditional software methods requires an intimate understanding and thorough validation of a complex ecosystem of programming languages, compilers, operating systems and hardware. We propose to consider an alternative where a system designer, for each individual problem, creates in a correct-by-construction manner both the design of a system and its compilation and execution infrastructure. This permits an uninterrupted chain of a formal correctness argument spanning from formalised requirements all the way to the gate-level characterisation of an execution environment. The past decade of advances in verification technology turned the mechanical verification of large-scale models into a reality while the pressure of certification makes the cost of a formally verified development routine increasingly acceptable. The proposal fits the Grand Challenge for Computer Research posed by Hoare in 2003, namely, development of a Verifying Compiler which not only mechanically translates a given program from one language to another but also verifies its correctness according to a formal specification. This allows meeting the most stringent software certification requirements such as SIL 4. We illustrate the vision with a small case-study developed using the Event-B modelling notation and tools.

As processors continue to get exponentially cheaper for end users following Moore’s law, the costs involved in their design keep growing, also at an exponential rate. The reason is ever increasing complexity of processors, which modern EDA tools struggle to keep up with. This paper focuses on the design of Instruction Set Architecture (ISA), a significant part of the whole processor design flow. Optimal design of an instruction set for a particular combination of available hardware resources and software requirements is crucial for building processors with high performance and energy efficiency, and is a challenging task involving a lot of heuristics and high-level design decisions. This paper presents a new compositional approach to formal specification and synthesis of ISAs. The approach is based on a new formalism, called Conditional Partial Order Graphs, capable of capturing common behavioural patterns shared by processor instructions, and therefore providing a very compact and efficient way to represent and manipulate ISAs. The Event-B modelling framework is used as a formal specification and verification back-end to guarantee correctness of ISA specifications. We demonstrate benefits of the presented methodology on several examples, including Intel 8051 microcontroller.

In the last decade we have witnessed a steady trend towards functional diversification of hardware, because an application specific hardware component is a lot easier to design and optimise than a general-purpose one. Therefore, a modern microelectronics system often contains several application specific cores, each targeted for a particular function. As operating conditions issues are becoming more important, we start to see non-functional diversification in terms of performance and energy consumption; it is expected that a system can operate in a wide spectrum of environmental conditions and it should support a hierarchy of energy-saving modes. As a result, "mode-specific" processing cores are gaining popularity. The number of possible combinations of functional and nonfunctional variations of hardware components is becoming unmanageable and is leading to inefficient silicon utilisation. In this paper we explore a novel approach to hardware design which allows building computation systems capable of adjusting to operating conditions through dynamic reconfiguration. We demonstrate the approach by designing an asynchronous microprocessor core that can operate in a wide range of supply voltages and can adjust its functionality towards a specific application and operating mode. Our methodology is based on a novel model of hardware description and on self-timed design techniques.

Instruction sets of modern processors contain hundreds of instructions defined on a relatively small set of datapath components and distinguished by their codes and the order in which they activate these components. Optimal design of an instruction set for a particular combination of available hardware components and software requirements is crucial for system performance and is a challenging task involving a lot of heuristics and high-level design decisions. The overall design process is significantly complicated by inefficient representation of instructions, which are usually described individually despite the fact that they share a lot of common behavioural patterns. This paper presents a new methodology for compact graph representation of processor instruction sets, which gives the designer a new high-level perspective for reasoning on large sets of instructions without having to look at each of them individually. This opens the way for various transformation and optimisation procedures, which are formally defined and explained on several examples, as well as practically evaluated on an FPGA platform.

A conversion driven design approach is described. It takes the outputs of mature and time-proven EDA synthesis tools to generate mixed radix datapath circuits in an endeavour to investigate the added relative advantages or disadvantages. An algorithm underpinning the approach is presented and formally described together with m-of-n encoded gate-level implementations. The application is found in a wide variety and overlapping areas of circuit design, here a subset are analysed where the method finds the strongest application: arithmetic circuits and hardware security. The obtained results are reported showing an increase in power consumption but with considerable improvement in resistance to differential power analysis (DPA).

A method for an automated synthesis of low-latency asynchronous controllers is presented. It is based on a direct mapping approach and starts from an initial specification in the form of a signal transition graph (STG). This STG is split into a device and an environment, which synchronize via a communication net that models wires. The device is represented as a tracker and a bouncer. The tracker follows the state of the environment and provides reference points to the device outputs. The bouncer communicates with the environment and generates output events in response to the input events according to the state of the tracker. This two-level architecture provides an efficient interface to the environment and is convenient for subsequent mapping into a circuit netlist. A set of optimization heuristics is developed to reduce the latency and size of the circuit. As a result of this paper, a software tool called OptiMist has been developed. Its low algorithmic complexity allows large specifications to be synthesized, which is not possible for the tools based on state-space exploration. OptiMist successfully interfaces conventional EDA design flow for simulation, timing analysis, and place-and-route

A logic design style known as phase difference-based logic (PDBL) has several benefits with respect to security and testing. An existing design method for PDBL circuits has so far been lacking an important component, a register. In this paper, we present the design of a speed independent PDBL register and a timed PDBL register, which can be used in asynchronous or synchronous circuits. Comparisons are presented in terms of speed, size, and power consumption.

Designing asynchronous circuits by reusing existing synchronous tools has become a promising solution to the problem of poor CAD support in asynchronous world. A straightforward way is to structurally map the gates in a synchronous netlist to their functionally equivalent modules which use delay-insensitive codes. Different trade-offs exist in previous methods between the overheads of the implementations and their robustness. The aim of this paper is to optimise the area of asynchronous circuits using partial acknowledgement concept. We employ this concept in two design flows, which are implemented in a software tool to evaluate the efficiency of the method. The benchmark results show the average reduction in area by 28% and in the number of inter-functional module wires that require timing verification by 67%, compared to NCL-X.

Comparison between synchronous and asynchronous models leads to a protocol-based fault model for asynchronous circuits. Protocol monitoring of the control path is separated from data comparison in the data path. A novel protocol decomposition technique is used to extract simple protocols from behaviour of a complex circuit. This technique is implemented as a software tool. An asynchronous checker model, implementation and simulation results are presented. Coverage of internal faults of the checker is calculated

Dual-rail encoding, return-to-spacer protocol, and hazard-free logic can be used to resist power analysis attacks by making energy consumed per clock cycle independent of processed data. Standard dual-rail logic uses a protocol with a single spacer, e.g., all-zeros, which gives rise to energy balancing problems. We address these problems by incorporating two spacers; the spacers alternate between adjacent clock cycles. This guarantees that all gates switch in every clock cycle regardless of the transmitted data values. To generate these dual-rail circuits, an automated tool has been developed. It is capable of converting synchronous netlists into dual-rail circuits and it is interfaced to industry CAD tools. Dual-rail and single-rail benchmarks based upon the advanced encryption standard (AES) have been simulated and compared in order to evaluate the method and the tool.