Concurrency is one of the most important issues in system-level design. Interleaving among parallel processes can cause an extremely large number of different behaviors, making design and verification difficult tasks. In this work, we propose a synchronization verification method for system-level designs described in the SpecC language. Instead of modeling the design with timed FSMs and using a model checker for timed automata (such as UPPAAL or KRONOS), we formulate the timing constraints with equalities/inequalities that can be solved by integer linear programming (ILP) tools. Verification is conducted in two steps. First, similar to other software model checkers, we compute the reachability of an error state in the absence of timing constraints. Then, if a path to an error state exists, its feasibility is checked by using the ILP solver to evaluate the timing constraints along the path. This approach can drastically increase the sizes of the designs that can be verified. Abstraction and abstraction refinement techniques based on the Counterexample-Guided Abstraction Refinement (CEGAR) paradigm are applied.

Recently, system level design languages (SLDLs), which can describe both hardware and software aspects of the design, are receiving attentions. Analog mixed-signal (AMS) extensions to SLDLs enable current discrete-oriented SLDLs to describe and simulate not only digital systems but also digital-analog mixed-signal systems. In this paper, we present our work on the AMS extension to one of the system level design language--SpecC. The extended language supports designer to describe all the analog, digital and software aspects in a universal language.

Recently, system level design languages (SLDL), which can describe both hardware and software aspects of the design, are receiving attention. Mixed-signal extensions of SLDL enable current discrete-oriented SLDLs to describe and simulate not only digital systems but also digital-analog mixed-signal systems. The synchronization between discrete and continuous behaviors is widely regarded as a critical part in the extensions. In this paper, we present an event-driven synchronization mechanism for both timed and untimed system level designs through which discrete and continuous behaviors are synchronized via AD events and DA events. We also demonstrate how the synchronization mechanism can be incorporated into the kernel of SLDL, such as SpecC. In the extended kernel, a new simulation cycle, the AMS cycle, is introduced. Three case studies show that the extended SpecC-based system level design environment using our synchronization mechanism works well with timed/untimed mixed-signal system level description.

Embedded systems are used in broad fields. They are one of the indispensable and fundamental technologies in a highly informative society in recent years. As embedded systems are large-scale and complicated, it is prosperous to design and develop a system LSI (Large Scale Integration). The structure of the system LSI has been increasing complexity every year. The degree of improvement of its design productivity has not caught up with the degree of its complexity by conventional methods or techniques. Hence, an idea for the design of a system LSI which has the flow of describing specifications of a system in UML (Unified Modeling Language) and then designing the system in a system level language has already proposed. It is important to establish how to convert from UML to a system level language in specification description or design with the idea. This paper proposes, extracts and verifies transformation rules from UML to SpecC which is one of system level languages. SpecC code has been generated actually from elements in diagrams in UML based on the rules. As an example to verify the rules, "headlights control system of a car" is adopted. SpecC code has been generated actually from elements in diagrams in UML based on the rules. It has been confirmed that the example is executed correctly in simulations. By using the transformation rules proposed in this paper, specification and implementation of a system can be connected seamlessly. Hence, it can improve the design productivity of a system LSI and the productivity of embedded systems.

SpecC language is designated to handle the design of entire system from specification to implementation and of hardware/software co-design. Concurrency is one of the features of SpecC which expresses the parallel execution of processes. Describing the systems which contain concurrent behaviors would have some data exchanging or transferring among them. Therefore, the synchronization semantics (notify/wait) of events should be incorporated. The actual design, which is usually sophisticated by its characteristic and functionalities, may contain a bunch of event synchronization codes. This will make the design difficult and time-consuming to verify. In this paper, we introduce a technique which helps verifying the synchronization of events in SpecC. The original SpecC code containing synchronization semantics is parsed and translated into a Boolean SpecC code. The difference decision diagrams (DDDs) is used to verify for event synchronization on Boolean SpecC code. The counter examples for tracing back to the original source are given when the verification results turn out to be unsatisfied. Here we also introduce idea on automatically refinement when the results are unsatisfied and preset some preliminary results.