Pith. sign in

REVIEW 4 major objections 5 minor 48 references

Forbench: Symbolic Simulation Helps Make Your Testbench More Formal

T0 review · 4 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Forbench shows that a Python-style symbolic testbench can match formal tools on coverage and beat them on runtime

desk verdict Solid tool paper with a genuinely new testbench paradigm; evaluation is a bit soft on methodology, but the core idea holds up. read the letter →

arxiv 2608.01045 v1 pith:77RZQBND submitted 2026-08-02 cs.AR

Ziyi Yang , Wenbin Che , Ziyue Zheng , Guangyu Hu , Hongce Zhang This is my paper
classification cs.AR MSC 68Q6068T27
keywords formalverificationsymbolicsimulationtestbenchRTLSMTcoroutinesbranchcoveragehardware
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper claims that the barrier between simulation and formal verification can be lowered by keeping the operational, stimulus-driven style of a testbench while letting signals be symbolic and solver-backed. The author's central claim is that a word-level symbolic simulation framework, Forbench, achieves branch coverage comparable to the best existing formal and concolic tools while running substantially faster, and detects injected processor bugs in under four seconds where a symbolic-execution baseline takes hundreds to thousands of seconds. A sympathetic reader would care because it offers a practical third path: engineers do not have to write SystemVerilog Assertions or adopt an axiomatic mindset, yet they still get systematic, exhaustive exploration of bounded behaviors. The paper demonstrates this on processor-scale RTL designs, showing that the framework scales and that its testbench-driven forking, rather than design-driven path explosion, keeps the state space manageable.

What carries the argument

The central object is the symbolic state tuple $(M^t_s, \Phi^t, X^t)$: a map from state variables to symbolic expressions, a set of accumulated path constraints, and a set of fresh X-variables for unspecified inputs. When a wait-condition is encountered, the engine checks satisfiability of $\Phi \wedge E$ and $\Phi \wedge \neg E$ and forks the coroutine into two clones only when both are satisfiable. This condition-driven forking, together with expression simplification (independence/constant analysis, assumption-guided evaluation, ITE unreachable-case pruning, and word-level sweeping) is what keeps exploration tractable while preserving exhaustiveness over the bounded input space.

What would settle it

Run a design with known Verilog corner cases (e.g., a latch inferred from an incomplete if, or a module using 'x' assignments or tri-state buses) through the Forbench flow and compare the symbolic simulation result against a bit-exact reference simulator for a bounded exhaustive set of concrete inputs; a mismatch would show that the BTOR2 abstraction loses semantics. Alternatively, construct a testbench with a wait_condition that branches on a corner-case value and check whether the forking logic explores the unreachable branch.

Watch

Extended reading notes

Core claim

Forbench is a formal testbench paradigm where the testbench remains a familiar procedural Python program (active-stepping or coroutine-based) but signal values can be symbolic variables constrained by SMT formulas. The engine treats RTL as a state transition system, maintains symbolic state maps and path conditions, checks assertions by SMT satisfiability, and forks coroutines only when a wait-condition in the testbench is satisfiable in both directions. Because forking is driven by testbench conditions rather than by the design's branching, the number of concurrent symbolic states is dramatically lower than in symbolic execution. The paper's experimental claim is that this design achieves b

Load-bearing premise

The whole verification result rests on the assumption that the Yosys-generated BTOR2 model is a faithful, cycle-accurate representation of the original Verilog RTL, including corner-case semantics such as X/Z values, latches, and tristate logic; any semantic mismatch between Verilog and BTOR2 would void the claimed exhaustive coverage.

Editorial extensions

If this is right

  • Verification engineers can write a symbolic testbench in Python, keeping the structure they already use for simulation, and still obtain full bounded-input coverage rather than a single trace.
  • The framework's runtime advantage over prior symbolic simulators and STSearch/Hot-FV suggests that testbench-driven forking is a scalable way to reason about processor-scale RTL in pre-silicon validation.
  • Support for symbolic initial states enables modular inductive verification, allowing properties to be checked from arbitrary states rather than only from reset.
  • The coroutine-based style with symbolic wait-conditions offers a way to write overlapped I/O sequences that are notoriously tricky to express in SVA, reducing the risk of vacuous or over-constrained properties.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the approach generalizes beyond the evaluated designs, it could make formal verification a drop-in replacement for coverage-driven simulation in many industrial testbenches, since the same testbench code can be run concretely or symbolically by changing only a flag.
  • The testbench-condition-driven forking suggests a broader principle: verification complexity should scale with the number of user-posed questions, not with the design's internal control flow; this aligns with the paper's data showing few branches explored in the micro-riscv experiments.
  • One could test whether the runtime advantage persists when the testbench itself encodes many symbolic branches (e.g., complex protocol checks), since forking overhead grows with the number of wait-conditions; the paper does not isolate that cost.
  • The state-merging abstraction function is described but not exercised in the experiments; a targeted study on designs that do require merging would test its soundness and the practical cost of finding an over-approximating predicate.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. The paper presents Forbench, a word-level symbolic simulation framework for RTL verification that keeps a simulation-style, testbench-driven workflow while replacing concrete stimuli with SMT-backed symbolic values. It supports two testbench styles (active-stepping and coroutine-based), forks coroutines when a testbench wait condition is symbolically satisfiable in both directions, and optionally merges states via over-approximating predicates. The experiments claim three results: (1) Forbench is faster than the WASIM symbolic simulator and VossII on five designs while providing bounded symbolic coverage; (2) it reaches branch coverage comparable to prior formal/concolic tools (Pono, EBMC, STSearch, Hot-FV) on ITC'99 and processor benchmarks, with generally lower runtime; and (3) it detects all ten injected micro-riscv bugs in under 4 seconds per bug, versus hundreds to thousands of seconds for a symbolic-execution baseline. The paper also argues that testbench-level forking, rather than design-level branching, avoids path explosion and makes formal reasoning more accessible to simulation engineers.

Significance. If the empirical claims hold, Forbench is a useful step toward lowering the adoption barrier of formal methods: it preserves the familiar testbench structure, offers a Python interface, and demonstrates that symbolic simulation can scale to processor-scale RTL on branch-coverage and bug-finding tasks. The coroutine-forking mechanism and state-merging abstraction are technically interesting, and the public repository link makes the artifact potentially reproducible. However, the paper's central claims are empirical, and the evaluation as presented has several load-bearing methodological gaps that need to be addressed before the results can be considered reliable: model fidelity of the Yosys-to-BTOR2 path, baseline provenance and run-to-run variability, and the definition of the branch-coverage metric.

major comments (4)
  1. [§5.1 (Experiment Setup)] The entire evaluation is performed on BTOR2 models generated by Yosys from Verilog, but the paper never validates that this translation preserves the behavior and branch structure of the original RTL. BTOR2 is a bit-vector format that does not fully capture Verilog X/Z propagation, latches, tristate logic, and initial-block semantics; Yosys can also restructure branches during synthesis. Since Table 3 reports branch coverage and Table 4 reports bug detection, these results concern the synthesized model, not the Verilog design. I ask the authors to (i) state explicitly whether branch counts and coverage are measured on Verilog or BTOR2 artifacts, (ii) provide a differential-testing check between Forbench on BTOR2 and a Verilog simulator (Icarus/Verilator) on at least the benchmark designs, and (iii) discuss how X/Z and latch semantics are handled, or justify that the benchmarks do not dep
  2. [Table 3 and §5.3] The runtime and coverage comparison against previous tools is not sufficiently grounded. The paper does not state whether the Pono, EBMC, STSearch, Hot-FV, and Random columns were re-run in the same environment or copied from prior publications; the footnote about the 30,000-second limit applies only to Random, and even then it is unclear whether those runs were performed by the authors. If timings come from different machines or different tool versions, the 'significantly better runtime performance' claim is not apples-to-apples. Additionally, all numbers appear to be single runs with no variance information. Please rerun all baselines on the same machine and benchmark format, report at least the mean/range over several runs, and clearly indicate provenance for every column.
  3. [§5.4 and Table 4] The bug-finding comparison has two problems. First, the paper states that the injected bugs were 're-created' from the textual description in [18] because the official repository lacks buggy RTL; this introduces a risk that the bugs differ from the original ones in subtle but important ways (e.g., exact decode logic or X behavior). Second, the symbolic-execution baseline columns (#Exec Instr., Time, Partial Paths, Paths) appear to be taken from [18] rather than re-run on the same re-created designs and the same hardware. Without re-running the baseline on the identical RTL and machine, the speedup numbers in Table 4 are not a controlled comparison. Please re-run the baseline, or at least provide the provenance and a clear statement of what was measured where.
  4. [§5.3 (Branch coverage metric)] The paper does not define how branch coverage is computed. It reports a 'Branches' column and a 'Lines' column, and states that Forbench 'matches' the coverage of other tools, but there is no algorithm or tool configuration describing which branches are counted (e.g., Yosys BTOR2 cond nodes, Verilog if/case branches, synthesized control-flow guards), how unreachable branches are handled, and how the same metric is applied across all tools. This matters because the equality of Forbench's coverage with Hot-FV/Pono on several rows could be an artifact of different branch-mapping conventions. Please specify the exact coverage definition, the branch-count extraction method, and whether the same definition is used for every tool in Table 3.
minor comments (5)
  1. [Abstract] Typo: 'In additional to' should be 'In addition to'.
  2. [§5.2] Typo: 'owning to' should be 'owing to'.
  3. [Algorithm 2] The notation is confusing: the input and output both use S_t^1/S_t^2, and the pseudo-code references S_t^1 before any clone is created. Use S_t for the current state and S_t' (or S_t^true/S_t^false) for the forked states.
  4. [Fig. 2 and §4.1.2] The Python snippets use curly quotation marks and assign a string literal (e.g., dut.a.value = 'a0') where a symbolic variable object is presumably intended. Clarify the API and use straight ASCII quotes in the code examples.
  5. [Table 2] The VossII column mixes '>3600' (timeout) with 'N/A' (Yosys compatibility issue). The text says VossII could not complete a single cycle for AES or Rocket, but the table also shows N/A for other designs; please state explicitly which designs were attempted and which were excluded due to compatibility, as this affects the interpretation of 'outperforms VossII'.

Circularity Check

0 steps flagged · score 2.0 of 10

No significant circularity; self-citations are implementation details or baselines, not load-bearing reductions.

full rationale

Forbench is an empirical tool paper: the central claims are that its word-level symbolic simulation matches the branch coverage of existing formal/concolic tools while running faster, and that it detects injected processor bugs far more quickly than a symbolic-execution baseline. These claims are supported by measured experiments on external benchmarks (ITC'99, OR1200, Rocket, micro-riscv) against external tools (Icarus, Verilator, Wasim, VossII, Pono, EBMC, STSearch, and the symbolic-execution setup of Bruns et al.). I found no equation or procedure in which a predicted quantity is defined in terms of its own inputs, no fitted parameter that is later renamed a prediction, and no result that is forced by a self-citation chain. The self-citations present are: (1) [8] Wasim, for the relational handling of unspecified symbolic values; (2) [27] SMT-Sweep, for word-level sweeping/expression merging; and (3) [47] Hot-FV, which is used as a comparison baseline in the branch-coverage experiment. None of these is load-bearing as an authority for the paper's conclusions. The word-level sweeping technique is an optimization whose effect is demonstrated by measured runtimes; the coverage parity with Hot-FV is an empirical outcome, not a constructional identity, since both tools are measuring the same DUT branch structure independently. The equality of Forbench and Hot-FV coverage percentages might invite suspicion, but the paper provides no definitional link between them, and the most plausible reading is that both methods saturate the same feasible coverage ceiling. The unvalidated Yosys-to-BTOR2 translation is a genuine threat to validity—the reported coverage and bug detections are for the BTOR2 model, and semantic mismatch with Verilog could undermine the results—but that is a correctness risk, not circularity. It does not make the claims equivalent to their inputs. Accordingly, no concrete circular step can be exhibited, and the appropriate finding is no significant circularity aside from minor, non-load-bearing self-citation.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The paper's central claims are empirical and tool-based. They rest on the faithfulness of the BTOR2 frontend, the soundness of the SMT solver, and the correct execution of the Python testbench by the coroutine framework. No fitted parameters or new physical entities are introduced.

assumptions (4)
  • domain assumption The Yosys-generated BTOR2 model is a faithful cycle-accurate representation of the original Verilog RTL.
    Section 5.1 states designs are compiled to BTOR2 via Yosys; the symbolic simulation then operates on the BTOR2 model, so any Verilog-to-BTOR2 semantic mismatch would invalidate the coverage guarantees.
  • standard math The SMT solver (Bitwuzla) is sound and complete for the bit-vector and boolean formulas produced by the simulator.
    Algorithms 1 and 2 rely on satisfiability checks to decide forks, assertion violations, and abstraction; unsound or incomplete solver answers would produce false verification results.
  • domain assumption The Python testbench code used in the experiments is correctly interpreted by Forbench's custom coroutine framework, and arbitrary Python side effects are either absent or handled.
    Section 4.3 describes forking coroutines at wait_cond, but does not specify semantics for general Python control flow or side effects; the experiments presuppose that the testbench code falls within the supported subset.
  • domain assumption The over-approximating state merging in Section 4.4 preserves soundness of the analysis.
    Section 4.4 claims over-approximation preserves soundness, but no formal proof is given; however, this feature is not used in any of the presented experiments.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Forbench: Symbolic Simulation Helps Make Your Testbench More Formal." pith.science (2026). https://pith.science/paper/77RZQBND

@misc{pith2026260801045,
  author       = {Pith},
  title        = {Pith review of: Forbench: Symbolic Simulation Helps Make Your Testbench More Formal},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/77RZQBND}},
  note         = {Machine review of arXiv:2608.01045}
}
read the original abstract

Simulation remains the dominant approach in pre-silicon verification due to its ease of deployment and intuitive workflow. However, as simulation only explores a limited subset of possible execution traces within feasible time budgets, it often fails to explore rare corner cases, leaving latent bugs undetected. In contrast, formal verification offers mathematically rigorous guarantees of correctness. However, its practical adoption is constrained, not only by the scalability challenges over large-scale designs, but also by the change of mindset from stimulus-driven operations to the sequence-centric axiomatic view of design behaviors, introducing extra difficulty of writing precise properties to capture the exact verification intent. This paper aims to lower the barrier of applying formal methods in verification, by making simulation "more formal." It introduces Forbench, a word-level symbolic simulation framework that retains the familiar execution semantics of simulation but augments it with solver-backed symbolic signals and state transitions, enabling systematic exploration of RTL behaviors under symbolic inputs and conditions. It offers a Python interface, similar to the existing simulation-based frameworks, for defining constraints, coordinating symbolic (co-)simulations, and performing property checks. In additional to this more accessible interface, experiments also show that Forbench achieves notably speed-up over prior symbolic methods without the loss of coverage.

Figures

Figures reproduced from arXiv: 2608.01045 by the authors.

Figure 1
Figure 1. A motivating example showing how the intuitive [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. A demonstration of the Forbench verification methodology and the two testbench styles. Example ○a on the left uses the active-stepping style, which explicitly invokes “dut.step()” to advance to the next clock cycle. Example ○b on the right is coroutine-based, which allows concurrently interfacing with multiple DUT interfaces via separate coroutines. reusable manner, in SVA sequence composition is less intuitive. Mi￾… view at source ↗
Figure 3
Figure 3. An example demonstrating verification of a stream [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

48 extracted references · 46 canonical work pages

  1. [18]

    Processor verification using symbolic execution: A risc-v case-study

    Niklas Bruns, Vladimir Herdt, and Rolf Drechsler. Processor verification using symbolic execution: A risc-v case-study. In2023 Design, Automation & Test in Europe Conference & Exhibition (DATE), pages 1–6. IEEE, 2023

    work page 2023

  2. [1]

    Part 4: The 2020 wilson research group functional verifi- cation study

    Harry Foster. Part 4: The 2020 wilson research group functional verifi- cation study. Verification Horizons (Siemens EDA Blog), December 2020. URL https://blogs.sw.siemens.com/verificationhorizons/2020/12/02/part-4-the- 2020-wilson-research-group-functional-verification-study/. Accessed: 2025-09- 25

    work page 2020

  3. [2]

    Part 8: The 2022 wilson research group functional verifi- cation study

    Harry Foster. Part 8: The 2022 wilson research group functional verifi- cation study. Verification Horizons (Siemens EDA Blog), December 2022. URL https://blogs.sw.siemens.com/verificationhorizons/2022/12/12/part-8-the- 2022-wilson-research-group-functional-verification-study/. Accessed: 2025-09- 25

    work page 2022

  4. [3]

    Gem: Gpu-accelerated emulator-inspired rtl simulation

    Zizheng Guo, Yanqing Zhang, Runsheng Wang, Yibo Lin, and Haoxing Ren. Gem: Gpu-accelerated emulator-inspired rtl simulation. In2025 62nd ACM/IEEE Design Automation Conference (DAC), pages 1–7. IEEE, 2025

    work page 2025

  5. [4]

    Difuzzrtl: Differential fuzz testing to find cpu bugs

    Jaewon Hur, Suhwan Song, Dongup Kwon, Eunjin Baek, Jangwoo Kim, and Byoungyoung Lee. Difuzzrtl: Differential fuzz testing to find cpu bugs. In2021 IEEE Symposium on Security and Privacy (SP), pages 1286–1303. IEEE, 2021

    work page 2021

  6. [5]

    Rfuzz: Coverage-directed fuzz testing of rtl on fpgas

    Kevin Laeufer, Jack Koenig, Donggyu Kim, Jonathan Bachrach, and Koushik Sen. Rfuzz: Coverage-directed fuzz testing of rtl on fpgas. In2018 IEEE/ACM International Conference on Computer-Aided Design (ICCAD), pages 1–8. IEEE, 2018

    work page 2018

  7. [6]

    Fuzzing hardware like software

    Timothy Trippel, Kang G Shin, Alex Chernyakhovsky, Garret Kelly, Dominic Rizzo, and Matthew Hicks. Fuzzing hardware like software. In31st USENIX Security Symposium (USENIX Security 22), pages 3237–3254, 2022

    work page 2022

  8. [7]

    Fuzzbtor2: A random generator of word-level model checking problems in btor2 format

    Shengping Xiao, Chengyu Zhang, Jianwen Li, and Geguang Pu. Fuzzbtor2: A random generator of word-level model checking problems in btor2 format. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 36–43. Springer, 2023

    work page 2023

Show all 48 references
  1. [8]

    Wasim: A word-level abstract symbolic simula- tion framework for hardware formal verification

    Wenji Fang and Hongce Zhang. Wasim: A word-level abstract symbolic simula- tion framework for hardware formal verification. InInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 11–18. Springer, 2023

    2023

  2. [9]

    Deeply optimizing the sat solver for the ic3 algorithm

    Yuheng Su, Qiusong Yang, Yiwei Ci, Yingcheng Li, Tianjun Bu, and Ziyu Huang. Deeply optimizing the sat solver for the ic3 algorithm. InInternational Conference on Computer Aided Verification, pages 237–257. Springer, 2025

    2025

  3. [10]

    Symbolic model checking without bdds

    Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. Symbolic model checking without bdds. InInternational conference on tools and algorithms for the construction and analysis of systems, pages 193–207. Springer, 1999

    1999

  4. [11]

    Efficient implementation of property directed reachability

    Niklas Eén, Alan Mishchenko, and Robert Brayton. Efficient implementation of property directed reachability. In2011 Formal Methods in Computer-Aided Design (FMCAD), pages 125–134. IEEE, 2011

    2011

  5. [12]

    Automatic verification of finite-state concurrent systems using temporal logic specifications.ACM Transactions on Programming Languages and Systems (TOPLAS), 8(2):244–263, 1986

    Edmund M Clarke, E Allen Emerson, and A Prasad Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications.ACM Transactions on Programming Languages and Systems (TOPLAS), 8(2):244–263, 1986

    1986

  6. [13]

    Model checking

    Edmund M Clarke. Model checking. InInternational conference on foundations of software technology and theoretical computer science, pages 54–56. Springer, 1997

    1997

  7. [14]

    Handbook of model checking, volume 10

    Edmund M Clarke, Thomas A Henzinger, Helmut Veith, Roderick Bloem, et al. Handbook of model checking, volume 10. Springer, 2018

    2018

  8. [15]

    A survey of symbolic execution techniques.ACM Computing Surveys (CSUR), 51(3):1–39, 2018

    Roberto Baldoni, Emilio Coppa, Daniele Cono D’elia, Camil Demetrescu, and Irene Finocchi. A survey of symbolic execution techniques.ACM Computing Surveys (CSUR), 51(3):1–39, 2018

    2018

  9. [16]

    En- hancing symbolic execution with veritesting

    Thanassis Avgerinos, Alexandre Rebert, Sang Kil Cha, and David Brumley. En- hancing symbolic execution with veritesting. InProceedings of the 36th interna- tional conference on software engineering, pages 1083–1094, 2014

    2014

  10. [17]

    Satisfiability modulo theories

    Clark Barrett and Cesare Tinelli. Satisfiability modulo theories. InHandbook of model checking, pages 305–343. Springer, 2018

    2018

  11. [19]

    Verilator and systemperl

    Wilson Snyder. Verilator and systemperl. InNorth American SystemC Users’ Group, Design Automation Conference, volume 79, pages 122–148, 2004

    2004

  12. [20]

    Klee: unassisted and automatic generation of high-coverage tests for complex systems programs

    Cristian Cadar, Daniel Dunbar, Dawson R Engler, et al. Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI, volume 8, pages 209–224, 2008

    2008

  13. [21]

    Symbolic trajectory evaluation

    Scott Hazelhurst and Carl-Johan H Seger. Symbolic trajectory evaluation. In Formal hardware verification: Methods and systems in comparison, pages 3–78. Springer, 2005

    2005

  14. [22]

    Replacing testing with formal verification in intel coretm i7 processor execution engine validation

    Roope Kaivola, Rajnish Ghughal, Naren Narasimhan, Amber Telfer, Jesse Whitte- more, Sudhindra Pandav, Anna Slobodova, Christopher Taylor, Vladimir Frolov, Erik Reeber, and Armaghan Naik. Replacing testing with formal verification in intel coretm i7 processor execution engine v...

    2009 doi

  15. [23]

    Jin Yang and C.-J.H. Seger. Introduction to generalized symbolic trajectory evaluation.IEEE Transactions on Very Large Scale Integration (VLSI) Systems, 11 (3):345–353, 2003. doi: 10.1109/TVLSI.2003.812320

    2003

  16. [24]

    C. J. Seger. The VossII hardware verification suite. https://github.com/TeamVoss/ VossII, 2020

    2020

  17. [25]

    Picker: A multilingual verification tool for hardware design and validation

    XS-MLVP Team. Picker: A multilingual verification tool for hardware design and validation. https://github.com/XS-MLVP/picker, 2025

    2025

  18. [26]

    Cocotb: a python-based digital logic verification frame- work

    Benjamin John Rosser. Cocotb: a python-based digital logic verification frame- work. InMicro-electronics Section seminar. CERN, Geneva, Switzerland, 2018

    2018

  19. [27]

    Smt- sweep: Word-level representation unification for hardware verification, 2025

    Ziyi Yang, Guangyu Hu, Mingkai Miao, Changyuan Yu, and Hongce Zhang. Smt- sweep: Word-level representation unification for hardware verification, 2025. URL https://arxiv.org/abs/2507.02008

    2025

  20. [28]

    Goldmine: Automatic assertion generation using data mining and static analysis

    Shobha Vasudevan, David Sheridan, Sanjay Patel, David Tcheng, Bill Tuohy, and Daniel Johnson. Goldmine: Automatic assertion generation using data mining and static analysis. In2010 Design, Automation & Test in Europe Conference & Exhibition (DATE 2010), pages 626–629. IEEE, 2010

    2010

  21. [29]

    The seahorn verification framework

    Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A Navas. The seahorn verification framework. InInternational Conference on Computer Aided Verification, pages 343–361. Springer, 2015

    2015

  22. [30]

    Program verification with constrained horn clauses

    Arie Gurfinkel. Program verification with constrained horn clauses. InInterna- tional Conference on Computer Aided Verification, pages 19–29. Springer, 2022

    2022

  23. [31]

    Symbolic quick error detection using symbolic initial state for pre-silicon verification

    Mohammad Rahmani Fadiheh, Joakim Urdahl, Srinivas Shashank Nuthakki, Sub- hasish Mitra, Clark Barrett, Dominik Stoffel, and Wolfgang Kunz. Symbolic quick error detection using symbolic initial state for pre-silicon verification. In2018 Design, Automation & Test in Europe Confe...

    2018

  24. [32]

    Smt-switch: a solver-agnostic c++ api for smt solving

    Makai Mann, Amalee Wilson, Yoni Zohar, Lindsey Stuntz, Ahmed Irfan, Kristo- pher Brown, Caleb Donovick, Allison Guman, Cesare Tinelli, and Clark Barrett. Smt-switch: a solver-agnostic c++ api for smt solving. InInternational Conference on Theory and Applications of Satisfiabil...

    2021

  25. [33]

    Bitwuzla

    Aina Niemetz and Mathias Preiner. Bitwuzla. InInternational Conference on Computer Aided Verification, pages 3–17. Springer, 2023

    2023

  26. [34]

    Btor2, btormc and boolector 3.0

    Aina Niemetz, Mathias Preiner, Clifford Wolf, and Armin Biere. Btor2, btormc and boolector 3.0. InInternational Conference on Computer Aided Verification, pages 587–595. Springer, 2018

    2018

  27. [35]

    Yosys-a free Verilog synthesis suite

    Clifford Wolf and Johann Glaser. Yosys-a free Verilog synthesis suite. InProceed- ings of the 21st Austrian Workshop on Microelectronics (Austrochip), volume 97, 2013

    2013

  28. [36]

    Icarus verilog: open-source verilog more than a year later.Linux Journal, 2002(99):3, 2002

    Stephen Williams and Michael Baxter. Icarus verilog: open-source verilog more than a year later.Linux Journal, 2002(99):3, 2002

    2002

  29. [37]

    Hardware-implementation-of-aes-verilog

    Vamshi Pasala Narayan. Hardware-implementation-of-aes-verilog. https://github. com/pnvamshi/Hardware-Implementation-of-AES-Verilog. [Online; accessed 2025-10-21]

    2025

  30. [38]

    Asanovic et al

    K. Asanovic et al. The rocket chip generator. Technical Report UCB/EECS-2016- 17, Dept. EECS, Univ. California, Berkeley, CA, USA, 2016

    2016

  31. [39]

    Piccolo: Risc-v cpu, simple 3-stage pipeline, for low-end applica- tions

    Bluespec, Inc. Piccolo: Risc-v cpu, simple 3-stage pipeline, for low-end applica- tions. [Online], 2018. Available: https://github.com/bluespec/Piccolo

    2018

  32. [40]

    Flute: Risc-v cpu, simple 5-stage in-order pipeline

    Bluespec, Inc. Flute: Risc-v cpu, simple 5-stage in-order pipeline. [Online], 2018. Available: https://github.com/bluespec/Flute

    2018

  33. [41]

    Ridecore: Risc-v dynamic execution core, an out-of-order risc-v proces- sor written in verilog hdl

    Kise Lab. Ridecore: Risc-v dynamic execution core, an out-of-order risc-v proces- sor written in verilog hdl. [Online], 2016. Available: https://github.com/ridecore/ ridecore

    2016

  34. [42]

    OR1200 source code, 2020

    OpenRISC. OR1200 source code, 2020. [Online]. Available: https://github.com/ openrisc/or1200

    2020

  35. [43]

    Characteristics of the itc’99 benchmark circuits

    Scott Davidson. Characteristics of the itc’99 benchmark circuits. InIEEE Interna- tional Test Synthesis Workshop (ITSW), volume 87, 1999

    1999

  36. [44]

    Pono: a flexible and extensible smt-based model checker

    Makai Mann, Ahmed Irfan, Florian Lonsing, Yahan Yang, Hongce Zhang, Kristo- pher Brown, Aarti Gupta, and Clark Barrett. Pono: a flexible and extensible smt-based model checker. InInternational Conference on Computer Aided Verifi- cation, pages 461–474. Springer, 2021

    2021

  37. [45]

    Kroening and M

    D. Kroening and M. Purandare. EBMC: The enhanced bounded model checker. [Online], 2022. Available: http://www.cprover.org/ebmc, accessed: 2022

    2022

  38. [46]

    Stsearch: State tracing-based search heuristics for rtl validation

    Ziyue Zheng and Yangdi Lyu. Stsearch: State tracing-based search heuristics for rtl validation. In2023 Design, Automation & Test in Europe Conference & Exhibition (DATE), pages 1–6. IEEE, 2023

    2023

  39. [47]

    Hot-fv: A semi-formal test generation framework for rtl functional coverage using warm starting states

    Ziyue Zheng, Zhiyuan Yan, Xiangchen Meng, Guangyu Hu, Hongce Zhang, and Yangdi Lyu. Hot-fv: A semi-formal test generation framework for rtl functional coverage using warm starting states. InProceedings of the IEEE International Conference on Computer Design (ICCD), 2025

    2025

  40. [48]

    MicroRV32

    Sallar Ahmadi-Pour and Rolf Drechsler. MicroRV32. URL https://github.com/agra- uni-bremen/microrv32/

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.