Not available / text

"January 2004" / Bibliography: leaves 183-198. / xv, 198 leaves : ill. ; 30 cm. / Title page, contents and abstract only. The complete thesis in print form is available from the University Library. / As no single specification or verification method is able to solve all classes of problems, especially with industrial-sized applications, a diversity of modelling languages and analysis techniques specialised and optimized for various domains is needed, along with the ability to use them in combination. The work presented in this thesis has concentrated on developing techniques to support the use of a combination of modelling languages, especially visual languages, for system specification. Also, in order to tackle the main obstacles of model checking and make it more accessible to and usable by practising engineers, this work has focused on providing lightweight but effective methods and tools to alleviate the state space explosion problem in model checking. / Thesis (Ph.D.)--University of Adelaide, School of Computer Science, 2004

"January 2004" / Bibliography: leaves 183-198. / xv, 198 leaves : ill. ; 30 cm. / Title page, contents and abstract only. The complete thesis in print form is available from the University Library. / As no single specification or verification method is able to solve all classes of problems, especially with industrial-sized applications, a diversity of modelling languages and analysis techniques specialised and optimized for various domains is needed, along with the ability to use them in combination. The work presented in this thesis has concentrated on developing techniques to support the use of a combination of modelling languages, especially visual languages, for system specification. Also, in order to tackle the main obstacles of model checking and make it more accessible to and usable by practising engineers, this work has focused on providing lightweight but effective methods and tools to alleviate the state space explosion problem in model checking. / Thesis (Ph.D.)--University of Adelaide, School of Computer Science, 2004

This dissertation addresses the challenge of modelling and functional verification for com- plex computer micro-architecture designs. It is evident that the emerging span and com- plexity of new computer architectures outstrip existing design modelling and verification methods. Several attempts in industry and academia, including High Level Modelling, still do not scale to address this problem. Typically they lack precise and clear language semantics for formal analysis, and do not have native support for concurrency, or the design language and methodology do not fit. Therefore, the gap between what current solutions provide and what industry needs is increasing. In this research we aim to leap ahead of the common incremental research in this area, and develop a new framework for algorithm level modelling and verification. We introduce a high level and executable Architectural Specification Language (ASL) for modelling the functional behaviour of the architectural algorithms. The semantics of our models is based on the theory of Abstract State Machines with synchronous parallel execution and finite choice, which we find naturally suitable for hardware modelling. Our framework is also powered by native symbolic execution algorithms for enabling high- level verification, design explorations and refinement checks of the high level models down to the design implementation. We developed a new framework that implements our ideas through ASL and supports symbolic execution. We demonstrate the utility of our language and symbolic execu- tion on examples and case studies in various modelling domains, and show a promising framework and methodology. We believe our approach will make it easier to explore micro-architectural algorithm behavior and easier to validate this using dynamic or formal techniques, thus yielding a promising attack on the modelling and verification problem, and enabling more productive convergence to high quality implementations.

Not available / text

Behavioral synthesis is the process of compiling an Electronic System Level (ESL) design to a register-transfer level (RTL) implementation. ESL specifications define the design functionality at a high level of abstraction (e.g., with C/C++ or SystemC), and thus provide a promising approach to address the exacting demands to develop feature-rich, optimized, and complex hardware systems within aggressive time-to-market schedules. Behavioral synthesis entails application of complex and error-prone transformations during the compilation process. Therefore, the adoption of behavioral synthesis highly depends on our ability to ensure that the synthesized RTL conforms to the ESL description. This dissertation provides an end-to-end scalable equivalence checking support for behavioral synthesis. The major challenge of this research is to bridge the huge semantic gap between the ESL and RTL descriptions, which makes the direct comparison of designs in ESL and RTL difficult. Moreover, a large number and a wide variety of aggressive transformations from front-end to back-end require an end-to-end scalable checking framework. This dissertation provides an end-to-end scalable equivalence checking support for behavioral synthesis. The major challenge of this research is to bridge the huge semantic gap between the ESL and RTL descriptions, which makes the direct comparison of designs in ESL and RTL difficult. Moreover, a large number and a wide variety of aggressive transformations from front-end to back-end require an end-to-end scalable checking framework. A behavioral synthesis flow can be divided into three major phases, including 1) front-end : compiler transformations, 2) scheduling: assigning each operation a clock cycle and satisfying the user-specified constraints, and 3) back-end : local optimizations and RTL generation. In our end-to-end and incremental equivalence checking framework, we check each of the three phases one by one. Firstly, we check the front-end that consists of a sequence of compiler transformations by decomposing it into a series of checks, one for each transformation applied. We symbolically explore paths in the input and output programs of each transformation, and check whether the input and output programs have the same observable behavior under the same path condition. Secondly, we validate the scheduling transformation by checking the preservation of control and data dependencies, and the preservation of I/O timing in the user-specified scheduling mode. Thirdly, we symbolically simulate the scheduled design and the generated RTL cycle by cycle, and check the equivalence of each mapped variables. We also develop several key optimizations to make our back-end checker scale to real industrial-strength designs. In addition to the equivalence checking framework, we also present an approach to detecting deadlocks introduced by parallelization of RTL blocks that are connected by synthesized interfaces with handshaking protocols. To demonstrate the efficiency and scalability of our framework, we evaluated it on transformations applied by a behavioral synthesis tool to designs from the C-based CHStone and SystemC-based S2CBench benchmarks. Based on the evaluation results, our front-end checker can efficiently validate more than 75 percent of the total of 1008 compiler transformations applied to designs from the CHStone benchmark, taking an average time of 1.5 seconds per transformation. Our scheduling checker can validate control-data dependencies and I/O timing of all designs from S2CBench benchmark. Our back-end checker can handle designs with more than 32K lines of synthesized RTL from the CHStone benchmark, which demonstrates the scalability of the checker. Furthermore, our checker found several bugs in a commercial tool, underlining both the importance of formal equivalence checking and the effectiveness of our approach.

Due to the rapidly increasing complexity in hardware designs and competitive time to market trends in the industry, there is an inherent need to move designs to a higher level of abstraction. Behavioral Synthesis is the process of automatically compiling such Electronic System Level (ESL) designs written in high-level languages such as C, C++ or SystemC into Register-Transfer Level (RTL) implementation in hardware description languages such as Verilog or VHDL. However, the adoption of this flow is dependent on designers' faith in the correctness of behavioral synthesis tools. Loop pipelining is a critical transformation employed in behavioral synthesis process, and ubiquitous in commercial and academic behavioral synthesis tools. It improves the throughput and reduces the latency of the synthesized hardware. It is complex and error-prone, and a small bug can result in faulty hardware with expensive ramifications. Therefore, it is critical to certify the loop pipelining transformation so that designers can trust the behaviorally synthesized pipelined designs. Certifying a loop pipelining transformation is however, a major research challenge because there is a huge semantic gap between the input sequential design and the output pipelined implementation, making it infeasible to verify their equivalence with automated sequential equivalence checking (SEC) techniques. Complex loop pipelining transformations can be certified by a combination of theorem proving and SEC: (1) creating a certified pipelining algorithm which generates a reference pipeline model by exploiting pipeline generation information from the synthesis flow (e.g. the iteration interval of a generated pipeline) and (2) conduct SEC between the synthesized pipeline and this reference model. However, a key and arguably, the most complex component of this approach is the development of a formal, mechanically verifiable loop pipelining algorithm. We show how to systematically construct such an algorithm, and carry out its verification using the ACL2 theorem prover. We propose a framework of certified pipelining primitives which are essential for designing pipelining algorithms. Using our framework, we build a certified loop pipelining algorithm. We also propose a key invariant in certifying this algorithm, which links sequential loops with their pipelined counterparts. This is unlike other invariants that have been used in proofs of microprocessor pipelines so far. This dissertation provides a framework for creating certified pipelining algorithms utilizing a mechanical theorem prover. Using this framework, we have developed a certified loop pipelining algorithm. This certified algorithm is essential in the overall approach to certify behaviorally synthesized pipelined designs. We demonstrate the scalability and robustness of our algorithm on several ESL designs across various domains.

Not available / text

Hardware/Software (HW/SW) interfaces are pervasive in computer systems. However, many HW/SW interface implementations are unreliable due to their intrinsically complicated nature. In industrial settings, there are three major challenges to improving reliability. First, as there is no systematic framework for HW/SW interface specifications, interface protocols cannot be precisely conveyed to engineers. Second, as there is no unifying formal model for representing the implementation semantics of HW/SW interfaces accurately, some critical properties cannot be formally verified on HW/SW interface implementations. Finally, few automatic tools exist to help engineers in HW/SW interface development. In this dissertation, we present an automata-theoretic approach to HW/SW co-verification that addresses these challenges. We designed a co-specification framework to formally specify HW/SW interface protocols; we synthesized a hybrid Büchi Automaton Pushdown System, namely Büchi Pushdown System (BPDS), as the unifying formal model for HW/SW interfaces; and we created a co-verification tool, CoVer that implements our model checking algorithms and realizes our reduction algorithms for BPDS. The application of our approach to the Windows device/driver framework has resulted in the detection of fifteen specification issues. Furthermore, utilizing CoVer, we discovered twelve real bugs in five drivers. These non-trivial findings have demonstrated the significance of our approach in industrial applications.

Web Service Business Process Execution Language (BPEL) has become a standard language in the world of Service Oriented Architecture (SOA) for specifying interactions between internet services. This standard frees developers from low-level concerns involving platform, implementation, and versioning. These freedoms risk development of less robust artifacts that may even become part of a mission-critical system. Model checking a BPEL artifact for correctness with respect to temporal logic properties is computationally complex, since it requires enumerating all communication and synchronization amongst various services with itself. This entails modeling BPEL features such as concurrency, hierarchy, interleaving, and non-deterministic choice. The thesis will provide rules and procedures for translating these features to a veriable model written in Promela. We will use these rules to build a program which automates the translation process, bringing us one step closer to push button verification. Finally, two BPEL artifacts will be translated, manually edited, verified, and analyzed. / by Augusto Varas. / Thesis (M.S.C.S.)--Florida Atlantic University, 2009. / Includes bibliography. / Electronic reproduction. Boca Raton, Fla., 2009. Mode of access: World Wide Web.