الفهرس 
IntroductionOnly 14 pages are availabe for public view
 |  | from | 142 |  |  |
| | | from | 142 | | |
Abstract
Due to the growing complexity of the state-of-the-art System-on-Chips, shared resources are used in each and every component of the system. These shared resources, which are crucial for the proper functionality of various components within an SoC, require a fair and responsive mechanism for effective resolution of conflicts. The shared resources -to name a few- could be an AMBA bus, buffers, memory blocks, arithmetic, and logic units, which can be used by multiple clients in the system. To address the challenge of conflict resolution between different resource requestors, arbiters are deployed. Arbiters differ according to multiple aspects, such as fairness (weak fairness, strong fairness) and timing.
Accordingly, the verification of arbiter circuits is of great importance, not only from a functional perspective ensuring they function correctly, but also from a security perspective, guarding against potential security vulnerabilities. The verification of arbiters evaluates the properties that ensures fairness, deadlock-freedom, request-to-grant delay and other properties, which differ according to the arbiter algorithm.
This thesis introduces a formal verification framework, tailored for evaluating the precise operational behavior of a diverse combination of arbiter configurations. By harnessing the expressiveness of SystemVerilog assertions and leveraging the power of model checking techniques.
A novel dimension of this research is the exploration of hardware security. This thesis presents a novel methodology for modeling hardware Trojans, each characterized by distinct activation triggers and malicious payloads. The innovation lies in achieving this without applying any invasive modifications of the underlying circuits. This modeling approach enables the efficient detection and analysis of potential security vulnerabilities in these arbiter circuits.
Results discuss the cost of running the formal verification environment for the Trojan-free versions of arbiters. The formal environment leverage Questa PropCheck and extract the required time and memory. It also shows how the formally modelled hardware Trojans affect the hold-fire criteria of the formal environment that ensures this framework is able to detect different models of randomly-injected hardware Trojans through firing at least one property. The proposed work can be generalized to validate the expected functional and security requirement of complex systems.