Assertion-based verification (ABV) is a critical method to ensure logic designs comply with their architectural specifications. ABV requires assertions, which are generally converted from specifications through human interpretation by verification engineers. Existing methods for generating assertions from specification documents are limited to sentences extracted by engineers, discouraging their practical applications. In this work, we present AssertLLM, an automatic assertion generation framework that processes complete specification documents. AssertLLM can generate assertions from both natural language and waveform diagrams in specification files. It first converts unstructured specification sentences and waveforms into structured descriptions using natural language templates. Then, a customized Large Language Model (LLM) generates the final assertions based on these descriptions. Our evaluation demonstrates that AssertLLM can generate more accurate and higher-quality assertions compared to GPT-4o and GPT-3.5.

Hardware verification is crucial to ensure the cor-rectness in the logic design of digital circuits. The purpose of verification is to either find bugs or show their absence. Prior works mostly focus on the bug-finding process and have proposed a range of verification algorithms and techniques to be faster to reach a bug or conclude with a proof of correctness. However, for a human verification engineer, it also matters how to better analyze the counterexamples trace to understand the root cause of bugs. This kind of technique remains absent in word-level circuit analysis. In this paper, we investigate the counterexample reduction method. Given the existing techniques for the bit-level circuit model, we first extend current semantic analysis methods to the word-level counterexample reduction and then develop a more efficient word-level structural analysis approach. We compare the effectiveness and overhead of these methods on the hardware model-checking problems and show the usefulness of such analysis in applications including pivot input analysis, word-level model-checking and counterexample-guided abstraction refinement.

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.

Though graph neural networks (GNNs) have been used in SAT solution prediction, for a subset of symmetric SAT problems, we unveil that the current GNN-based end-to-end SAT solvers are bound to yield incorrect outcomes as they are unable to break symmetry in variable assignments. In response, we introduce AsymSAT, a new GNN architecture coupled where a recurrent neural network is (RNN) to produce asymmetric models. Moreover, we bring up a method to integrate machine-learning-based SAT assignment prediction with classic SAT solvers and demonstrate its performance on non-trivial SAT instances including logic equivalence checking and cryptographic analysis problems with as much as 75.45% time saving.

Formal verification has been widely adopted to check logic correctness. One of the challenges in formal verification is how to quickly reach a formal proof for a user-specified property. This is especially difficult when the property involves word-level reasoning. In this work, we propose to augment the target property with additional conjectures automatically learned from simulation traces. The conjectures are generated by a reinforcement learning model, which dynamically expands production rules according to observations from simulation. Experiments show that our property strengthening method achieves notable speed-up on multiple verification tasks, including sequential equivalence checking and word-level property checking.