SystemC TLM Verification

Description

Revolutionary new system specification languages which build on recent advances in microelectronics system --form processors, memory and advanced operating system through to sensors and networking-- can now be integrated into a single chip, known as System-on-Chip (SoC). The SoC technology requires a design language, or System Level Language, which can model both the software and the hardware. In this respect, SystemC is regarded as one of the most relevant system level modeling and simulation languages that has become an industry standard, adopted by thousands of users. However, the language is in its infancy and still has great need for good verification tools and techniques. We propose a framework for the verification of SoC modeled in SystemC including a static analysis to abstract SystemC designs; hence, reducing their complexity for better model checking and assertion based verification performance. The static analysis is based on abstract interpretation techniques, which can handle large and complex systems. Furthermore, it enables the static verification of critical problems such as infinite loops.




Figure1. SoC Verification Framework: The SystemC Case.

For model checking, the reduced model is first translated to AsmL (Abstract State Machines Language) and checked against properties written in PSL (the Property Specification Language standard). AsmL enables a higher level of abstraction and provides an interface for multiple model checking and theorem proving tools such as SMV and PVS. Using the Asmlt tool from Microsoft Research, AsmL code can be compiled and translated to C\# or connected to the .NET framework. We model the PSL in AsmL, where the user defines directly the design properties in AsmL according to the PSL syntax. When the model checking does not terminate due to state explosion, we complete the verification process by enabling assertion based verification. For instance, the PSL assertions are compiled to generate a set of C\# modules that are plugged in read-only mode to the SystemC design then verified by simulation. We defined a syntactical transformation from AsmL to SystemC that we proved to be sound using trace semantics. Furthermore, we implemented a genetic algorithm to guide the test vectors generation in order to enhance the coverage of the assertions using simulation. Our framework has shown promoting results when applied to transacion level models (TLM) rom the SystemC library, as well as commercial standard designs such as the PCI bus, the look-aside interface (LA-1), and the AGP bus. Its performance has been compared to other commercial tools such as RuleBase from IBM and FormalCheck from Cadence. Figure 1 displays a diagram providing details about the overall SystemC verification framework described above. Several issues are still open and need more investigation. Currently, we are exploring three main open-problems related to: (1) defining a real coverage for semi-formal verification using assertion based verification; (2) automatically improving the coverage of multiple assertions using genetic algorithms or other techniques such as genetic programming and neural networks; and (3) enhancing the simulation time through a sound reduction of the SystemC model. The third axis, in particular, involves finding reduction algorithms and proving their soundness and correctness.