hardware verification engineers

Abstract: Large language models are increasingly used to generate SystemVerilog Assertions from natural-language specifica- tions and register-transfer-level designs. Existing datasets and benchmarks support important goals such as large- scale training, formal evaluation, specification-to-assertion generation, and mutation-based testing. A complemen- tary need is to study whether a generated assertion cap- tures externally observable behavior or depends on inci- dental details of one RTL implementation. We present EquivSVA, a formally verified dataset organized around behavior families. Each family contains four structurally distinct RTL implementations of the same externally ob- servable behavior, shared interface-level gold properties, three controlled mutants, and formal-validation evidence. EquivSVA contains 120 behavior families across 12 cat- egories, 480 reference RTL implementations, 914 gold properties, and 360 mutants. Every final family passes a fixed 17-job validation suite covering RTL equivalence, gold-property proofs, property reachability, mutant dis- tinguishability, and gold-property checks on mutants. We also provide fixed family-safe train, development, and test splits. As a small demonstration of the analyses en- abled by the dataset, we evaluate the publicly released, Apache-2.0-licensed Qwen2.5-Coder-7B-Instruct model on the held-out test split. Of 293 interface-only generated properties, 93 are formally sound, and the number of sound properties varies across equivalent implementations for 14 of 24 test families. These results illustrate how behavior-family organization can support controlled stud- ies of assertion-generation robustness without requiring changes in intended functionality. The dataset, generators, validation scripts, and case-study artifacts are publicly released at https://github.com/aditigupta96/EquivSVA.

Abstract: Adiabatic logic reuses the energy stored on load capacitances through quasi-reversible switching, enabling a lower minimum energy consumption than conventional static CMOS. Yet its practicality in FinFET technologies and at multi-GHz clock rates has yet to be investigated. This work provides a systematic evaluation of Positive Feedback Adiabatic Logic (PFAL) simulated in the TSMC 16nm FinFET process. A set of PFAL standard-cell gates were realised, along with two representative combinational circuits - a 2$\times$2 multiplier and a 4-bit comparator - and compared against static CMOS logic using the energy--delay product (EDP) and the energy advantage metric $η= E_{\mathrm{CMOS}} / E_{\mathrm{PFAL}}$. Transient simulations reveal three sources of non-adiabatic loss: two specific to the PMOS/NMOS latch, threshold-voltage-related loss and a previously unreported redundant charging of the output node and one related to the complexity of PFAL logic trees. The low-threshold Buffer/NOT cell achieves a minimum EDP of $1.23\times10^{-26}$J$\cdot$s at $V_{\mathrm{CLK}} = 0.6$V and $f_{\mathrm{CLK}} = 7.94$GHz, while PFAL preserves an energy benefit over static CMOS of up to roughly $5\times$ at reduced frequencies and elevated supply voltages. A parallel-coupled quadrature voltage-controlled oscillator is designed as a realistic four-phase power-clock generator. With this non-ideal supply, the Buffer/NOT energy stays within $2\%$ of the ideal sinusoidal case at $3$GHz. A loading study quantifies the phase shift and amplitude reduction induced by increasing fan-out. Overall, the results provide a design-oriented evaluation of PFAL in 16nm FinFET and a motivation to exploit adiabatic logic for future low-power system architectures.

Abstract: Reusing a set of verified security assertions across RISC-V processor targets remains one of the most expensive bottlenecks in hardware security verification. Manual translation takes hours per assertion. Raw LLM translation is fast but unreliable, introducing signal hallucination, where the model invents port names absent from the target RTL and produces outputs that may vary across model updates or even within the same model version. This paper presents AutoTrans, an automated framework that addresses the above shortcomings. First, a new lightweight Regular Expression-based System Verilog signal extractor is proposed to identify the signals for generating security assertions. This step is necessary to prevent signal hallucination. Second, a template is introduced to create prompt and pinned inference parameters that guarantee a byte-identical prompt assembly on every run, making the pipeline output resilient to model updates. Moreover, the introduced template for LLM prompting is capable of generating security assertions from English-only security descriptions of RISC-V processors, with no manual authoring. Third, a formal verification process (JasperGold FPV) is integrated, which guarantees that the generated security assertions verify the security of the RISC-V processor rather than silently entering the result set. The workflow is applied on Deepseek V4 to translate security assertions from one RISC-V to another (e.g., for IBEX from NS31A RISC-V). The experiment shows that AutoTrans achieves 78\% Auto Translation Acceptance Rate (TAR) automatically and without human intervention and 100\% Final TAR after refinement by humans.