Modern computing platforms are becoming increasingly accelerator-rich to meet the demanding power-performance requirements for emerging applications. Application-specific accelerators provide efficiency in computation; however, the heterogeneity of hardware components and the complexity of software/hardware interaction bring new challenges in developing and deploying such accelerator-rich platforms. In the days of microprocessors, the instruction-set architecture provided a natural specification/abstraction of the hardware. Top-down, it provided a specification for functional verification of microprocessor implementation. Bottom-up, it provided an abstraction of the microprocessor that defined the operational semantics of instructions. However, such a uniform and meaningful interface between the software program and hardware accelerators is lacking. Such a limitation is felt in both the compilation and correctness verification of the programs. This limits system integration verification at an early stage.

This thesis addresses the development challenges in modern accelerator-rich computing platforms, focusing on correct program development, based on the recently proposed Instruction-Level Abstraction (ILA) model. It first introduces the ILA formal model as a uniform software/hardware interface for accelerators and processors and describes the ILAng platform for modeling and verification using ILAs. This thesis then demonstrates how the ILA provides for correct software development in accelerator-rich platforms from two perspectives. First, it shows the use of ILAs for correct program compilation through an end-to-end compilation flow that correctly maps applications operations to accelerator operations. Second, it presents an ILA-based software/hardware co-verification methodology for checking system-level properties, with a deep dive into security verification of modern System-on-Chip designs.

In summary, this thesis presents the ILA formal model as a uniform interface between software programs and hardware accelerators. With the instruction-level interface, the ILA allows the specification of mappings between compiler intrinsics and accelerator operations. This enables utilizing standard compilation flows for programs that interact with accelerators and provides formally verifiable compilation. Furthermore, as a verified abstraction of accelerators, the ILA captures the operational semantics of hardware at the architecture level. This enables utilizing existing software verification techniques for scalable software/hardware co-verification and the correctness validation of system-level properties. Overall, this thesis demonstrates using ILAs for addressing the challenges of correct software development in modern accelerator-rich platforms.