A promising approach for security verification of a Register-Transfer Level (RTL) design is assertion-based verification (ABV), where desired properties are expressed as SystemVerilog Assertions (SVAs). To create assertions, verification engineers typically start with identifying the relevant modules and necessary variables that are relevant to a given property and then construct the assertion based on those variables. While there have been several attempts to automate assertion creation, prior work identified that automatically recognizing relevant modules and subsequently extracting the required variables within the found module to construct an SVA is a bottleneck. Recently, Large Language Models (LLMs) have emerged, demonstrating promising code generation capabilities. However, their application in helping to automate valid SVA generation, along with the combination of static analysis methods, remains not well explored. This work investigates whether, and to what extent, LLMs can assist in each stage of the automation pipeline or whether their promise requires more evidence to substantiate. This study identifies specific areas where Large Language Models (LLMs) yield measurable and practical improvements in a hybrid workflow, as well as areas where their limitations are evident.

Due to outsource manufacturing, the semiconductor industry must deal with various hardware threats such as piracy and overproduction. To prevent illegal electronic products from functioning, the circuit can be encrypted using a protected key only known to the designer. However, an attacker can still decipher the secret key utilizing a functioning circuit bought from the market, and the encrypted layout leaked from an untrusted foundry. In this paper, after introducing essential conformity and mutuality features for secure logic encryption, we propose DLE, a novel Distributed Logic Encryption design that resists against all known oracle guided and structural attacks including the newly proposed fault-aided SAT-based attack that iteratively injects a single stuck-at fault to thwart the locking effect. DLE forces the attacker to insert multiple stuck-at faults simultaneously in critical points to achieve a smaller but meaningful encrypted circuit; thus, exponentially reducing the chance to hit all the critical points with properly located stuck-at fault injections. Our experiments confirm that DLE maintains an exponentially high degree of security under diverse attacks with the polynomial area and linear performance overheads.

Hardware IP owners must envision procedures to avoid piracy and overproduction of their designs under a fabless paradigm. A newly proposed technique to obfuscate critical components in a logic design is called eFPGA-based redaction, which replaces a sensitive sub-circuit with an embedded FPGA, and the eFPGA is configured to perform the same functionality as the missing sub-circuit. In this case, the configuration bitstream acts as a hidden key only known to the hardware IP owner. In this paper, we first evaluate the security promise of the existing eFPGA-based redaction algorithms as a preliminary study. Then, we break eFPGA-based redaction schemes by an initial but not necessarily efficient attack named DIP Exclusion that excludes problematic input patterns from checking in a brute-force manner. Finally, by combining cycle breaking and unrolling, we propose a novel and powerful attack called Break & Unroll that is able to recover the bitstream of state-of-the-art eFPGA-based redaction schemes in a relatively short time even with the existence of hard cycles and large size keys. This study reveals that the common perception that eFPGA-based redaction is by default secure against oracle-guided attacks, is prejudice. It also shows that additional research on how to systematically create an exponential number of non-combinational hard cycles is required to secure eFPGA-based redaction schemes.