The Hardware-Software Interface for Systems-on-Chip: Formal Modeling and Modular Verification

Jun 25, 2021, 3:00 pm3:00 pm
Event Description

Modern computing platforms are getting increasingly heterogeneous with domain-specific hardware accelerators. The heterogeneity provides efficiency in computation; however, it also brings about new challenges in specification and verification.

For homogeneous systems with only the general-purpose processors, the instruction set architecture (ISA) creates a separation between the hardware and software in terms of design and verification. It decouples the development of a software program from the hardware implementation of the processor, and verification of hardware and software becomes more scalable. However, for specialized hardware accelerators in emerging systems-on-chip (SoCs), there is no such ISA-like model for the interface.

This thesis considers the instruction-level abstraction (ILA) as a generalization of the ISA for domain-specific accelerators in heterogeneous SoCs. It presents an ILA-based hardware formal verification methodology where ILA is used as a specification. This methodology demonstrates how formal verification can benefit from the attributes of the ILA. The thesis then discusses the importance of invariants in such formal hardware verification and proposes two techniques, both based on syntax-guided synthesis, for environment invariant synthesis and hardware model checking, respectively. As a hardware-software interface model, ILA can also be used as a hardware abstraction in system-level hardware-software verification. Specifically, as SoC components typically use shared memory accesses for bulk data transfer, the verification must take memory consistency models (MCMs) into account. This is addressed by the ILA-MCM verification framework in this thesis.

In summary, this thesis presents the ILA as the hardware-software interface model for the specification and verification of modern heterogeneous SoCs. The ILA-based verification methodology allows modular verification which increases the scalability of formal SoC verification.