Feature-Oriented Development And Formal Functional Verification Of SystemC Model Product Line

With the functionality of chips getting more and more complex, but their time-to-market getting more and more limited, more and more chips want to be implemented as System-on-a-Chip (SoC). SoC is an integrated system that integrates hardware (e.g. microprocessor and memory) and embedded software that running on the hardware. The most significant characteristic of SoC is that most of its functionality is implemented by the embedded software running on the hardware platform. So the development of SoC is much more flexible, and time-to-market is shortened. Traditional chip design flow begins with the description of System's Register-Transfer-Level (RTL) model, but cannot meet the requirements of early software development, so it is not applicable to SoC development. New design flow begins with the description of System's Transaction Level Model (TLM). Transaction level is much more abstract than RTL, so its development is much easier, and it simulates much faster, which meets the requirements of early software development, and is applicable to SoC development. SystemC is the standard language for transaction level modeling, so the study on the development and verification techniques of SystemC is of great significance.This thesis firstly proposes to treat the SystemC models developed for the same SoC project as a special Software Product Line (SPL), which we name SystemC Product Line (SCPL). Then, we study SCPL development methodology, SCPL type correctness and SCPL formal functional verification. SPL is a collection of software developed for a same domain. Because of the same domain, the software shares a set of common features. The study on SPL aims at increasing the efficiency of software development and verification by taking the advantags of the common features. SCPL is the collection of SystemC models developed for a same SoC project, so they also share a set of common features. The goal of our study is to increase the efficiency of development and verification of SystemC models by taking the advantages of the common features. Considering that SystemC models are C++ programs, the study on SCPL can borrow the study fruit of SPL. Considering that SystemC models aim at simulating the concurrent behavior of hardware, but software is running sequentially, the study on SCPL and SPL differentiate from each other. The study on SPL includes four main contents: the development methodology of SPL, syntax correctness of SPL, type correctness of SPL and behavior correctness of SPL. We make a parallel study on these contents for SCPL and get the following results:(1) We argue that under the new chip design flow that takes TLM as the entrance, the development of a SoC is always accompanied with a collection of SystemC models. We propose to treat the collection as a special SPL, and name it SCPL. We point out the difference between SCPL and normal SPL. (2) We point out the problems we meet when we develop SCPL with Object-Oriented (OO) methodology, and propose to develop SCPL with Feature-Oriented Programming (FOP) paradigm. We point out the problems when developing SPL with current FOP, and propose our corresponding solutions to these problems and apply them to the development of SCPL. Our case study shows that compared with OO development, FO development of SCPL can reduce duplicate code significantly, so as to increase development efficiency. At the same time, compared with SCPL development based on conditional compilation, FO SCPL development can greatly reduce the code embedded in conditional compilation directives. Since the excessive usage of conditional compilation directives is the key that makes code hard to develop, understand and maintain, our proposal of FO SCPL development can increase development efficiency, enhance code's understandability and maintainability.(3) We propose a simplified SystemC named SCS and its feature-oriented extension FSCS, discuss the type correctness problem of SCPL developed with FSCS, and give a sound and complete formal judge method to this problem. To judge the correctness of a SCPL, traditional method enumerates and compiles the SystemC models in the SCPL. Compared with the enumeration method, our method can shorten the judge time significantly. On the other hand, current SPL type correctness judge methods suffer from their in-completeness or the simplicity of their target language. Our method is complete, and our target language FSCS is applicable to simple SCPL development.(4) We propose a SCPL formal functional verification method based on the concept of property preservation. Our case study shows that compared with the verification method that enumerates and checks each SystemC model in the SCPL, our method can reduce the number of SystemC models that really need to be checked, so our method can reduce the time and space required by SCPL formal functional verification.(5) We propose the concept of property deduction, and propose a SCPL formal functional verification method based on this concept. Compared with property preservation, the requirements for property deduction is much looser, so the application of this method is broader. Our case study shows that compared with the verification method that enumerates and checks each SystemC model in the SCPL, this method can dramatically reduce the number of SystemC models that really need to be checked, so our method can efficiently reduce the time and space required by SCPL formal functional verification.In this thesis, we complete the development of the OpenRisc 1000 project and MJPEG decode chip project with our feature-oriented SCPL development method, judge the type correctness of the former project with our formal judgement method, and verify the behavior of the former project with our formal functional verification methods. Comparing our development of the former project with the open source implementation provided by OpenCores organization, the code embedded in conditional compilation directives has reduced remarkably, so the code's understandability and maintainability have considerably improved. Comparing our latter project with OO SCPL implementation, the total lines of code has reduced significantly, so the development efficiency has greatly improved. The result of the type correctness judgment of the OpenRisc 1000 project shows that our method improves the efficiency dramatically. The result of the formal functional verification of the OpenRisc 1000 project shows that our preservation based method and deduction based method can reduce the time and space required by SCPL formal functional verification significantly.