Modelling and Assertion-Based Verification of Run-Time Reconfigurable Designs with Functional Programming Abstractions

Abstract

With the increasing design and production costs and long time-to-market for Application Specific Integrated Circuits (ASICs), implementing digital circuits on reconfigurable hardware is becoming a more common practice. A reconfigurable hardware combines the flexibility of the software domain with the high performance of the hardware domain, and provides a flexible life cycle management for the product with a lower cost. High-level design and verification methodologies for reconfigurable designs increase the productivity of the designer and provide the possibility of broader Design Space Exploration (DSE) in early stages of the design flow. A complete design and assertion-based verification flow for Run-Time Reconfigurable (RTR) designs using functional abstractions of Haskell is proposed in this thesis, in which partially reconfigurable hardware is used as the implementation platform. The proposed flow includes modelling of RTR designs in high levels of abstraction by using higher-order functions and polymorphism in Haskell, as well as their implementation on Field Programmable Gate Arrays (FPGAs) with Partial Reconfiguration (PR) support. The so called Assertion Based Verification (ABV) is used as the verification approach which is integrated in the early stages of the design flow. In order to increase the performance of the verification process, the ABV is done by implementing assertion-checker circuits and the Design Under Verification (DUV) on the reconfigurable platform. The integrated assertion-checker expressions are automatically assembled by using proposed building blocks. The proposed structures for assertion-checkers are used for both simulation and synthesis purposes. Using reconfigurable hardware to implement verification circuits, accelerates the verification process, increases its flexibility, and enables verifying designs with large verification circuitry with a high amount of assertion checkers. This is realised by reconfiguring the desired set of the checkers on the reconfigurable hardware on-the-fly. A partitioning algorithmis also proposed for clustering the assertion-checker circuits to implement the verification circuits in a limited reconfigurable area in the target FPGA. An RTR architecture is also proposed for mapping assertion-checkers at run-time on FPGAs without PR support. The proposed flow is experimented with example designs on a Zynq FPGA as the hardware/software implementation platform to investigate its feasibility.