Special Session Paper: Application of Functional Verification Techniques in Hardware Trust

From bibtex.

Abstract

Functional verification techniques, particularly assertion-based verification, play a critical role in ensuring both correctness and security of modern hardware designs. In this paper, we propose and integrate a spectrum of formal and assertion-driven methods that extend conventional functional verification to address emerging security threats—ranging from stealthy Hardware Trojans (HTs) to adversarial cyber-attacks and cache side-channel exploits. First, we review traditional formal verification approaches such as SAT, BDD, and SCA, and discuss their adaptation to approximate computing and resource-bounded contexts. Next, we present an assertion-driven HT-detection paradigm at RTL, using control-flow graph matching and LTL-based specification mining with a hybrid similarity metric. We then demonstrate three complementary assertion-based methodologies for uncovering hardware security vulnerabilities: (1) deriving countermeasure assertions from an extracted finite-state machine model of an HT trigger; (2) automatically mining ISA-aware temporal assertions for RISC-V processors to detect embedded Trojans; and (3) mining temporal assertions from vehicle-dynamics traces to detect adversarial cyber attacks in autonomous vehicles. Finally, we propose a formal assertion-generation framework for securing RTL designs against cache side-channel attacks and HT insertions—generating security assertions for both cache memory and RISC-V processor implementations, and validating their efficacy against known CSCAs and Trojan benchmarks. Through these case studies, we demonstrate that assertion-based verification not only enhances functional correctness guarantees but also provides a high-fidelity, scalable mechanism for detecting and localizing a diverse range of hardware security threats.