Federated learning (FL) with fully homomorphic encryption (FHE) effectively safeguards data privacy during model aggregation by encrypting local model updates before transmission, mitigating threats from untrusted servers or eavesdroppers in transmission. However, the computational burden and ciphertext expansion associated with homomorphic encryption can significantly increase resource and communication overhead. To address these challenges, we propose FedBit, a hardware/software co-designed framework optimized for the Brakerski-Fan-Vercauteren (BFV) scheme. FedBit employs bitinterleaved data packing to embed multiple model parameters into a single ciphertext coefficient, thereby minimizing ciphertext expansion and maximizing computational parallelism. Additionally, we integrate a dedicated FPGA accelerator to handle cryptographic operations and an optimized dataflow to reduce the memory overhead. Experimental results demonstrate that FedBit achieves a speedup of two orders of magnitude in encryption and lowers average communication overhead by $60.7 \%$, while maintaining high accuracy.

Large language models (LLMs) have demonstrated impressive capabilities in generating software code for high-level programming languages such as Python and C++. However, their application to hardware description languages, such as Verilog, is challenging due to the scarcity of high-quality training data. Current approaches to Verilog code generation using LLMs often focus on syntactic correctness, resulting in code with functional errors. To address these challenges, we present AutoVeriFix, a novel Python-assisted two-stage framework designed to enhance the functional correctness of LLM-generated Verilog code. In the first stage, LLMs are employed to generate high-level Python reference models that define the intended circuit behavior. In the second stage, these Python models facilitate the creation of automated tests that guide the generation of Verilog RTL implementations. Simulation discrepancies between the reference model and the Verilog code are iteratively used to identify and correct errors, thereby improving the functional accuracy and reliability of the LLM-generated Verilog code. Experimental results demonstrate that our approach significantly outperforms existing state-of-the-art methods in improving the functional correctness of generated Verilog code.

Chip manufacturing relies on rigorous verification to prevent costly design errors before fabrication and deployment. Branch coverage, a key metric for Register-Transfer Level (RTL) validation, ensures thorough testing of decision points in the design. However, RTL designs often contain numerous hard-to-activate branches, which can lead to hidden bugs and security vulnerabilities. While concolic testing addresses the memory explosion issues associated with formal methods, it relies on heuristics that may get stuck in local optima. In this paper, we propose a novel approach that reformulates Concolic testing as a reinforcement learning problem. Our method utilizes the agent that takes into account RTL structural characteristics and runtime simulation states to select strategies for guiding the simulation path toward target branches. Experimental results demonstrate that our approach effectively directs simulations toward branch targets, reduces search redundancy, and significantly increases branch coverage, thereby improving the efficiency and effectiveness of the test generation process.

The increasing complexity of modern processor designs has posed significant challenges in achieving comprehensive coverage metrics for functional verification of Register-Transfer Level (RTL) designs. Despite the availability of white-box RTL models, recent advancements in hardware fuzzing have predominantly focused on grey-box methodologies, which lack effective utilization of internal logic and structural information.This paper presents a novel approach that addresses this limitation by extracting control flow graphs (CFGs) from processor designs and analyzing the dependencies within these graphs. The analyzed CFGs serve as heuristic information to guide the generation of processor stimuli. By effectively leveraging internal logic information during the simulation of complex processors, this method provides interpretable heuristics for test generation. Experimental results demonstrate the effectiveness of utilizing control flow information derived from processor designs in enhancing the convergence speed of coverage metrics and guiding test sequences towards hard-to-reach states.

Verification is critical in ensuring the reliable operation of modern, complex computing systems. However, as processor designs become increasingly sophisticated, conventional static verification techniques struggle to generate high-quality test sequences that achieve comprehensive coverage. Dynamic simulation-based approaches, which leverage coverage-driven objectives, can increase confidence in correct processor functionality but often suffer from low verification efficiency due to the generation of redundant test sequences and significant computational overhead. To address these challenges, this paper presents DeepVerifier, a novel coverage-guided test generation framework that leverages data-driven learning of existing test sequences and their associated coverage feedback. DeepVerifier uses a language model to learn the semantic representations of test sequences, ensure adherence to syntax constraints, and estimate the relationship between test sequences and coverage scores. By updating test sequences with higher coverage, DeepVerifier can significantly improve the efficiency and effectiveness of the verification process. Experimental results of verifying an out-of-order RISC-V microprocessor demonstrate that the framework accurately estimates the coverage scores of test sequences and updates high-quality sequences that contribute to higher coverage. This coverage-guided test generation technique holds promise for enhancing the reliability of modern processor designs.

Deep neural network (DNN) accelerators have been developed to enhance the effectiveness of DNN models, particularly in resource-constrained devices. Achieving high-throughput and energy-efficient inference within area constraints requires careful consideration of design choices in both hardware (HW) and mapping spaces. To get better performance and energy efficiency, it is important to optimize hardware and mapping together. However, this co-optimization process presents a considerable challenge due to the expansive combined HW-Mapping design space. To find the optimal configuration in this large design space, we formulate the exploration of the hardware configuration as an optimization problem, and embed the exploration of the mapping design space into the evaluation stage of optimization. We implement a HW-Mapping co-optimization framework called MACO to find optimal configurations for both hardware and mapping, and provide a generic interface to integrate different optimization algorithms, including multi-objective Bayesian optimization (MOBO), non-dominated sorting genetic algorithms (NSGA), and random search. We evaluate our framework with four popular DNN models of different properties. Our evaluation shows that the MOBO-based approach can achieve a 30% energy reduction and a 37% latency reduction with the same area as the state-of-the-art HW-Mapping optimization framework.

General Matrix-Matrix Multiplication (GEMM) stands as the most ubiquitous operation in machine learning applications. However, performing GEMM within Fully Homomorphic Encryption (FHE) is inefficient due to high computational demands and significant data migration constrained by limited bandwidth. Additionally, the inherent limitations of FHE schemes restrict the widespread application of machine learning, as standard activation functions are incompatible. This incompatibility necessitates alternative nonlinear functions, which lead to notable accuracy reductions. To address these challenges, we introduce a polynomial encoding methodology for GEMM under the Brakerski/Fan-Vercauteren (BFV) scheme and extend the method to inference with packing inputs and weights for different sizes. Furthermore, we design specialized hardware to accelerate the inference process through optimized scheduling between the hardware and the host system. In experiments, we implemented our hardware on an FPGA U250 platform. Compared to existing solutions, our method achieves superior performance, achieving the highest $4.22 \times$ and $3.99 \times$ speedups on MNIST and CIFAR-10.

Effective power management is crucial for optimizing the performance and longevity of integrated circuits. Cycle-accurate power prediction can help power management during runtime. This paper introduces a Cycle-accurate Power Prediction framework via Spiking neural networks (SNNs) and Genetic signal Selection (CPP-SGS), which integrates SNNs and Genetic Algorithms (GAs) to predict real-time power consumption of chips. We apply GAs to select the most relevant signals as the input to SNNs to reduce the model size and inference time, making it well-suited for dynamic power estimation in real-time scenarios. The experimental results show that CCP-SGS outperforms the state-of-the-art approaches, with a normalized root mean squared error (NRMSE) of less than 1.6%.

Sparse general matrix multiplication (SpGEMM) is a crucial operation of deep neural networks (DNNs), leading to the development of numerous specialized SpGEMM accelerators. These accelerators leverage flexible interconnects, thereby outperforming their rigid counterparts. However, the suboptimal utilization of sparsity patterns limits overall performance efficiency. In this work, we propose DuSGAI, a sparse GEMM accelerator that employs a parallel index intersection structure to utilize dual-side sparsity. Our evaluation of DuSGAI with five popular DNN models demonstrates a 3.03× performance improvement compared to the state-of-the-art SpGEMM accelerator.

Modern processors feature complex architectures that necessitate the generation of extensive test programs to ensure functional correctness, making testing the most time-consuming stage of the processor design flow. Existing automated verification frameworks for agile design exhibit significant limitations, such as fixed program structures restricting flexibility, uncontrolled control flows leading to invalid instructions, and low coverage of the vast state space. To address these limitations, we propose CURE-Fuzz, a curiosity-driven reinforcement learning framework designed to enhance agile hardware testing. By integrating a hierarchical test generation model with a curiosity-driven exploration mechanism, CURE-Fuzz enables precise control over test program structure and dependencies while efficiently navigating unexplored processor states. Evaluations on Rocket and Boom core demonstrate that CURE-Fuzz achieves higher coverage and exhibits superior bug detection capabilities compared to state-of-the-art fuzzers.

Quantized Neural Networks (QNN) with extremely low-bitwidth data have proven promising in efficient storage and computation on edge devices. To further reduce the accuracy drop while increasing speedup, layer-wise mixed-precision quantization (MPQ) becomes a popular solution. However, existing algorithms for exploring MPQ schemes are limited in flexibility and efficiency. Comprehending the complex impacts of different MPQ schemes on post-training quantization and quantization-aware training results is a challenge for conventional methods. Furthermore, an end-to-end framework for the optimization and deployment of MPQ models is missing in existing work.In this paper, we propose the MiCo framework, a holistic MPQ exploration and deployment framework for edge AI applications. The framework adopts a novel optimization algorithm to search for optimal quantization schemes with the highest accuracies while meeting latency constraints. Hardware-aware latency models are built for different hardware targets to enable fast explorations. After the exploration, the framework enables direct deployment from PyTorch MPQ models to bare-metal C codes, leading to end-to-end speedup with minimal accuracy drops.

Simulation plays a crucial role in the verification of hardware designs, ensuring that they behave correctly before fabrication. However, traditional simulation methods can be inefficient when dealing with complex designs, especially in corner cases. To mitigate this inefficiency, Concolic testing has emerged as a promising technique, utilizing symbolic execution to guide the simulation process. However, the heuristics used in path exploration for Concolic testing often struggle with local optima, resulting in suboptimal verification outcomes and incomplete coverage of the design space. In this paper, we propose an agent-based framework to dynamically adjust path exploration strategies by leveraging beam search and large language models (LLMs). Experimental results demonstrate that this approach significantly improves branch coverage, especially for hard-to-detect branches, while also optimizing the use of computational resources.

AI models utilizing extremely low-bitwidth weights have shown promise in efficient storage and computation while maintaining satisfactory results through proper training processes. By converting floating-point multiplication into simpler addition and shifting operations, these models are well-suited for deployment on resource-constrained devices. However, traditional CPU architectures often fail to fully exploit the advantages of multiplication-free operations due to a lack of hardware support. In this paper, we propose BNRV, a lightweight SIMD extension designed for the RISC-V Instruction Set Architecture (ISA) that specifically targets multiplication-free operations involving 8-bit data and low-bitwidth weights (ranging from 1 to 2 bits). We have also developed an accompanying library with optimized kernels for deploying various AI models using BNRV. Our proposed extension significantly accelerates low-bitwidth quantized multiplication (up to$10.95 \times$times faster) and lowbitwidth transformer model inference (up to$3.11 \times$faster), with minimal power overhead (less than 2%) and area overhead (less than 4%) compared to processors without BNRV support.

Functional verification is critical in ensuring the correctness of register transfer level (RTL) models. Formal methods, such as model checkers, are powerful tools that help achieve high coverage in functional validation by transforming the coverage problem into property verification tasks. However, these methods typically demand significant memory usage and long verification times. One major issue is that the satisfiability problem for each unsolved property always starts from the reset state of a design, leading to repeated solving of the same subset of clauses across different properties. In this paper, we propose an open-source semi-formal framework based on model checkers that accelerates test stimulus generation through two techniques: assertion ordering and strategic selection of starting states. These techniques enable model checkers to intelligently select starting states that are much closer to the final state, thereby reducing unnecessary computations. Through comprehensive experiments on ITC'99 benchmarks and modern complex processor designs, including OpenCores 1200 and Rocket-Chip, we demonstrate that our proposed techniques can achieve higher coverage with less than half of the test generation time.

Design space exploration (DSE) has long been a very important topic in electronic design automation (EDA), but the growing diversity of applications and the complexity of integrated circuits make conventional DSE frameworks less effective and efficient. Therefore, an exploration algorithm that can find the optimal designs with fewer samples is demanded. This paper proposes a DSE framework for microprocessors that integrates a novel optimization algorithm with EDA flows. The proposed optimization algorithm utilizes space partitioning and Bayesian optimization to explore diverse and high-dimensional design spaces in microprocessors efficiently. Using the framework, we explore the design space of VexRiscv CPUs for TinyML workloads, where our proposed optimization algorithm obtains more Pareto-optimal designs and higher hypervolume with fewer samples.

Design space exploration (DSE) has long been a very important topic in electronic design automation (EDA). As the diversity of applications and the complexity of integrated circuits have grown rapidly in recent years, conventional DSE frameworks become less effective and efficient. This is due to the time-consuming nature of design point evaluation and the challenge of exploring high-dimensional design spaces. To address these issues, this paper proposes a DSE framework for microprocessors with a novel multi-objective optimization algorithm to find optimal designs with fewer samples. The proposed algorithm utilizes space partitioning and Bayesian optimization to efficiently explore high-dimensional design spaces in microprocessors.

The validation of Register-Transfer Level (RTL) models requires achieving sufficient branch coverage. However, automatically activating all branches in RTL models is challenging, considering the complexity of modern designs. While traditional methods, such as model checkers, can achieve high coverage, they typically demand substantial computational resources to solve formal equations. In contrast, constraint-random approaches have better scalability but suffer from inefficiency due to poor heuristics. This paper introduces APE-FV, a Concolic testing framework designed for RTL functional verification to effectively cover rare branches. APE-FV dynamically modifies the path exploration strategy by considering structural information, simulated paths, and states. Additionally, our framework incorporates an incremental exploration technique, which reduces the burden on solvers and enhances efficiency. Experimental results demonstrate that our approach accelerates the verification process and maintains high coverage, outperforming state-of-the-art techniques.

Branch coverage is important in the functional val-idation of Register-Transfer-Level (RTL) models. While random tests can cover the majority of easy-to-reach branches, there are still many hard-to-activate branches in today's industrial designs. These remaining corner branches are typically the source of bugs and hardware trojans. Directed test generation approaches using formal methods effectively activate a specific branch but are limited by the state explosion problem. Semi-formal methods, such as concolic testing, improve the scalability by exploring one path at a time. This paper presents a novel concolic testing framework to exercise the corner branches through state tracing-based search heuristics (STSearch). The proposed approach heuristically gen-erates and evaluates input sequences based on a novel heuristic indicator that evaluates the distance between the current state and the target branch condition. The heuristic indicator is designed to utilize both the static structural property of the design and the state from dynamic simulation. Compared to the existing concolic testing approaches, where a full new path is generated in each round by solving path constraints, the cycle-based heuristic search in the proposed approach is more effective and efficient. Experimental results show that our approach significantly outperforms the state-of-the-art approaches in both running time and memory usage.

Simulation is widely used for validation of Register-Transfer-Level (RTL) models. While simulating with millions of random or constrained-random tests can cover majority of the functional scenarios, the number of remaining scenarios can still be huge (hundreds or thousands) in case of today's industrial designs. Hard-to-activate branches are one of the major contributors for such remaining/untested scenarios. While directed test generation techniques using formal methods are promising in activating branches, it is infeasible to apply them on large designs due to state space explosion. In this article, we propose a fully automated and scalable approach to cover the hard-to-activate branches using concolic testing of RTL models. While application of concolic testing on hardware designs has shown some promising results in improving the overall coverage, they are not designed to activate specific targets such as uncovered corner cases and rare scenarios. In other words, existing concolic testing approaches address state space explosion problem but leads to path explosion problem while searching for the uncovered targets. Our proposed approach maps directed test generation problem to target search problem while avoiding overlapping searches involving multiple targets. This article makes two important contributions. (1) We propose a directed test generation technique to activate a target by effective utilization of concolic testing on RTL models. (2) We develop efficient learning and clustering techniques to minimize the overlapping searches across targets to drastically reduce the overall test generation effort. Experimental results demonstrate that our approach significantly outperforms the state-of-the-art methods in terms of test generation time (up to 205X, 69X on average) as well as memory requirements (up to 31X, 7X on average).

Hardware Trojans are serious threat to security and reliability of computing systems. It is hard to detect these malicious implants using traditional validation methods since an adversary is likely to hide them under rare trigger conditions. While existing statistical test generation methods are promising for Trojan detection, they are not suitable for activating extremely rare trigger conditions in stealthy Trojans. To address the fundamental challenge of activating rare triggers, we propose a new test generation paradigm for trigger activation by repeated maximal clique sampling (TARMAC). The basic idea is to utilize a satisfiability modulo theories (SMTs) solver to construct a test corresponding to each maximal clique. This article makes three fundamental contributions: 1) it proves that the trigger activation problem can be mapped to clique cover problem, and the test vectors generated by covering maximal cliques are complete and compact; 2) it proposes efficient test generation algorithms to activate trigger conditions by repeated maximal clique sampling; and 3) it outlines an efficient mechanism to run the clique sampling in parallel to significantly improve the scalability of our test generation framework. The experimental results demonstrate that our proposed approach is scalable and it outperforms state-of-the-art approaches by several orders-of-magnitude in detecting stealthy Trojans.

Detection of hardware Trojans is vital to ensure the security and trustworthiness of System-on-Chip (SoC) designs. Side-channel analysis is effective for Trojan detection by analyzing various side-channel signatures such as power, current, and delay. In this article, we propose an efficient test generation technique to facilitate side-channel analysis utilizing dynamic current. While early work on current-aware test generation has proposed several promising ideas, there are two major challenges in applying it on large designs: (i) The test generation time grows exponentially with the design complexity, and (ii) it is infeasible to detect Trojans, since the side-channel sensitivity is marginal compared to the noise and process variations. Our proposed work addresses both challenges by effectively exploiting the affinity between the inputs and rare (suspicious) nodes. The basic idea is to quickly find the profitable ordered pairs of test vectors that can maximize side-channel sensitivity. This article makes two important contributions: (i) It proposed an efficient test generation algorithm that can produce the first patterns in the test vectors to maximize activation of suspicious nodes using an SMT solver, and (ii) it developed a genetic-algorithm based test generation technique to produce the second patterns in the test vectors to maximize the switching in the suspicious regions while minimizing the switching in the rest of the design. Our experimental results demonstrate that we can drastically improve both the side-channel sensitivity (62× on average) and time complexity (13× on average) compared to the state-of-the-art test generation techniques.

Assertions are widely used for functional validation as well as coverage analysis for both software and hardware designs. Assertions enable runtime error detection as well as faster localization of errors. While there is a vast literature on both software and hardware assertions for monitoring functional scenarios, there is limited effort in utilizing assertions to monitor System-on-Chip (SoC) security vulnerabilities. We have identified common SoC security vulnerabilities and defined several classes of assertions to enable runtime checking of security vulnerabilities. A major challenge in assertion-based validation is how to activate the security assertions to ensure that they are valid. While existing test generation using model checking is promising, it cannot generate directed tests for large designs due to state space explosion. We propose an automated and scalable mechanism to generate directed tests using a combination of symbolic execution and concrete simulation of RTL models. Experimental results on diverse benchmarks demonstrate that the directed tests are able to activate security assertions non-vacuously.

A major challenge in assertion-based validation is how to activate the assertions to ensure that they are valid. While existing test generation using model checking is promising, it cannot generate directed tests for large designs due to state space explosion. We propose an automated and scalable mechanism to generate directed tests using a combination of symbolic execution and concrete simulation of RTL models. Experimental results show that the directed tests are able to activate assertions non-vacuously.

Hardware Trojans are serious threat to security and reliability of computing systems. It is hard to detect these malicious implants using traditional validation methods since an adversary is likely to hide them under rare trigger conditions. While existing statistical test generation methods are promising for Trojan detection, they are not suitable for activating extremely rare trigger conditions in stealthy Trojans. To address the fundamental challenge of activating rare triggers, we propose a new test generation paradigm by mapping trigger activation problem to clique cover problem. The basic idea is to utilize a satisfiability solver to construct a test corresponding to each maximal clique. This paper makes two fundamental contributions: 1) it proves that the trigger activation problem can be mapped to clique cover problem, 2) it proposes an efficient test generation algorithm to activate trigger conditions by repeated maximal clique sampling. Experimental results demonstrate that our approach is scalable and it outperforms state-of-the-art approaches by several orders-of-magnitude in detecting stealthy Trojans.

Side-channel analysis is widely used for hardware Trojan detection in integrated circuits by analyzing various side-channel signatures, such as timing, power and path delay. Existing delay-based side-channel analysis techniques have two major bottlenecks: (i) they are not suitable in detecting Trojans since the delay difference between the golden design and a Trojan inserted design is negligible, and (ii) they are not effective in creating robust delay signatures due to reliance on random and ATPG based test patterns. In this paper, we propose an efficient test generation technique to detect Trojans using delay-based side channel analysis. This paper makes two important contributions. (1) We propose an automated test generation algorithm to produce test patterns that are likely to activate trigger conditions, and change critical paths. Compared to existing approaches where delay difference is solely based on extra gates from a small Trojan, the change of critical paths by our approach will lead to significant difference in path delay. (2) We propose a fast and efficient reordering technique to maximize the delay deviation between the golden design and Trojan inserted design. Experimental results demonstrate that our approach significantly outperforms state-of-the-art approaches that rely on ATPG or random test patterns for delay-based side-channel analysis.

Network-on-chip (NoC) is widely employed by multicore system-on-chip (SoC) architectures to cater to their communication requirements. Increasing NoC complexity coupled with its widespread usage has made it a focal point of potential security attacks. Distributed denial-of-service (DDoS) is one such attack that is caused by malicious intellectual property (IP) cores flooding the network with unnecessary packets causing significant performance degradation through NoC congestion. In this article, we propose an efficient framework for real-time detection and localization of DDoS attacks. This article makes three important contributions. We propose a real-time and lightweight DDoS attack detection technique for NoC-based SoCs by monitoring packets to detect any violations. Once a potential attack has been flagged, our approach is also capable of localizing the malicious IPs using the latency data in the NoC routers. The applications are statically profiled during design time to determine communication patterns. These patterns are then used for real-time detection and localization of DDoS attacks. We have evaluated the effectiveness of our approach against different NoC topologies and architecture models using both real benchmarks and synthetic traffic patterns. Our experimental results demonstrate that our proposed approach is capable of real-time detection and localization of DDoS attacks originating from multiple malicious IPs in NoC-based SoCs.

Network-on-Chip (NoC) is widely employed by multi-core System-on-Chip (SoC) architectures to cater to their communication requirements. The increased usage of NoC and its distributed nature across the chip has made it a focal point of potential security attacks. Denial-of-Service (DoS) is one such attack that is caused by a malicious intellectual property (IP) core flooding the network with unnecessary packets causing significant performance degradation through NoC congestion. In this paper, we propose a lightweight and real-time DoS attack detection mechanism. Once a potential attack has been flagged, our approach is also capable of localizing the malicious IP using latency data gathered by NoC components. Experimental results demonstrate the effectiveness of our approach with timely attack detection and localization while incurring minor area and power overhead (less than 6% and 4%, respectively).

Simulation is widely used for validation of Register-Transfer-Level (RTL) models. While simulating with millions of random (or constrained-random) tests can cover majority of the targets (functional scenarios), the number of remaining targets can still be huge (hundreds or thousands) in case of today's industrial designs. Prior work on directed test generation using concolic testing can cover only one target at a time. A naive extension of prior work to activate the remaining targets would be infeasible due to wasted effort in multiple overlapping searches. In this paper, we propose an automated test generation technique for activating multiple targets in RTL models using concolic testing. This paper makes three important contributions. First, it efficiently prunes the targets that can be covered by the tests generated for activating the other targets. Next, it minimizes the overlapping searches while trying to generate tests for activating multiple targets. Finally, our approach effectively utilizes clustering of related targets as well as common path sharing between the targets in the same cluster to drastically reduce the test generation time. Experimental results demonstrate that our approach significantly outperforms the existing methods in terms of overall coverage (up to 5X, 1.2X on average) as well as test generation time (up to 146X, 80X on average).

Detection of hardware Trojans is vital to ensure the security and trustworthiness of System-on-Chip (SoC) designs. Side-channel analysis is effective for Trojan detection by analyzing various side-channel signatures such as power, current and delay. In this paper, we propose an efficient test generation technique to facilitate side-channel analysis utilizing dynamic current. While early work on current-aware test generation has proposed several promising ideas, there are two major challenges in applying it on large designs: (i) the test generation time grows exponentially with the design complexity, and (ii) it is infeasible to detect Trojans since the side-channel sensitivity is marginal compared to the noise and process variations. Our proposed work addresses both challenges by effectively exploiting the affinity between the inputs and rare (suspicious) nodes. We formalize the test generation problem as a searching problem and solve the optimization using genetic algorithm. The basic idea is to quickly find the profitable test patterns that can maximize switching in the suspicious regions while minimize switching in the rest of the circuit. Our experimental results demonstrate that we can drastically improve both the side-channel sensitivity (30x on average) and time complexity (4.6x on average) compared to the state-of-the-art test generation techniques.

Computing systems utilize multicore processors with complex cache coherence protocols to meet the increasing need for performance and energy improvement. It is a major challenge to verify the correctness of a cache coherence protocol since the number of reachable states grows exponentially with the number of cores. In this paper, we propose an efficient test generation technique, which can be used to achieve full state and transition coverage in simulation-based verification for a wide variety of cache coherence protocols. Based on effective analysis of the state space structure, our method can generate more efficient test sequences (50% shorter) on-the-fly compared with tests generated by BFS. While our on-the-fly method can reduce the numbers of required tests by half, it can still be impractical to verify all possible transitions in the presence of large number of cores. We propose scalable on-the-fly test generation techniques using quotient state space. The proposed approach guarantees selection of important transitions by utilizing equivalence classes, and omits only similar transitions. Our experimental results demonstrate that our proposed approaches can efficiently tradeoff between transition coverage and validation effort.