Abstract Solving constraints involving inductive (aka recursive) definitions is challenging. State-of-the-art SMT/CHC solvers and first-order logic provers provide only limited support for solving such constraints, especially when they involve, e.g., abstract data types. In this work, we leverage structured prompts to elicit Large Language Models (LLMs) to generate auxiliary lemmas that are necessary for reasoning about these inductive definitions. We further propose a neuro-symbolic approach, which synergistically integrates LLMs with constraint solvers: the LLM iteratively generates conjectures, while the solver checks their validity and usefulness for proving the goal. We evaluate our approach on a diverse benchmark suite comprising constraints originating from algebraic data types and recurrence relations. The experimental results show that our approach can improve the state-of-the-art SMT and CHC solvers, solving considerably more (around 25%) proof tasks involving inductive definitions, demonstrating its efficacy.

Modern processors are becoming increasingly complicated, making them hard to be bug-free. Bounded model checking (BMC) and coverage-guided fuzzing (CGF) are two main complementary techniques for verifying processors. BMC can exhaustively explore the state-space upto a given path-depth bound, but suffers from the infamous state-space explosion problem, thus limited to smaller bounds for realistic processor designs. CGF is efficient and scalable for verifying large-scale complex designs, but struggles with the coverage due to the difficulty in generating comprehensive and diverse seeds. To bring the best of both worlds, we propose BMCFuzz, a novel two-way hybrid verification approach that synergistically integrates BMC and CGF. Specifically, BMCFuzz alternatively switches BMC and CGF according to their performance in improving coverage, where CGF is leveraged to quickly explore the state space, detect flaws, and moreover record snapshots that are crucial valuations of all the circuit-level registers, while BMC with selected high-valuable snapshots as initial states is utilized to exhaustively explore uncovered points. Moreover, the witnesses of BMC are further used to generate seeds for CGF. This synergistic integration of BMC and CGF helps BMC alleviate the state-space explosion problem and feeds CGF with more high-quality seeds. We implement BMCFuzz as a fully open-source tool and evaluate it on three well-known open-source RISC-V processor designs (i.e., NutShell, Rocket, and BOOM). Experimental results show that BMCFuzz achieves higher coverage compared to the state-of-the-art methods and discovers three previously unknown bugs, demonstrating the potential of BMCFuzz as a powerful, open-source tool for advancing processor design and verification.

Chisel is an open-source hardware description language embedded in Scala to facilitate parameterized and reusable digital circuit design. Chisel is becoming increasingly popular and has been used to design RISC-V CPUs, e.g. RocketChip and XiangShan. While Chisel features high-level hardware designs, its verification is still low-level: Low-level (e.g. Verilog) programs are first generated from Chisel programs, then the verification tools are applied to these low-level programs. In this work, we focus on formal verification of arithmetic units. Efficient low-level formal verification of arithmetic units has always been a challenge and remains an active research area, attributed to the state explosion problem brought on by bit widths. To circumvent this problem for arithmetic Chisel designs, we propose an approach to their high-level formal verification so that their correctness is verified for all bit widths at once, instead of for each bit width separately. The key idea is to transform arithmetic Chisel designs into Scala software programs that simulate their behaviors, where the high-level features are preserved, then resort to Stainless, a deductive formal verification tool for Scala. We validate the effectiveness of this approach by formally verifying the correctness of dividers and multipliers in two representative open source RISC-V processors, namely, RocketChip and XiangShan. Compared to the existing proof-assistant-based parameterized verification approaches for arithmetic designs (e.g. Kami), the verification cost in our approach is much lower on average.

Abstract The determinization of a nondeterministic Büchi automaton (NBA) is a fundamental construction of automata theory, with applications to probabilistic verification and reactive synthesis. The standard determinization constructions, such as the ones based on the Safra-Piterman’s approach, work on the whole NBA. In this work we propose a divide-and-conquer determinization approach. To this end, we first classify the strongly connected components (SCCs) of the given NBA as inherently weak, deterministic accepting, and nondeterministic accepting. We then present how to determinize each type of SCC independently from the others; this results in an easier handling of the determinization algorithm that takes advantage of the structure of that SCC. Once all SCCs have been determinized, we show how to compose them so to obtain the final equivalent deterministic Emerson-Lei automaton, which can be converted into a deterministic Rabin automaton without blow-up of states and transitions. We implement our algorithm in our tool COLA and empirically evaluate COLA with the state-of-the-art tools Spot and Owl on a large set of benchmarks from the literature. The experimental results show that our prototype COLA outperforms Spot and Owl regarding the number of states and transitions.