ABSTRACT. In this paper we propose and implement a methodology for power reduction in digital circuits, closing the gap between conceptual (by designer) and local (by EDA) clock gating. We introduce a new class of coarse grained local clock gating conditions and develop a method for detecting such conditions and formally proving their correctness. The detection of these conditions relies on architecture characterization and statistical analysis of simulation, all done at the RTL. Formal verification is performed on an abstract circuit model. We demonstrate a significant power reduction from 33 to 40% of total power on a clusterized circuit design for video processing.

ABSTRACT. To simplify the implementation of dataflow systems in hardware, we present a technique for designing latency-insensitive dataflow blocks. We provide buffering with backpressure, resulting in blocks that compose into deep, high-speed pipelines without introducing long combinational paths. Our input and output buffers are easy to assemble into simple unit-rate dataflow blocks, arbiters, and blocks for Kahn networks. We prove the correctness of our buffers, illustrate how they can be used to assemble arbitrary dataflow blocks, discuss pitfalls, and present experimental results that suggest our pipelines can operate at a high clock rate independent of length

ABSTRACT. Loop parallelization techniques for massively parallel processor arrays using one-level tiling are often either I/O- or memory-bounded, exceeding the target architecture's capabilities. Furthermore, if the number of available processing elements is only known at runtime, as in adaptive systems, static approaches fail. To solve these problems, we present a hybrid compile/runtime technique to symbolically parallelize loop nests with uniform dependences on multiple levels. At compile time, two novel transformations are performed: (a) symbolic hierarchical tiling followed by (b) symbolic multi-level scheduling. By tuning the size of the tiles on multiple levels, a trade-off between the necessary I/O-bandwidth and memory is possible, which facilitates obeying resource constraints. The resulting schedules are symbolic with respect to the number of tiles; thus, the number of processing elements to map onto does not need to be known at compile time. At runtime, when the number is known, a simple prolog chooses a feasible schedule with respect to I/O and memory constraints that is latency-optimal for the chosen tile size. In this way, our approach dynamically chooses latency-optimal and feasible schedules while avoiding expensive re-compilations.

ABSTRACT. We propose an algorithm for reachability analysis in micro-architectural models of communication fabrics. The main idea of our solution is to group transfers in what we call transfer islands. In an island, all transfers fire at the same time. To justify our abstraction, we give semantics of the initial models using a process algebra. We then prove that a transfer occurs in the transfer islands model if and only the same transfer occurs in the process algebra semantics. We encode the abstract micro-architectural model together with a given state reachability property in the input format of nuXmv. Reachability is then solved either using BDDs or IC3. Combined with inductive invariant generation techniques, our approach shows promising results.

ABSTRACT. The long-term goal of the work presented here is the automatic instrumentation of C programs with temporal property checkers to perform the runtime verification that these programs behave as expected, both for debugging purposes and for security or safety-oriented monitoring. This paper describes our first results towards this objective. To give requirements engineers or software developers the possibility to express advanced properties, the chosen specification language is the IEEE standard PSL (Property Specification Language). From PSL properties, a tool automatically generates assertion checkers and instruments the program with these verification components together with an observation mechanism that enables their event-driven activation. For maximum flexibility, the current implementation proposes either to decorate the source code or to observe the binary code under execution. An analysis of these solutions is achieved by means of experimental results.

ABSTRACT. Due to the heterogeneity and complexity of systems-of-systems (SoS), their simulation is becoming very time consuming, expensive and hence impractical. As a result, design simulation is increasingly being complemented with more efficient design emulation. Runtime monitoring of emulated designs would provide a precious support in the verification activities of such complex systems.

We propose novel algorithms for translating signal temporal logic (STL) assertions to hardware runtime monitors implemented in field programmable gate array (FPGA). In order to accommodate to this hardware specific setting, we restrict ourselves to past and bounded future temporal operators interpreted over discrete time. We evaluate our approach on two examples: the mixed signal bounded stabilization; and the serial peripheral interface (SPI) communication protocol. These case studies demonstrate the suitability of our approach for runtime monitoring of both digital and mixed signal systems.

ABSTRACT. We investigate the problem of verifying the absence of zeno executions in a hybrid system. A zeno execution is one in which there are infinitely many discrete transitions in a finite time interval. The presence of zeno executions poses challenges towards implementation and analysis of hybrid control systems. We present a simple transformation of the hybrid system which reduces the non-zenoness verification problem to the termination verification problem, that is, the original system has no zeno executions if and only if the transformed system has no non-terminating executions. This provides both theoretical insights and practical techniques for non-zenoness verification. Further, it also provides techniques for isolating parts of the hybrid system and its initial states which do not exhibit zeno executions. We illustrate the feasibility of our approach by applying it on hybrid system examples.

ABSTRACT. Verification condition generators (VCGs) can reduce overall correctness statements about sequential programs to verification conditions (VCs) that can then be proved independently by automatic theorem provers like SMT solvers. SMT solvers became not only more powerful in recent years in that they can now solve much bigger problems than before, they can now also solve problems of less restricted logics, for example, by covering non-linear arithmetic as required by some hybrid systems. However, there is so far still no VCG procedure that could generate VCs of hybrid programs for these SMT solvers.

We therefore propose in this paper a first VCG procedure for hybrid systems that is based on induction proofs on the strongly connected components (SCCs) of the underlying state transition diagrams. Given the right invariants for a safety property, the VCs can be automatically generated for the considered hybrid system. The validity of the VCs is then independently proved by SMT solvers and implies the correctness of the considered safety property.

ABSTRACT. Unsafe behavior of hybrid systems can have disastrous consequences, motivating the need for formal verification of the software running on these systems. Foundational verification in a proof assistant such as Coq is a promising technique that can provide extremely strong, foundational, guarantees about software systems. In this paper, we show how to apply this technique to hybrid systems. We define a TLA-inspired formalism in Coq for reasoning about hybrid systems and use it to verify two quadcopter modules: the first limits the quadcopter's velocity and the second limits its altitude. We ran both of these modules on an actual quadcopter, and they worked as intended. We also discuss lessons learned from our experience foundationally verifying hybrid systems.