4. Models for SoCs and Specifications

In order to perform system-level verification of SoCs, it is essential to not only model the on-chip IP protocols but also high-level requirements that describe the desired sequencing of control flow and data-flow between these IPs. This chapter provides the concept of SoC boiler plates. These provide an approach by which engineers can capture correctness criteria of a SoC at the system-level using “structured English” requirements. We then show how these can be automatically mapped to temporal logic formula. This chapter also introduces a type of finite state machine called synchronous Kripke structures (SKS). These are used for the formal representation of on-chip communication protocols of the IPs. This chapter may be viewed as the “requirements / specification” chapter.