Boolean satisfiability (SAT) based methods have traditionally been popular for formally verifying properties for digital circuits. We present a novel methodology for formulating a SPICE-type circuit simulation problem as a satisfiability problem. We start with a circuit level netlist, capture the non-linear behavior of the circuits at the transistor level via conservative approximations and transform the simulation problem into a search problem that can be exhaustively explored via a SAT solver. Thus, for DC as well as fixed time-step based transient and periodic steady state (PSS) simulation formulations, the solutions produced by the solver are formal in nature. We also present algorithms for abstraction refinement and smart interval generation to improve the computational efficiency of our proposed solution scheme. We have implemented our ideas into a tool called fSpice which is the first attempt at building a formal SPICE engine. We demonstrate the applicability of our ideas by showing experimental results using pruned versions of real designs that faced challenges during chip tape-out. Categories and Subject Descriptors I.6.5 [Simulation and Modeling]: Model Development General Terms Algorithms, Design

We propose the notion of logical reliability for real-time program tasks that interact through periodically updated program variables. We describe a reliability analysis that checks if the given short-term (e.g., single-period) reliability of a program variable update in an implementation is sufficient to meet the logical reliability requirement (of the program variable) in the long run. We then present a notion of design by refinement where a task can be refined by another task that writes to program variables with less logical reliability. The resulting analysis can be combined with an incremental schedulability analysis for interacting real-time tasks proposed earlier for the Hierarchical Timing Language (HTL), a coordination language for distributed real-time systems. We implemented a logical-reliability- enhanced prototype of the compiler and runtime infrastructure for HTL.

Synchronous systems offer a clean semantics and an easy verification path at the expense of often inefficient implementations. Capturing design specifications as synchronous models and then implementing the specifications in a less restrictive platform allow to address a much larger design space. The key issue in this approach is maintaining semantic equivalence between the synchronous model and its implementation. We address this problem by showing how to map a synchronous model onto a loosely time-triggered architecture that is fairly straightforward to implement as it does not require global synchronization or blocking communication. We show how to maintain semantic equivalence between specification and implementation using an intermediate model (similar to a Kahn process network but with finite queues) that helps in defining the transformation. Performance of the semantic preserving implementation is studied for the general case as well as for a few special cases.

Safety-critical feedback-control applications may suffer faults in the controlled plant as well as in the execution platform, i.e., the controller. Control theorists design the control laws to be robust with respect to the former kind of faults while assuming an idealized scenario for the latter. The execution platforms supporting modern real-time embedded systems, however, are distributed architectures made of heterogeneous components that may incur transient or permanent faults. Making the platform fault tolerant involves the introduction of design redundancy with obvious impact on the final cost. We present a design flow that enables the efficient exploration of redundancy/cost tradeoffs. After providing a system-level specification of the target platform and the fault model, designers can rely on the synthesis of the low-level fault-tolerance mechanisms. This is performed automatically as part of the embedded software deployment through the combination of the following three steps: replication, mapping, and scheduling. Our approach has a sound foundation in fault-tolerant data flow, a novel model of computation that simplifies the integration of formal validation techniques. Finally, we report on the application of our design flow to two case studies from the automotive industry: a steer-by-wire system from General Motors and a drive-by-wire system from BMW.

The complexity and physical distribution of modern active-safety automotive applications requires the use of distributed architectures. These architectures consist of multiple electronic control units (ECUs) connected with standardized buses. The most common configuration features periodic activation of tasks and messages coupled with run-time priority-based scheduling. The correct deployment of applications on such architectures requires end-to-end latency deadlines to be met. This is challenging since deadlines must be enforced across a set of ECUs and buses, each of which supports multiple functionality. The need for accommodating legacy tasks and messages further complicates the scenario.

Architecture design is a critical stage of the electronics/controls/software (ECS)-based vehicle design flow. Traditional approaches relying on component-level design and analysis are no longer effective as they do not always allow for the quantitative evaluation of properties arising from the composition of subsystems. This paper presents a system level architecture design methodology that is supported by tools and methods for the quantitative evaluation of key metrics of interest related to timing, dependability and cost. An example of its application to a by-wire system case study is presented, and the challenges faced in its application in the context of the actual development process are discussed

Modern automotive architectures support the execution of distributed safety- and time-critical functions on a complex networked system with several buses and tens of ECUs. Schedulability theory allows the analysis of the worst case end-to-end latencies and the evaluation of the possible architecture configurations options with respect to timing constraints. The paper presents an optimization framework, based on an ILP formulation of the problem, to select the communication and synchronization model that leverages the trade-offs between the purely periodic and the precedence constrained data-driven activation models to meet the latency and jitter requirements of the application. The authors demonstrate its effectiveness by optimizing a complex automotive architecture

We address the problem of mapping a set of processes which communicate synchronously on a distributed platform. The Time Triggered Architecture (TTA) proposed by Kopetz for the communication mechanism of a distributed platform offers a direct mapping that would preserve the semantics of the specification. However, its exact implementation may, at times, be problematic as it requires the distributed platform to have the clocks of its components perfectly synchronized. We propose as implementation architecture a relaxation of TTA called Loosely Time-Triggered Architecture (LTTA), in which computing units perform writes into and reads from the communication medium independently, triggered by local, quasi-periodic but non synchronized, clocks. LTTA offers some of the advantages of TTA with lower hardware cost and greater flexibility. So far LTTA was studied for single directional two-users communications over an LTT bus. General topology was not studied. In this paper we propose a design flow that ensures semantics preservation for an LTT communication network with arbitrary topology. Key elements are two new protocols for clock regeneration and predictive traffic shaping. Our approach relies on a mathematical Model of Communication (MoC) that we describe in detail.

Schedulability theory provides support for the analysis of the worst case latencies in distributed computations when the architecture of the system is known and the communication and synchronization mechanisms have been defined. In the design of complex automotive systems, however, a great benefit of schedulability analysis may come from its use as an aid in the exploration of the software architecture configurations that can best support the target application. We present an optimization algorithm that leverages the trade-offs between the purely periodic and the data-driven activation models to meet the latency requirements of distributed vehicle functions. We demonstrate its effectiveness on a complex automotive architecture

The large variety of architectural dimensions in automotive electronics design, for example, bus protocols, number of nodes, sensors and actuators interconnections and power distribution topologies, makes architecture design task a very complex but crucial design step especially for OEMs. This situation motivates the need for a design environment that accommodates the integration of a variety of models in a manner that enables the exploration of design alternatives in an efficient and seamless fashion. Exploring these design alternatives in a virtual environment and evaluating them with respect to metrics such as cost, latency, flexibility and reliability provide an important competitive advantage to OEMs and help minimize integration risks later in the design cycle. In particular, the choice of the degree of decentralization of the architecture has become a crucial issue in automotive electronics. In this paper, we demonstrate how a rigorous methodology (platform-based design) and the Metropolis framework can be used to find the balance between centralized and decentralized architectures

Designing cost-sensitive real-time control systems for safety-critical applications requires a careful analysis of both performance versus cost aspects and fault coverage of fault tolerant solutions. This further complicates the difficult task of deploying the embedded software that implements the control algorithms on a possibly distributed execution platform (for instance in automotive applications). In this paper, we present a novel technique for constructing a fault tree that models how component faults may lead to system failure. The fault tree enables us to use existing commercial analysis tools to assess a number of dependability metrics of the system. Our approach is centered on a model of computation, Fault Tolerant Data Flow (FTDF), that enables the integration of formal verification techniques. This new analysis capability is added to an existing design framework, also based on FTDF, that enables a synthesis-based, correct-by-construction, design methodology for the deployment of real-time feedback control systems in safety critical applications.

Designing cost-sensitive real-time control systems for safety-critical applications requires a careful analysis of the cost/coverage trade-offs of fault-tolerant solutions. This further complicates the difficult task of deploying the embedded software that implements the control algorithms on the execution platform that is often distributed around the plant (as it is typical, for instance, in automotive applications). We propose a synthesis-based design methodology that relieves the designers from the burden of specifying detailed mechanisms for addressing platform faults, while involving them in the definition of the overall fault-tolerance strategy. Thus, they can focus on addressing plant faults within their control algorithms, selecting the best components for the execution platform, and defining an accurate fault model. Our approach is centered on a new model of computation, fault tolerant data flows (FTDF), that enables the integration of formal validation techniques.

We present a tool suite for building, simulating, and analyzing the results of hierarchical descriptions of the scheduling policy for modules sharing a bus in real-time applications. These schedules can be based on a variety of factors including characteristics of messages and time slicing and are represented in a hierarchical tree-like structure that specifies multiple levels of arbitration. This structure can describe many popular arbitration schemes. Our simulator evaluates the specified scheduling structure on a set of message traces for a given bus. We illustrate our approach by applying it to two examples: the SAE Automotive Benchmark and Voice Over IP (VoIP). Although this paper deals with just bus scheduling policies, the approach can be easily extended to other real-time scheduling problems.

The design of engine control systems has been traditionally carried out using a mix of heuristic techniques validated by simulation and prototyping using approximate average-value models. However, the ever increasing demands on passengers' comfort, safety, emissions, and fuel consumption imposed by car manufacturers and regulations call for more robust techniques and the use of cycle-accurate models. We argue that these models must be hybrid because of the combination of time-domain and event-based behaviors. We present a hybrid model of the engine in which both continuous and discrete time-domain as well as event-based phenomena are modeled in a separate but integrated manner. Based on this model, we formalize the specification of the overall engine control by defining a number of hybrid control problems. To cope with the difficulties arising in the design of hybrid controllers, a design methodology is proposed. This methodology consists of a relaxation of the hybrid problem by simplifying some of its components to obtain a solvable problem,and then deriving a solution to the original control problem by appropriately modifying the control law so obtained to take into consideration the original specifications and models. The effectiveness of this approach is illustrated on three challenging problems: fast force-transient control, cutoff control, and idle speed control.