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.

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.

This special issue is based on extended versions of the best papers presented at the 39th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2018).Petri Nets 2018 was co-located with the Application of Concurrency to System Design Conference (ACSD 2018).Both were organized by the Interes Institute and Faculty of Electrical Engineering and Information Technology, Slovak University of Technology.The conference took place at the Austria Trend Hotel Bratislava, from June 24 to June 29, 2018.In total, 33 papers were submitted to Petri Nets 2018 by authors from 19 different countries.Each paper was reviewed by three reviewers.The Program Committee (PC) selected 23 papers for presentation: 15 theory papers and 8 tool papers.The authors of the best six papers were invited to submit an extended version of their conference paper for this special issue.The selected papers contained highly innovative and very strong contributions, as was demonstrated by the unanimous support of the reviewers.Also the PC unanimously supported these invitations.After a rigorous review process comprising two rounds of reviewing, the invited papers were accepted.Besides a subset of the original reviewers, we also invited additional reviewers to ensure the best feedback possible.We believe that the papers in this special issue are of high quality and represent the state-of-the-art in their respective fields.The article "Analysis and Synthesis of Weighted Marked Graph Petri Nets" by Raymond Devillers and Thomas Hujsa focuses on an important subclass of persistent Petri nets, the weighted marked graphs (WMGs), also called generalised (or weighted) event (or marked) graphs or weighted T-nets.The authors provide new behavioural properties of WMGs expressed on their reachability graph, notably backward persistence and strong similarities between any two sequences sharing the same starting state and the same destination state.They also propose necessary structural conditions that must be fulfilled by a labelled transition system to be WMG-solvable.Finally, the authors propose a general synthesis method to create a WMG whose reachability graph minimally includes the specification.The article "Operational Semantics, Interval Orders and Sequences of Antichains" by Ryszard Janicki and Maciej Koutny introduces a new general class of nets that can represent both inhibitor and activator nets -called safe nets with context arcs.The authors analyse in detail fundamental relationships between interval sequences and sequences of maximal antichains, and provide simple algorithms that transform one into another.

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 partially observed Petri nets, diagnosis is the task of detecting whether the given sequence of observed labels indicates that some unobservable fault has occurred. Diagnosability is an associated property of the Petri net, stating that in any possible execution, an occurrence of a fault can eventually be diagnosed. In this article, we consider diagnosability under the weak fairness (WF) assumption, which intuitively states that no transition from a given set can stay enabled forever—it must eventually either fire or be disabled. We show that a previous approach to WF-diagnosability in the literature has a major flaw and present a corrected notion. Moreover, we present an efficient method for verifying WF-diagnosability based on a reduction to LTL-X model checking. An important advantage of this method is that the LTL-X formula is fixed—in particular, the WF assumption does not have to be expressed as a part of it (which would make the formula length proportional to the size of the specification), but rather the ability of existing model checkers to handle weak fairness directly is exploited.

Factored planning mitigates the state explosion problem by avoiding the construction of the state space of the whole system and instead working with the system's components. Traditionally, finite automata have been used to represent the components, with the overall system being represented as their product. In this article, we change the representation of components to safe Petri nets. This allows one to use cheap structural operations like transition contractions to reduce the size of the Petri net before its state space is generated, which often leads to substantial savings compared with automata. The proposed approach has been implemented and proved efficient on several factored planning benchmarks. This article is an extended version of our ACSD 2013 paper [Jezequel et al. 2013], with the addition of the proofs and the experimental results of Sections 6 and 7.

Merged processes (MPs) are a recently proposed condensed representation of a Petri net's behaviour similar to branching processes (unfoldings), which copes well not only with concurrency but also with other sources of state space explosion like sequences of choices. They are by orders of magnitude more compact than traditional unfoldings, and yet can be used for efficient model checking. However, constructing complete MPs is difficult, and the only known algorithm is based on building a (potentially much larger) complete unfolding prefix of a Petri net, whose nodes are then merged. Obviously, this significantly reduces their appeal as a representation that can be used for practical model checking. In this paper, we develop an algorithm that avoids constructing the intermediate unfolding prefix and builds a complete merged process directly from a safe Petri net. In particular, a challenging problem of truncating a merged process is solved.

One of the difficulties in designing modern hardware systems is the necessity for comprehending and dealing with a very large number of system configurations, operational modes, and behavioural scenarios. It is often infeasible to consider and specify each individual mode explicitly, and one needs methodologies and tools to exploit similarities between the individual modes and work with groups of modes rather than individual ones. The modes and groups of modes have to be managed in a compositional way: the specification of the system should be composed from specifications of its blocks. This includes both structural and behavioural composition. Furthermore, one should be able to transform and optimise the specifications in a formal way. In this article, we propose a new formalism, called parameterised graphs . It extends the existing conditional partial order graphs (CPOGs) formalism in several ways. First, it deals with general graphs rather than just partial orders. Moreover, it is fully compositional. To achieve this, we introduce an algebra of parameterised graphs by specifying the equivalence relation by a set of axioms, which is proved to be sound, minimal, and complete. This allows one to manipulate the specifications as algebraic expressions using the rules of this algebra. We demonstrate the usefulness of the developed formalism on several case studies coming from the area of microelectronics design.

A new way of constructing N-way arbiters is proposed. The main idea is to perform arbitrations between all pairs of requests, and then make decision on what grant to issue based on their outcomes. Crucially, all the mutual exclusion elements in such

We propose a technique for verification of mobile systems. We translate finite control processes, a well-known subset of π-Calculus, into Petri nets, which are subsequently used formodel checking. This translation always yields bounded Petri nets with a small bound, and we develop a technique for computing a non-trivial bound by static analysis. Moreover, we introduce the notion of safe processes, a subset of finite control processes, for which our translation yields safe Petri nets, and show that every finite control process can be translated into a safe one of at most quadratic size. This gives a possibility to translate every finite control process into a safe Petri net, for which efficient unfolding-based verification is possible. Our experiments show that this approach has a significant advantage over other existing tools for verification of mobile systems in terms of memory consumption and runtime. We also demonstrate the applicability of our method on a realistic model of an automated manufacturing system.

Synthesis of asynchronous circuits from signal transition graphs (STGs) involves resolution of state encoding conflicts by means of refining the STG specification. In this paper, a fully automatic technique for resolving such conflicts by means of insertion of new signals and concurrency reduction is proposed. It is based on conflict cores, i.e., sets of transitions causing encoding conflicts, which are represented at the level of finite and complete unfolding prefixes, and a SAT solver is used to find where in the STG the transitions of new signals should be inserted and to check the validity of concurrency reductions. The experimental results show significant improvements over the state space based approach in terms of runtime and memory consumption, as well as some improvements in the quality of the resulting circuits.

The paper presents a new method for checking unique and complete state coding, the crucial conditions in the synthesis of asynchronous control circuits from signal transition graphs (STGs). The method detects state coding conflicts in an STG using its partial order semantics (unfolding prefix) and an integer programming technique. This leads to huge memory savings compared to methods based on reachability graphs, and also to significant speedups in many cases. In addition, the method produces execution paths leading to an encoding conflict. Finally, the approach is extended to checking the normalcy property of STGs, which is a necessary condition for their implementability using gales whose characteristic functions, are monotonic.