The behavior of any electronic system can be traced back to how its constituting components physically interact with each other. Such low-level interactions explain how specific states of a given circuit are physically possible. Some circuit states can be erroneous, e.g., applying a voltage stress greater than what some device can tolerate. It is of particular importance to know whether such errors can happen on a given circuit, so that required corrections can be made. Identifying errors requires some circuit modeling technique, and a way to explore the state space of the circuit model (which may be very large if at all finite). In this work, we show the limitations of classical verification techniques, and propose a new approach based on formal methods to overcome them. We propose new circuit semantics for transistor-level descriptions from (1) recalling and improving existing semantics, and (2) introducing novel alternate ones. We then demonstrate their usage in our verification framework—which makes use of a satisfiability modulo theories (SMT) solver—to verify specific electric properties of circuits. Specifically, we address the problem of the search for circuit transistors that are subject to electrical overstress (EOS). We draw interesting conclusions by comparing the presented circuit semantics, both formally and via experimental benchmarks.

Hardware verification is crucial to ensure the quality of Integrated Circuits, and prevent costly bugs down the manufacturing flow. Electrical Rule Checking (ERC) is a verification step used to assert that a circuit complies with some electrical rules, from the absence of short-circuits to dedicated constructor rules. In this survey, we provide a global overview of existing ERC techniques at transistor-level, where voltage values are explicit. We propose a new classification method to compare the existing approaches based on their semantic modeling of circuits. This survey precisely describes transistor-level ERC research challenges and existing solutions. We believe it will help structure this research domain by positioning existing approaches with respect to each other. Obviously, a survey should also facilitate technological transfer and this one should help CAD vendors identify the most relevant approaches to integrate in their tools. Finally, we highlight several promising directions to improve the existing solutions.

We present a novel technique for Electrical Rule Checking (ERC) based on formal methods. We define a relational semantics of Integrated Circuits (IC) as a means to model circuits' behavior at transistor-level. We use Z3, a Satisfiability Modulo Theory (SMT) solver, to verify electrical properties on circuits – thanks to the defined semantics. We demonstrate the usability of the approach to detect current leakage due to missing level-shifter on large industrial circuits, and we conduct experiments to study the scalability of the approach.

We consider the verification of electrical properties of circuits to identify potential violations of electrical design rules, also called Electrical Rule Checking (ERC). We present a general approach based on Satisfiability Modulo Theory (SMT) to verify that these errors cannot occur in a given circuit. We claim that our approach is scalable and more precise than existing analyses, like voltage propagation. We applied these techniques to a specific type of errors, the missing level shifters. On an industrial case-study, our technique is able to flag 31 % of the warnings raised by the voltage propagation analysis as being false alarms.

Abstract We consider swarms of asynchronous oblivious robots evolving into an anonymous grid-shaped network. In this context, we investigate optimal (w.r.t. the number of robots) deterministic solutions for the terminating exploration problem. We first show lower bounds in the semi-synchronous model. Precisely, we show that at least three robots are required to explore any grid of at least three nodes, even in the probabilistic case. Then, we show that at least four (resp. five) robots are necessary to deterministically explore a $\bf(2,2)$-Grid (resp. a $\bf(3,3)$-Grid). We then propose deterministic algorithms in the asynchronous model. This latter being strictly weakest than the semi-synchronous model, all the aforementioned bounds still hold in that context. Our algorithms actually exhibit the optimal number of robots that is necessary to explore a given grid. Overall, our results show that except in two particular cases, three robots are necessary and sufficient to deterministically explore a grid of at least three nodes and then terminate. The optimal number of robots for the two remaining cases is four for the $\bf(2,2)$-Grid and five for the $\bf(3,3)$-Grid, respectively.

We study the implementation of data-flow applications on multi-core processor with on-chip shared multi-banked memory. Specifically, we consider the Kalray MPPA2 processor and three applications coded using the industrial toolchain SCADE Suite. We focus on the runtime environment assuming global static scheduling, time-triggered and non-preemptive execution of tasks. Our contributions include (i) a technique to implement SCADE applications compliant with execution models inspired by PREMs (PRe-dictable Execution Models), (ii) an exhaustive comparison of three execution models with and without isolation, and finally (iii) guidelines for predictable implementation of a data-flow application on multi-core processors with shared on-chip memory.

Embedded systems tend to require more and more computational power. Many-core architectures are good candidates since they offer power and are considered more time predictable than classical multi-cores. Data-flow Synchronous languages such as Lustre or Scade are widely used for avionic critical software. Programs are described by networks of computational nodes. Implementation of such programs on a many-core architecture must ensure a bounded response time and preserve the functional behavior by taking interference into account. We consider the top-level node of a Lustre application as a software architecture description where each sub-node corresponds to a potential parallel task. Given a mapping (tasks to cores), we automatically generate code suitable for the targeted many-core architecture. This minimizes memory interferences and allows usage of a framework to compute the Worst-Case Response Time.

Static timing analysis aims at computing a guaranteed upper bound to the Worst-Case Execution Time (WCET) of a program. It requires both an accurate modeling of the hardware, and a precise analysis of the program in order to reject infeasible executions (in particular, all infinite ones). For the actual computation of the worst-case execution, most of the existing tools and methods are based on the Implicit Path Enumeration Technique (IPET), which consist in encoding this search into a numerical optimization problem (Integer Linear Programming, ILP). An interest of this approach is that it naturally integrates the loop bounds. It also allows to implicitly prune infeasible paths, as far as they can be expressed using linear constraints. Several works on the subject are using this ability in order to enhance the WCET estimation: they identify specific property patterns (e.g., implications, exclusions) and propose ad hoc translation into numerical constraints.

This paper addresses the question of producing modular sequential imperative code from synchronous data-flow networks. Precisely, given a system with several input and output flows, how to decompose it into a minimal number of sub-systems executed atomically and statically scheduled without restricting possible feedback loops between input and output?

This paper addresses the problem of designing and implementing complex control systems for real-time embedded software. Typical applications involve different control laws corresponding to different phases or modes, e.g., take-off, full flight and landing in a fly-by-wire control system. On one hand, existing methods such as the combination of Simulink/Stateflow provide powerful but unsafe mechanisms by means of imperative updates of shared variables. On the other hand, synchronous languages and tools such as Esterel or SCADE/Lustre are too restrictive and forbid to fully separate the specification of modes from their actual instantiation with a particular control automaton.

Architecture description languages are used to describe both the hardware and software architecture of an application, at system-level. The basic software components are intended to be developed independently, and then deployed on the described architecture. This separate development of the architecture and of the software raises the problem of early validation of the integrated system.

We present an operational model for describing random reactive systems. Some models have already been proposed for this purpose, but they generally aim at performing global reasoning on systems, such as stochastic analysis, or formal proofs. Our goal is somehow less ambitious, since we are rather interested in executing such models, for testing or prototyping. But on the other hand, the proposed model is not restricted by decidability issues. Therefore it can be more expressive: in particular, our model is not restricted to finite-state descriptions. The proposed model is rather general: systems are described as implicit state/transition machines, possibly infinite, where probabilities are expressed by means of relative weights. The model itself is more an abstract machine than a programming language. The idea is then to propose highlevel, user-friendly languages that can be compiled into the model. We present such a language, based on regular expressions, together with its translation into the model.

The paper addresses the problem of automatizing the production of test sequences for reactive systems. We particularly focus on two points: (1) generating relevant inputs, with respect to some knowledge about the environment in which the system is intended to run; (2) checking the correctness of the test results, according to the expected behavior of the system. We propose to use synchronous observers to express both the relevance and the correctness of the test sequences. In particular, the relevance observer is used to randomly choose inputs satisfying temporal assumptions about the environment. These assumptions may involve both Boolean and linear numerical constraints. A prototype tool called LURETTE has been developed and experimented with, which works on observers written in the LUSTRE programming language.

This paper describes a method to verify safety properties of parameterized linear networks of processes. The method is based on the construction of a network invariant, defined as a fixpoint. Such invariants can often be automatically computed using heuristics based on Cousot's widening techniques. These techniques have been implemented and some non-trivial examples are presented.

The authors describe LUSTRE, a data flow synchronous language designed for programming reactive systems-such as automatic control and monitoring systems-as well as for describing hardware. The data flow aspect of LUSTRE makes it very close to usual description tools in these domains (block-diagrams, networks of operators, dynamical sample-systems, etc.), and its synchronous interpretation makes it well suited for handling time in programs. Moreover, this synchronous interpretation allows it to be compiled into an efficient sequential program. The LUSTRE formalism is very similar to temporal logics. This allows the language to be used for both writing programs and expressing program properties, which results in an original program verification methodology.>