Top-down Verification Methodology
Transaction level modeling allows exploring several SoC design architectures leading to better performance and easier verification of the final product. In this sub-project, we present an approach to design and verify SystemC models at the transaction level.We integrate the verification as part of the design-flow. In the proposed approach, we first model both the design and the properties (written in PSL) in UML. Then, we translate them into an intermediate format modeled with Abstract State Machines (ASM). The ASM model is used to generate an FSM of the design including the properties. Checking the correctness of the properties is performed on-the-fly while generating the state machine. Finally, we translate the veri.ed design to SystemC and map the properties to a set of assertions (as monitors in C#) that can be re-used to validate the design at lower levels through simulation.
Bottom-up Verification Methodology
In this subproject we present a bottom-up verification methodology. We propose an embedding of PSL in AsmL with an approach to verify properties on design implementations. We embed PSL properties in AsmL, to be able to reason about the behavior of the design, and its correctness against its specification. We use the AsmL tool in order to generate an FSM of the design model (including the properties). This approach enabled the verification of PSL properties on designs using classical model checking tools, for example SMV. For this, we translate the generated FSM into the input language of the SMV tool.
Enhancing Coverage using Genetic Algorithms
Recent advancement in hardware design urged using a transaction based model as a new intermediate design level. Supporters for the Transaction Level Modeling (TLM) trend claim its efficiency in terms of rapid prototyping and fast simulation in comparison to the classical RTL-based approach. Intuitively, from a verification point of view, faster simulation induces better coverage results. This is driven by two factors: coverage measurement and simulation guidance. In this sub-project, we propose to use an abstract model of the design, written in the abstract state machines language (AsmL), which provides an adequate way for measuring the functional coverage. Then, we use this metric in defining the fitness function of a genetic algorithm proposed to improve the simulation efficiency. Finally, we compare our coverage and simulation results to: (1) random simulation at the transaction level; and (2) the Specman tool of Verisity at RTL.
Towards a faster Simulation of SystemC
Accelerating simulation is one of the main reasons beyond the introduction of system level modeling. Here SystemC is one of the main players proven to speed-up simulation in comparison to classical HDL languages. However, the kernel architecture of the SystemC simulator treats the design as a black box. For instance, all active processes are executed without checking if they are relevant to the test plan. It is obvious that in random simulation you will include many runs not important for the verification of a specific feature. This is the case when you want to test a particular mode of a bus model, for example. We propose in this sub-project, as a solution for this problem, to classify the system’s states into “relevant” or “non-relevant” for the verification of certain features (assertions). We generate a reduced model of the design including only the processes relevant for the feature under test. Such a reduction directly results on simulation acceleration. We illustrate the performance of our approach on a set of models built on top of the Master/Slave library part of the SystemC release and for four levels of abstraction: untimed functional (UTF) and bus-cycle-accurate (BCA).
Languages Semantics
Our global methodology (see main webpage) we make use of three languages: SystemC, AsmL and PSL. We defined in this sub-project:
- A denotational semantics for SystemC.
- An ASM semantics of SystemC.
- A denotational semantics for AsmL.
- An ASM semantics for PSL.
