Current discrete event simulator requires heavy simulation overhead to switch between different components to simulate them in strictly chronological order. Therefore, timed simulation is significantly slower than un-timed simulation. By simply adding delays in the components and communication channels, our timed MPEG-2 decoder simulates more than 14 times slower than an un-timed simulation. In this paper, we propose a partial order method to speed up timed simulation by relaxing the order that the components are simulated. With partial order method, a component is not required to schedule a channel access if both behavioral and timing results of the access are known. The simulation switches less frequently hence the simulation overhead reduces. We show that partial order method can be used in complex system-level simulation such as MPSoC implementations of the MPEG-2 decoder. In our experiments, partial order method provides more than 10 times speedups over regular discrete event simulation for timed simulation.

Performance simulation of software for multiprocessor system-on-a-chips (MPSoC) suffers from poor tool support. Cycle accurate simulation at Instruction Set Simulation level is too slow and inefficient for any design of realistic size. Behavioral simulation, though useful for functional analysis at high level, does not provide any performance information that is crucial for design and analysis of MPSoC implementations. As a consequence, designers are often reduced to manually annotate performance information onto behavioral models, which contributes further to inefficiency and inaccuracy. In this paper, we use structural performance models to provide fast and accurate simulation of software for MPSoC.We generate structural models automatically using GCC with accurate performance annotation while considering optimizations for instruction selection, branch prediction, and pipeline interlock. Our structural models are able to simulate at several orders of magnitude faster than ISS and provide less than 1% error on performance estimation. These models allow realistic MPSoC design space explorations based on performance characteristics with simulation speed comparable to behavioral simulation. We validate our simulation models with several benchmarks and demonstrate our approach with a design case study of an MPEG-2 decoder.

Design of Multiprocessor System-on-a-Chips requires efficient and accurate simulation of every component. Since thememory subsystemaccounts for up to 50%of the performance and energy expenditures, it has to be considered in systemlevel design space exploration. In this paper, we present a novel technique to simulate memory accesses in software TLM/T models. We use a compiler to automatically expose all memory accesses in software and annotate them onto efficient TLM/T models. A reverse address map provides target memory addresses for accurate cache and memory simulation. Simulating at more than 10 MHz, our models allow realistic architectural design space explorations on memory subsystems. We demonstrate our approach with a design exploration case study of an industrial-strength MPEG-2 decoder.

Transaction-level models promise to be the basis of the verification environment for the whole design process. Realizing this promise requires connecting transaction-level and register-transfer-level (RTL) blocks through a transactor, which translates back and forth between RTL signal-based communication and transaction-level function-call-based communication. Each transactor is associated with a pair of interfaces, one at RTL and one at transaction level. Typically, however, a pair of interfaces is associated with more than one transactor, each assuming a different role in the verification process. In this paper, we propose a methodology in which both the interfaces and their relation are captured by a single formal specification. By using the specification, we show how the code for all the transactors associated with a pair of interfaces can be automatically generated. Our synthesis algorithm avoids the state-explosion problems associated with certain features of the specification formalism, at the expense of a more sophisticated simulation algorithm. We describe three different code-generation techniques targeted at different verification languages: (1) C++; (2) Verilog; and (3) the combination of the two that is compliant with the Standard Co-Emulation Modeling Interface protocol. In addition, we present several case studies demonstrating that automatically generated transactors can indeed replace handcrafted ones in realistic designs.

Transaction level models promise to be the basis of the verification environment for the whole design process. Realizing this promise requires connecting transaction level and RTL blocks through an object called a transactor, which translates back and forth between RTL signal-based communication, and transaction level function-call based communication. Each transactor is associated with a pair of interfaces, one at RTL and one at transaction level. Typically, however, a pair of interfaces is associated to more than one transactor, each assuming a different role in the verification process. In this paper we propose a methodology in which both the interfaces and their relation are captured by a single formal specification. By using the specification, we show how the code for all the transactors associated with a pair of interfaces can be automatically generated

With the increasing complexity and heterogeneity of embedded electronic systems, a unified design methodology at higher levels of abstraction becomes a necessity. Meanwhile, it is also important to incorporate the current design practice emphasizing IP reuse at various abstraction levels. However, the abstraction gap prohibits easy communication and synchronization in IP integration and co-simulation. In this paper, we present a communication infrastructure for an integrated design framework that enables co-design and co-simulation of heterogeneous design components specified at different abstraction levels and in different languages. The core of the approach is to abstract different communication interfaces or protocols to a common high level communication semantics. Designers only need to specify the interfaces of the design components using extended regular expressions; communication adapters can then be automatically generated for the co-simulation or other co-design and co-verification purposes.

With the scaling of technology and higher requirements on performance and functionality, power dissipation is becoming one of the major design considerations in the development of network processors. We use an assertion-based methodology for system-level power/performance analysis to study two dynamic voltage scaling (DVS) techniques, traffic-based DVS and execution-based DVS, in a network processor model. Using the automatically generated distribution analyzers, we analyze the power and performance distributions and study their trade-offs for the two DVS policies with different parameter settings, such as threshold values and window sizes. We discuss the optimal configurations of the two DVS policies under different design requirements. By a set of experiments, we show that the assertion-based trace analysis methodology is an efficient tool that can help a designer easily compare and study optimal architectural configurations in a large design space.

The debate about efficient methods for hardware-software co-design has taken interesting turns over the years. In this paper, we argue that the essential problems to solve are prior to the decision on how to partition the system in hardware-software. We present a formal platform-based design method we have proposed over the years and a design environment, Metropolis, supporting the methodology, which starts by capturing the design specifications at the highest level of abstraction and then proceed toward an efficient implementation by subsequent refinement steps. We present the modeling strategy used in Metropolis based on formal semantics that is general enough to support the models of computation proposed so far and that facilitates the creation of new ones. Nonfunctional and declarative constraints can also be captured using a logic language.

System level modeling with executable languages such as C/C++ has been crucial in the development of large electronic systems from general processors to application specific designs. To make sure that the executable models behave as they should, the designers often have to "eye-ball" the simulation traces and at best, apply simple "assert" statements or write simple trace checkers in some scripting languages. The problem is the lack of a concise and formal method to specify and check desired properties, whether they be functional or performance in nature. In this paper, we apply assertion checking methodology to the system design of network processors. Functional and performance assertions, based on linear temporal logic and logic of constraints, are written during the design process. Trace checkers and simulation monitors are automatically generated to validate particular simulation runs or to analyze their performance characteristics. Several categories of assertions are checked throughout the design process, such as equivalence, functionality, transaction, and performance. We demonstrate that the assertion-based methodology is very useful for both system level verification and design exploration.

Separating the description of important aspects of a design such as behavior and architecture, or computation and communication, may yield significant advantages in design time as well as in re-usability of the design. However, exploiting fully the re-usability opportunities offered by this approach implies to keep the various aspects of the design separated while verifying the design at a given level of abstraction. In particular, simulation of the design may undergo significant overhead versus a traditional approach where the design is represented and analyzed monolithically. In this paper, we present a few techniques that eliminate almost entirely the overhead while maintaining the positive aspects of the separation of concerns. Experimental results on a complex design back this assertion.

In the era of billion-transistor design, it is critical to establish effective verification methodologies from the system level, all the way down to the implementations. In this paper, we introduce logic of constraints (LOC), a logic that is particularly suited to express quantitative performance constraints as well as functional constraints. We analyze the expressiveness of LOC and show that it is important and different from linear temporal logic, upon which traditional hardware assertion languages (e.g., PSL and OpenVera) are based. We propose an automatic simulation trace checking/runtime monitoring methodology that can be used to verify system designs very efficiently. Since a subset of LOC is decidable, we also discuss the formal verification approach for LOC formulas. Through several industrial case studies, we demonstrate the usefulness of the LOC formalism and the corresponding simulation and verification approach at the higher transaction level of abstraction.

Verification of system designs continues to be a major challenge today. Simulation remains the primary tool for making sure that implementations perform as they should. We present algorithms to automatically generate trace checkers from formulas written in the formal quantitative constraint language, Logic Of Constraints (LOC), to analyze the simulation traces for functional and performance constraint violations. For many interesting formulas, the checkers exhibit linear time complexity and constant memory usage. We illustrate the usefulness and efficiency of this approach with large designs and traces.

STARS is a methodology for worst-case analysis of embedded systems. STARS manipulates abstract representations of system components to obtain upper bounds on the number of various events in the system, as well as a bound on the response time. VCC is a commercial discrete event simulator, that can be used both for functional and performance verification. We describe an extension of VCC to facilitate STARS. The extension allows the user to specify abstract representations of VCC modules. These abstractions are used by STARS, but their validity can also be checked by VCC simulation. We also propose a mostly automatic procedure to generate these abstractions. Finally, we illustrate on an example how STARS can be combined with simulation to find bugs that would be hard to find by simulation alone.

Design space exploration is the process of analyzing several functionally equivalent alternatives to determine the most suitable one. A fundamental question is whether an implementation is consistent with the high-level specification or whether two implementations are "equivalent." The synchronous assumption has made it possible to develop efficient procedures for establishing functional equivalence between different implementations in the domains of synchronous circuits and synchronous reactive systems. We extend this notion to embedded systems that do not satisfy the synchronous assumption inside their boundaries but only at the interface with the environment. Leveraging this property, we define synchronous equivalence for embedded systems that strongly resembles the concept of functional equivalence for sequential circuits. We develop efficient synchronous equivalence analysis algorithms for embedded system designs. The efficiency comes from analyzing the behavior statically on abstract representations, at a cost that some of the negative results may be false, i.e. the analysis is conservative. We develop primitives for making the representation more/less abstract, trading off complexity of the algorithms with the conservativeness of the results. We apply our analysis algorithms to an ATM switch and demonstrate that synchronous equivalence opens design exploration avenues uncharted before.

Design space exploration is the process of analyzing several functionally equivalent alternatives to determine the most suitable one. The synchronous assumption has made it possible to develop efficient procedures for establishing functional equivalence between different implementations in the domain of synchronous circuits as well as in the domain of synchronous reactive systems. We extend this notion to embedded systems that do not satisfy the synchronous assumption inside their boundaries but only at the interface with the environment Leveraging this property, we developed efficient synchronous equivalence analysis algorithms for embedded systems with loops and architectures with multiple computational units. We demonstrate our method on an ATM switch containing many interacting components.

This paper addresses the problem of schedu ling reactive real-time tran saction s(task groups) implementing a net work of extend ed Finite State Machines comm unicating asynchronously. Task instances are activated in response to internal and/or external ev ents.The objective is avoiding the loss of events exchanged by the tasks. This sc heduling problem has many similarities with the conventional formulation of real-tim e problems and yet it differs enough to justify a rethinking of the assu mptions an d techniques used to solve the problem. Our iterative solution targets fixed p riority systems and offers a priority assignment scheme together with a sufficiently tight worst-case analysis.

Recently a methodology for worst-case analysis of discrete systems has been proposed by the author. The methodology relies on a user-provided abstraction of system components. In this paper the author proposes a procedure to automatically generate such abstractions for system components with Boolean transition functions. She use a binary decision diagram (BDD) of the transition function to generate a formula in Presburger arithmetic representing the desired abstraction. The author's experiments indicate that the approach can be applied to control-dominated embedded systems.

We propose the use of the logic S1S as a mathematical framework for studying the synthesis of sequential designs. We will show that this leads to simple and mathematically elegant solutions to problems arising in the synthesis and optimization of synchronous digital hardware. Specifically, we derive a logical expression which yields a single finite state automaton characterizing the set of implementations that can replace a component of a larger design. The power of our approach is demonstrated by the fact that it generalizes immediately to arbitrary interconnection topologies, and to designs containing nondeterminism and fairness. We also describe control aspects of sequential synthesis and relate controller realizability to classical work on program synthesis and tree automata.

We propose a methodology for worst-case analysis of systems with discrete observable signals. The methodology can be used to verify different properties of systems such as power consumption, timing performance or resource utilization. We also propose an application of the methodology to timing analysis of embedded systems implemented on a single processor. The analysis provides a bound on the response time of such systems. It is typically very efficient, because it does not require a state space search.

Design exploration consists of analyzing several alternative implementations of the "same" function to determine the most desirable one. A fundamental question is whether an "implementation" is consistent with the high-level specification or whether two implementations are "equivalent". We define synchronous equivalence for embedded systems that strongly resembles the concept of functional equivalence for sequential circuits. We then present equivalence analysis algorithms that are of low polynomial complexity. We show an example of application of the algorithms to a real-life design (a shock absorber controller) and demonstrate that synchronous equivalence opens up design exploration avenues uncharted before.

We propose a software synthesis procedure for reactive embedded system. The procedure is an extension of the approach in the POLIS co-design framework. In our approach, control parts of the system are represented in a decomposed form, enabling more complex control structures to be represented. We propose a synthesis procedure for this representation that avoids unnecessary evaluations of the data part, as well as the overhead of run-time scheduling.

Software components for embedded reactive real-time applications must satisfy tight code size and run-time constraints. Cooperating finite state machines provide convenient intermediate format for embedded system co-synthesis, between high-level specification languages and software or hardware implementations. We propose a software generation methodology that takes advantage of a restricted class of specifications and allows for tight control over the implementation cost. The methodology exploits several techniques from the domain of Boolean function optimization. We also describe how the simplified control/data-flow graph used as an intermediate representation can be used to accurately estimate the size and timing cost of the final executable code.

Task scheduling for reactive real time systems is adifficult problem due to tight constraints that theschedule must satisfy.A static priority schemeis proposed here that can be formally validated.The method is applicable both for preemptiveand non-preemptive schedules and is conservativein the sense that a valid schedule may bedeclared invalid, but no invalid schedule may bedeclared valid.Experimental results show thatthe run time of our validation method is negligiblewith respect to other steps in system designprocess, and compares favorably with othermethods of schedule validation.

Both timing and functional properties are essential to characterize the correct behavior of an embedded system.Verication is in general performed either by simulation, or by bread-boarding.Given the safety requirements of such systems, a formal proof that the properties are indeed satised is highly desirable.In this paper, we present a formal veri cation methodology for embedded systems.The formal model for the behavior of the system used in POLIS is a network of Codesign Finite State Machines.This model is translated into automata, and veri ed using automatatheoretic techniques.An industrial embedded system is veri ed using the methodology.W e demonstrate that abstractions and separation of timing and functionality is crucial for the successful use of formal veri cation for this example.We also show that in POLIS abstractions and separation of timing and functionality can be done by simple syntactic modi cation of the representation of the system.

A promising approach to formal verification of real-time systems is to use timed automata to model systems, and then to check whether certain "unsafe" states are reachable. Although theoretically appealing, this approach has significant practical problems because it requires expensive computation of reachable states. Fortunately computing a superset of reachable states is sometimes much cheaper. Replacing the set of reachable states with its superset is a conservative approximation, in the sense that it can occasionally cause a correct system to be declared incorrect, but can never cause an incorrect system to be declared correct. We propose two algorithms for computing a superset of reachable states of a timed automaton. Both algorithms involve only manipulation of Boolean functions, which are used to represent both sets of discrete state components and timing information. The algorithms offer different trade-offs between accuracy of approximation and efficiency of computation. Initial experimental results show that they are competitive with the best published results, but that further improvements are necessary to scale up to realistic systems.

We present a mathematical framework for analyzing the synthesis of interacting, finite state systems. The logic S1S is used to derive simple, rigorous, and constructive solutions to problems in sequential synthesis. We obtain exact and approximate sets of permissible FSM network behavior, and address the issue of FSM realizability. This approach is also applied to synthesizing systems with fairness and timed systems.

Article Free Access Share on HSIS: a BDD-based environment for formal verification Authors: A. Aziz Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , F. Balarin Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , S.-T. Cheng Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , R. Hojati Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , T. Kam Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , S. C. Krishnan Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , R. K. Ranjan Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , T. R. Shiple Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , V. Singhal Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , S. Tasiran Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , H.-Y. Wang Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , R. K. Brayton Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , A. L. Sangiovanni-Vincentelli Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile Authors Info & Claims DAC '94: Proceedings of the 31st annual Design Automation ConferenceJune 1994 Pages 454–459https://doi.org/10.1145/196244.196467Published:06 June 1994Publication History 39citation325DownloadsMetricsTotal Citations39Total Downloads325Last 12 Months36Last 6 weeks17 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF