Assertion-based Verification for Inter-Device Communication in System-on-Chip

Abstract

Communication between devices on-chip takes place through bus interfaces and bus interconnect logic. Usually communication involves master and slave devices cross-talking by protocols defining when to send and receive the data and how the data should look like. Communication protocols could be standard or customized according to the chip design firm. Connecting or integrating such masters, slaves and interconnect in the system-on-chip is often an automatic process that involves scripting work, which in turn may involve mistakes. Devices communication may involve controlling or configuring devices and probing their statuses. In that case devices are looked at as memory mapped, and communication takes place so that devices configuration and status registers are read and written through transactions communicated on the device bus interface. The hardware description of the memory mapped devices is often automatically generated from a standard description of the registers, and consequently a percentage of failure rate comes from the nature of automation that may involve mistakes. This research work is concerned with two aspects of verification related to on-chip communication between devices. First, the connectivity between masters and slaves, or masters, slaves and the interconnect network. Second aspect is the memory mapped registers being the ways of configuring and monitoring devices. The thesis document focuses on formal verification of System-on-Chip connectivity and register specification, and proposes new methodologies for extracting or completing the specifications where it is commonly and practically unavailable.