Hardware Security Analysis of Arbiters: Trojan Modeling and Formal Verification

Due to the scale of modern systems, pre-silicon security has become a major concern for design and verification engineers. In this paper, we propose a formal verification framework for the verification of different arbiter circuits with different protocols and sizes using SystemVerilog Assertions (SVA). We also propose a formal way of the modeling and insertion of hardware Trojans of different trigger and payload types without applying any modifications to the Design Under Test (DUT). The obtained results show the formal analysis statistics in terms of time and memory for Trojan-free designs for a set of all-proven properties. It also shows how Trojan insertion affects the pass-fail criteria of the formal properties, where at least a single property fails due to the inserted Trojan. The proposed work can be generalized to verify the correct functionality and security of an arbiter circuit placed within any complex system.