Emergent Hardware Verification

Contents

Preface

Hardware is concurrent by nature. A chip is a population of state machines — flip-flops, blocks, IPs — that hold local state and influence one another only through signals on wires. For decades the software that verifies that hardware has been built on a different shape entirely: object hierarchies, sequential procedures, centralized schedulers. Much of verification’s cost traces back to that mismatch.

This book takes the opposite starting point. It models hardware with the one model of computation that already matches it: the actor model, in which independent units hold private state and communicate only through typed messages — here over an explicit, statically declared topology. Verification engineers already think this way — event-driven processes communicating through signal events are how Verilog itself works — and the framework lifts that familiar shape to the transaction level. The methodology that results is Emergent Verification: the verification architecture grows feature by feature, in a lightweight and composable structure, rather than being decided in full at the outset, and formal proof moves to the earliest stage of block development, so each block carries an executable formal contract before it is integrated. The consequences of that one choice run the length of the design flow, beginning with the book’s own title.

When a design and the environment that verifies it are written as one actor graph, that single authored artifact crosses every boundary of the flow as a re-rendering, never a rewrite: an executable specification, an architecture model, a formally proven block, a simulation testbench, a synthesizable netlist, and a hardware-emulation image are all the same actors, rendered for a different substrate. An actor is a finite state machine; finite state machines synthesize; so the verification environment — scoreboards, coverage, the register layer, and the rest — becomes hardware too when you need it to. Verification stops being a separate codebase that restarts at each boundary and becomes the specification itself, run with checkers attached, carried all the way down to gates. And because that same model reaches beyond verification into design, synthesis, and emulation, the book is Emergent Hardware Verification.

The methodology the industry standardized does not have this property, and it is worth being precise about why. Verification matured rapidly over two decades: Specman e brought Aspect-Oriented Programming to the domain, Vera and then SystemVerilog brought Object-Oriented Programming, and a succession of methodologies — eRM and RVM, then VMM, AVM, and OVM — culminated in UVM, standardized as IEEE Std 1800.2 and now the primary functional-verification methodology: the realization of Coverage-Driven Verification in a class library. UVM was designed for one class of problem — structured, sequence-driven bus protocols — and is built from a monolithic component hierarchy a team must stand up in full before the first feature can be checked. Two properties follow that the rest of the book returns to. A UVM environment is non-synthesizable and host-resident by construction, so it cannot follow the design onto an emulator without being discarded and re-coded. And a small change in the verification plan ripples across the hierarchy. Asynchronous multi-clock events, distributed multi-die coherence, and on-the-fly reconfiguration — the substance of modern SoCs — map poorly onto that hierarchy, and teams routinely spend more effort bending the framework to a new domain than writing the verification logic itself.

Picking the model once is what makes the verification investment compound rather than restart. Chapters 1–7 develop the methodology at IP and SoC scale across the three legs of a modern sign-off — formal proof (Chapter 3), simulation (Chapters 4–6), and hardware emulation (Chapter 7) — run concurrently in a sprint cycle that converges on a near-zero-bug tape-out. Chapter 7 is where the single-model choice pays its largest dividend: because the actor testbench is synthesizable in full, its conversion from simulation onto a commercial emulator, or onto an open FPGA-accelerated simulator, is automatic — a build target rather than the multi-week specialist port the status quo pays — and covers the whole verification environment, scoreboards and coverage included, not the design alone. The appendices carry the same model outward and downward: a complete specification-to-silicon continuum, the synthesizable form taken through place-and-route to an FPGA bitstream, AI-assisted RTL generation, distributed regression across machines and languages, and — at the largest scale — GPUs, AI accelerators, and the training and inference clusters they form, which are themselves actor systems (Appendix M).

The book covers both traditions. It develops the verification architecture and design-pattern vocabulary any methodology rests on (Chapter 4), UVM as the industry-standard realization of it (Chapter 5) — enough to read, extend, and debug real UVM environments with confidence — and the actor-based alternative as the contribution (Chapter 6 and the appendices). A reader can take the actor methodology on its own terms, or as a calibrated step from the UVM they already know.

Intended Audience

This book targets verification engineers, design engineers, system architects, and design managers seeking a more agile, scalable approach to hardware verification — and, in its later reach, to hardware design itself. It is particularly valuable for:

• • Verification Engineers wrestling with UVM’s setup cost and rigid component hierarchy.

• • Design (RTL) Engineers who will recognize their own world in the actor model — hardware modules are actors — and who can follow the synthesizable form from a three-line class to placed-and-routed gates.

• • Architects looking to implement verification strategies that evolve concurrently with the design, and to carry one executable model from specification to silicon.

• • Students and Researchers studying how OOP, the actor model, formal methods, and hardware verification connect.

Prerequisites

To get the most out of this book, readers should have:

• • A fundamental understanding of digital logic design and the SoC design flow.

• • Familiarity with SystemVerilog (or Verilog) as a hardware description language.

• • Basic OOP exposure helps but is not required — Chapter 4 covers the SystemVerilog OOP patterns the book uses, and Chapter 5 applies them.

Book Organization

• • Chapter 1: Foundations — SoC, Models of Computation, and the Path to Emergent Verification
  Establishes the verification-methodology landscape: the Models of Computation ladder that places hardware and testbenches at different tiers, the SoC architectural primitives, the two-axis abstraction grid (Computation \(\times \) Communication) that locates TLM and RTL, and the verification-flow scopes (block, integration, system). Introduces the industry-standard Coverage-Driven Verification (CDV) and identifies its structural limits. Introduces Emergent Verification as the alternative: adaptive planning, lightweight architecture, and a Formal/Simulation/Emulation pipeline running concurrently in a sprint cycle that converges on a near-zero-bug tape-out.

• • Chapter 2: RTL Design and Its Formal Contract
  Describes how RTL modeling is implemented in SystemVerilog and how temporal logic captures executable specifications, spanning six worked designs — round-robin arbiter, asynchronous handshake, FIFO, pipelined ALU, MSI cache coherence controller, and memory controller — each one earning a formal abstraction for the toolbox, from symbolic clients through predicate abstraction with the CEGAR loop to counter and memory abstraction.

• • Chapter 3: Formal Verification
  Takes the SVA properties written alongside the RTL in Chapter 2 and shows how a modern tool proves them. Develops the end-to-end formal flow (specification capture, block-level proof, module composition with assume–guarantee, subsystem and SoC scope with abstraction, and the sign-off artifact a tape-out review will ask for), walks the five proof engines that close the proof (CDCL, BMC, \(k\)-induction, Craig interpolation, IC3/PDR), lifts SAT to SMT for datapath work, frames the modern push-button orchestrator that runs all engines in parallel underneath one user-facing command, and then climbs past the automation ceiling into theorem proving — the Booth-multiplier proof worked end-to-end in Lean, the industrial FPU pyramid, and the AI-assisted proving frontier. Unusually for a formal-verification text, every engine taught here is also built: the companion implements each one from scratch, small enough to read and strong enough to prove every contract Chapter 2 printed, with an opt-in trace that narrates each solver step by name.

• • Chapter 4: TLM Verification Architecture
  Transitions from static to dynamic architectures via Object-Oriented Programming (OOP). Highlights the Meta-Pattern of OOP for encapsulation and polymorphism, the mechanics of Constraint-Driven Randomization, coverage, and virtual interfaces connecting dynamic software to static hardware. Establishes the layered verification architecture and the design-pattern vocabulary that any specific methodology (Chapter 5’s UVM, Chapter 6’s actor framework) goes on to implement.

• • Chapter 5: UVM: A Verification Framework
  Develops UVM as one industry-standard realization of the verification architecture from Chapter 4. Names the eight design patterns inside UVM’s base-class library, opens up the framework’s mechanics (factory, configuration database, phasing, RAL, sequencer-driver handshake), and works through the UBUS case study end-to-end. The patterns and mechanisms introduced let engineers read, extend, and debug existing UVM environments with confidence.

• • Chapter 6: Emergent Verification with Actors
  Develops actor-based verification end-to-end. Establishes the hardware-to-actor isomorphism that motivates the model, builds the actor framework as a small core (the Actor base class, the MsgBase envelope, ‘WIRE-based typed topology) plus ten parallel extension packages: supervision, routing, patterns, lifecycle, observability, verification, persistence, distributed transports, RAL, and test-kit. Shows how the resulting substrate supports dynamic, agile testbenches that adapt to evolving verification goals without rebuilding infrastructure, and closes by introducing the UVM-to-actors rewrite of the canonical UBUS example; the rewrite itself is walked end-to-end in Appendix A.

• • Chapter 7: Emulation
  Closes the three-leg pipeline by putting the actor substrate on hardware emulators. Walks the industrial-emulator taxonomy (custom-processor-array and FPGA-array emulators vs. the distributed-clock FPGA prototyper), the hybrid-emulation pattern that dominates 2024–2026 AI-accelerator flows, Amdahl’s law on the heterogeneous host+emulator machine and why a synthesizable-actor testbench escapes the trap that holds UVM-style flows at host throughput, gate-level emulation, the checkpoint-and-replay operational unlock, functional safety / fault-injection campaigns, and how a synthesizable-actor testbench converts from simulation onto a commercial emulator — or onto an open FPGA-accelerated simulator — automatically, with no manual port, for the whole verification environment and not the design alone. The book’s closing argument: the verification investment compounds across formal, simulation, and emulation when the model of computation is picked once and right.

• • Appendix A: From UVM to Actors — The UBUS Example
  A step-by-step walkthrough of the UBUS-as-actors rewrite that closes Chapter 6: data contracts, master/slave actors, observability, topology wiring, and the line-count comparison against the legacy UVM environment.

• • Appendix B: Mini-SoC Integration Case Study
  Builds a complete Mini-SoC testbench with two masters (CPU and DMA), a Timer, a Register Abstraction Layer, and an APB protocol bridge — entirely as actors. Demonstrates how the framework scales from a single IP to system-level integration.

• • Appendix C: Verifying Earl Grey as Actors
  Industrial-scale empirical close. Models all twenty-eight OpenTitan Earl Grey IP types as actors, including the always-on power island (pwrmgr, clkmgr, rstmgr, lc_ctrl), security-critical FSMs (alert handler with four parallel escalation classes, key manager), the entropy chain (entropy_src, csrng, edn0/edn1), the crypto IPs (AES, KMAC, HMAC, OTBN), the serial-bus and peripheral IPs (UART, I2C, SPI host/device, USB device, GPIO, pinmux, PWM, ADC controller), and the Ibex CPU with its lockstep pair, PLIC, and comparator.

  A seven-phase chip-level test exercises boot flow, peripheral traffic, symbolic-name CSR access through the framework’s RAL, crypto and entropy, OTBN program execution, lockstep glitch fault injection, and watchdog bite end-to-end, with the chip scoreboard observing cross-IP causality (alert\(\rightarrow \)reset, bite\(\rightarrow \)reset) from passive subscriptions. Includes a head-to-head line-count comparison against the OpenTitan UVM environment (\(\sim \)205 K UVM vs. \(\sim \)11 K actor framework for the same scope).

• • Appendix D: From Spec to Silicon — One Model, Many Languages
  The methodology contribution beyond verification. Lays out a seven-step continuum that the actor model spans: specification as executable actor code; architecture exploration with measurable performance/power claims; verification at both architectural and RTL phases (same TB topology either way); synthesis through the synthesizable form; FPGA emulation; AI-driven design; and verification by construction. Discusses host-language choices — SystemVerilog, C++, SystemC — with the explicit observation that the methodology is host-language-agnostic and SystemC is in some respects the stronger host for hardware-facing deployments.

• • Appendix E: The Synthesizable Form of the Actor Framework
  Defines five rules that constrain the framework to synthesizable RTL (no dynamic allocation, no virtual dispatch in hot path, bounded mailboxes, fixed fan-out, ready/valid handshake). Worked example: a counter actor synthesized through Yosys to 98 standard cells, its two-stage composition then placed and routed on a Lattice iCE40 HX8K target meeting timing at 126.6 MHz with 0.6% device utilization. A second worked example synthesizes an entire verification loop — stimulus, DUT, scoreboard with its golden model, and coverage — to gates, showing the verification environment itself is hardware, not only the design. Real silicon-quality numbers from the actor methodology.

• • Appendix F: Synthesizing Constrained-Random Stimulus
  Closes the synthesizability argument on the one construct the others leave stranded on the host: constrained-random stimulus. Establishes that randomize() exercises only the model-finding half of a constraint solver — it finds a witness, never refutes — so the legal set can be structured at compile time into a synthesizable sampler that needs no run-time solver. Works the riscv-dv constraint corpus end-to-end: every constraint shape compiled to hardware and validated both directions against the reference solver, a clause-learning SAT engine rendered onto the fabric for the hardest tier, and a Lean-certified sampler that is smaller and faster than the hand-written allocator. The stimulus generator rides the emulator beside the scoreboard and coverage instead of bottlenecking on the host.

• • Appendix G: FPGA Emulation — Automatic Conversion of the Actor Testbench to Hardware
  The engineering reference behind Chapter 7’s claim. The whole actor graph — design and verification alike — synthesizes and runs on the fabric; only genuine software-to-hardware seams (the workload read-out, external I/O) stay on the host, attached via the existing distributed-transport bridges. Verification artifacts (scoreboards, coverage, RAL, regression infrastructure) carry forward without rewrite, re-rendered onto the fabric. One authored graph compiles to three back-ends — open-source FPGA (Yosys \(\rightarrow \) nextpnr \(\rightarrow \) icepack/ecppack), a commercial emulator across a generated SCE-MI transactor, and FireSim across a generated FAME bridge — with the conversion provable on a laptop in FireSim metasimulation. Full-SoC bring-up is flagged as bounded follow-on work.

• • Appendix H: AI-Driven RTL Generation from Actor Specifications
  Conceptual treatment with a hand-translated worked example. Argues that AI-RTL tools today fight the wrong battle (English-to-Verilog crosses an enormous structural gap). With actor-code input, the translation becomes shape-preserving: structured concurrent code into structured concurrent RTL. Worked example uses the class/synth pair from Appendix E. Discusses prompt structure and the broader implications for AI as a collaborator at every step of the methodology continuum.

• • Appendix I: Actor-Based Hardware Simulation — a Working Prototype
  A header-only C++17 prototype simulator written natively against the actor model rather than the event-queue paradigm Verilator and VCS inherit from Verilog-XL (\(\sim \)568 lines for the simulator core, \(\sim \)165 lines for VCD output). Tests seven canonical RTL patterns — mux, D flip-flop, counter, shift register, ALU, Moore-style round-robin arbiter FSM, FIFO with full/empty flags — through 84 self-checks, all passing; the FIFO test additionally writes a standard VCD that opens in GTKWave. Not yet a Verilator replacement (users write designs as C++ actor classes rather than SystemVerilog), but a proof that the actor model captures the semantics of real RTL — two-phase NBA updates, combinational propagation to fixpoint, multi-stage flip-flop chains, FSMs with combinational decoders, stateful FIFOs with synchronous control flags. The path from here to an SV front-end is engineering, not research.

• • Appendix J: The SystemC Port — One Model, Two Languages
  Working header-only C++/SystemC implementation of the actor framework, parallel to the SystemVerilog implementation. Demonstrates the host-language-agnostic claim with a hello-world example and a port of the supervision package (Erlang-style Supervisor, DeathWatcher, LinkRegistry). Spells out the mapping from SV constructs to SystemC equivalents and the advantages SystemC brings for synthesis and host integration.

• • Appendix K: Pure C++ Actors for General Concurrent Software
  The general-software deployment of the methodology, parallel to Appendix J’s hardware-facing port. Two header-only tiers: a basic std::thread-per-actor implementation, and a C++20 coroutine tier with M:N green-thread scheduling that delivers Erlang/Go-class ergonomics in native C++. Comparisons with CAF, thread pools with shared queues, async/await, and OOP component hierarchies. Argues that actors composed with Data-Oriented Design are the natural shape for the vast majority of concurrent software systems.

• • Appendix L: Distributed Regression — Many Hosts, Many Languages, One Topology
  Working three-process polyglot demonstration: SystemC publisher, SystemC subscriber, and a Python subscriber consume the same actor messages over ZMQ. Same ‘WIRE-based typed topology, no DPI, no language bridges — the cross-process and cross-language scaling falls out of the framework’s transport-bridge pattern.

• • Appendix M: AI Hardware Systems with Actors — GPUs, Accelerators, and Distributed Compute
  Extends the methodology continuum upward to modern AI compute. Maps GPU programming primitives (kernel launches, CUDA streams, NCCL collectives, RDMA, MPI) onto actor concepts; establishes the neuron–actor isomorphism; expresses neural networks as actor topologies, with the backward pass falling out of the framework’s lineage infrastructure. Catalogues framework primitives that ML systems re-implement under different names. Shows how the four standard parallelism strategies of distributed training — data, pipeline, tensor, expert — become four ‘WIRE topologies over the same primitives. Treats inference serving (vLLM, TensorRT-LLM, Triton) as an actor topology with backpressure; extends to robotic and embodied AI hardware systems. Closes with the unifying claim that the actor model is the structural model of concurrent hardware systems at every scale.

How to Read This Book

The chapters build on each other, but several entry points are valid depending on your background and goals:

• • Verification engineer new to UVM: Read straight through. Chapter 4 builds the SystemVerilog OOP foundation, Chapter 5 develops UVM on top of it, and Chapter 6 then offers the actor-based alternative.

• • Experienced UVM engineer: Skim Chapter 4, read Chapter 5’s “What UVM gets right” section to calibrate, then proceed to Chapter 6 and the appendices for the actor framework. The UBUS rewrite at the end of Chapter 6 is the empirical close.

• • RTL designer: Chapter 2 is the immediate target. The actor model in Chapter 6 will feel familiar because hardware modules are actors — the chapter’s hardware-actor isomorphism makes that connection explicit.

• • Student or researcher: Chapter 1 establishes the verification-methodology landscape; Chapter 6 develops actor-based verification as the contribution; Appendix M extends the methodology to AI hardware systems; the appendices provide complete, runnable case studies.

Regardless of entry point, Chapter 7 (Emulation) is worth reaching: it is where the actor testbench — design and verification actors alike — re-renders onto the hardware fabric with no rewrite, the payoff the single-model choice builds toward.

Acknowledgments

The one who plays every role at once — friend, teacher, beloved, and Godhead — is the beautiful Krishna, who taught the Bhagavad Gita to Arjuna on the battlefield of Kurukshetra five thousand years ago. His teachings keep me going; helped by the one, I cross this ocean of happiness and distress. This work is offered to Him.

“Perform your duty equipoised, O Arjuna, abandoning all attachment to success or failure. Such equanimity is called yoga.”

— Bhagavad Gita 2.48

My gratitude also goes to Sankat Mochan Hanuman Ji, the beautiful deity of courage who resides on Mount Madonna; and to Ganesh Ji, the deity of intellect and wisdom and scribe of the Mahabharata, who I feel came in the avatar of AI in this yuga and helped me with the proofreading of this book.

I would like to express my deepest gratitude to all my mentors throughout my life who have taught me the intricacies of hardware design and verification, as well as to all my colleagues across the multiple companies I have had the privilege to work with. Thank you to my family for your unwavering support. A very special thanks to Hrishikesha and Anukta, who happen to be my children in this life and, as I so often realize, expressions of God. They beautifully drew the cover image to reflect the emergent systems around us — specifically capturing the resilient baya weaver nest that protects its family from predators, and the succulent plant that thrives even with scarce water. Finally, my thanks to everyone who reviewed the manuscript and contributed many valuable changes to it. I am especially grateful to Mohamed Ghonim for his thorough review of Chapters 2 and 3 and for our many discussions; to Suman Kasam for his review of Chapter 6; to Thomas Nemeh for his discussions on Chapter 2; and to Santosh Mundhe for his review of the constraint-solver examples.

Conventions and Terminology

A handful of terms appear early and reappear throughout the book. This sidebar gives the working definitions; later chapters develop each in detail.

• • SoC — System-on-Chip: an integrated circuit that combines processors, memory, interconnect, and peripherals on a single die. The unit of design and verification this book targets.

• • RTL — Register-Transfer Level. Hardware modeled as registers and the combinational logic that updates them on each clock edge. (Chapter 2.)

• • MoC — Model of Computation. The abstract framework that defines how computation and communication happen in a system. The book’s argument hinges on picking a MoC that matches hardware’s structural shape. (Chapter 1.)

• • SVA — SystemVerilog Assertions. Temporal-logic properties that hold over RTL signals; used to formally check sequencing and concurrency invariants. (Chapter 2.)

• • FSM — Finite State Machine: a finite set of states with transitions driven by inputs. Foundational tier of the MoC ladder; ubiquitous in RTL. (Chapter 2.)

• • FIFO — First-In, First-Out queue. The canonical hardware buffer for crossing clock domains and absorbing burst traffic. (Chapter 2.)

• • DUT — Design Under Test: the RTL or netlist that the testbench is verifying. Used throughout this book.

• • TLM — Transaction-Level Modeling. Verification at the level of whole transactions (a burst, a packet, a register access) instead of pin-level signal events. (Chapter 4.)

• • Transaction — one logical unit of communication between components, e.g. a single bus burst or memory access. Carries enough data to model an effect on the system without tracking individual cycles. (Chapter 4.)

• • BFM — Bus Functional Model: a verification component that translates abstract transactions into cycle-accurate pin-level activity on a bus interface, and vice versa. Sits between the testbench’s transaction-level world and the DUT’s signal-level world. (Chapter 5.)

• • Agent — a verification component that drives and monitors one logical interface (driver + sequencer + monitor + configuration), typically reusable across testbenches. (Chapter 5.)

• • Monitor — a passive observer that converts pin activity on an interface into transactions for downstream analysis. (Chapter 5.)

• • Scoreboard — a checker that compares the DUT’s observed responses against the expected reference values. The pass/fail oracle for the test. (Chapter 5.)

• • VIP — Verification IP: a packaged, reusable verification component for a specific protocol (AXI, PCIe, USB, etc.). (Chapter 5.)

• • UVM — Universal Verification Methodology, IEEE Std 1800.2. The SystemVerilog-based, IEEE-standardized framework for Coverage-Driven Verification. (Chapter 5.)

• • RAL — Register Abstraction Layer. UVM’s modeling layer for the DUT’s control/status register space; lets tests access registers symbolically (regmodel.STATUS.read) instead of by raw address. (Chapter 5.)

• • CDV — Coverage-Driven Verification. The industry-standard methodology of constrained-random stimulus plus functional coverage as the verification-completion metric. (§1.5 of Chapter 1.)

• • EV — Emergent Verification. The alternative this book proposes: verification architecture grows incrementally with the design rather than being decided up front. (§1.6 of Chapter 1 and Chapter 6.)

Actor-Framework Quick Reference

The actor-framework vocabulary builds up across Chapter 6 and the appendices faster than the general-purpose terminology above. This sidebar collects the recurring names in one place; each entry points at the chapter or appendix that defines it.

• • Actor — the framework’s encapsulated unit of state, mailbox, and act() handler. Virtual base class in actor_pkg/actor_pkg.sv; every concrete actor subclasses it. (Chapter 6.)

• • MsgBase — the universal message envelope: trace_id, parent_span, timestamp_ns, sender_id. Every typed payload is wrapped in an Msg#(T) that extends MsgBase. (Chapter 6.)

• • Msg#(T) — parameterized typed-payload wrapper. T is the user-defined struct; the wrapper carries the lineage fields plus the payload. (Chapter 6.)

• • mbox — an actor’s inbound mailbox; bounded if the actor was constructed with capacity > 0, unbounded if 0. Producers call publish() which lands here. (Chapter 6.)

• • ‘WIRE(producer, MsgT, consumer) — the framework’s only wiring primitive. Declares that the consumer receives every message of type MsgT that the producer publishes. Resolved at elaboration; no dynamic subscription, no listen(), no ‘TAP. (Chapter 6.)

• • ‘PUBLISH(data) — fire-and-forget emission. Wraps the typed payload in a Msg envelope, looks up the payload type’s subscribers in the producer’s table, and try_puts into each consumer’s mailbox; backed-up subscribers drop, producer never stalls. (Chapter 6.)

• • ‘PUBLISH_TO(actor, data) — directed emission to one specific actor instance, bypassing the type-keyed fan-out. Used when a producer holds an explicit handle to its target (e.g. a bridge forwarding to its APB-side sink). (Chapter 6.)

• • ‘PUBLISH_TRACED(data, parent_msg) — like ‘PUBLISH, but propagates the trace_id and records the upstream message as the parent span so causal lineage survives the fan-out. (Chapter 6.)

• • try_publish(msg) — backpressure-aware variant; returns 1 only when all wired consumers accepted. Caller can react to a full mailbox. (Chapter 6.)

• • act(MsgBase msg) — the per-message handler each actor implements. The framework’s run() task reads from mbox and dispatches each message to act(). (Chapter 6.)

• • on_terminate() — cleanup hook called by stop() after the run process is killed. File-handle owners (StructuredLogActor, RecorderActor) close their fd here. (Chapter 6.)

• • TransportBridgeActor — abstract base for distributed transports (ZMQ, NATS, iceoryx, libfabric). Subclasses serialize outbound messages to bytes and deserialize inbound bytes back to typed messages. (Chapter 6 §actor_distributed_pkg; Appendix L demonstrates.)

• • FpgaProxyActor — the \(\sim \)50-line bridge actor at a software-to-hardware seam (the host read-out, external I/O, or a link whose far side is software). The verification actors themselves synthesize onto the fabric; this bridge carries only what genuinely crosses the seam. (Appendix G specifies; Chapter 7 walks the methodology.)

• • SpecActor — a runtime-executable specification compiled from TLA+, Alloy, or Cryptol; produces an expected output stream the DiffActor compares against the DUT’s actual output stream. (Chapter 6 §actor_verification_pkg.)

• • ScoreboardActor / CoverageActor / RalActor — the verification-package primitives a per-IP testbench typically wires (a scoreboard subscribes to DUT outputs and checks against a reference; a coverage actor records typed bins; a RAL actor brokers symbolic-name register access). (Chapter 6.)

• • Five Rules — the synthesizable-form rules from Appendix E: (1) no dynamic allocation, (2) no virtual dispatch in the hot path, (3) bounded mailboxes only, (4) fixed-cardinality fan-out, (5) ready/valid handshake on every channel. An actor that obeys these synthesizes to RTL through Yosys or vendor synthesis. (Appendix E.)

Companion Code

The worked examples in this book are real, runnable code, carried in the book’s repository alongside the text; every line count and synthesis result cited in these pages can be reproduced by building and running it. The chapters and appendices with runnable companions build from their own directories:

• • Chapter 2 — ch2_rtl_fv_examples/: the seven RTL designs — the introductory soda-machine FSM plus the six that each earn a formal abstraction — each in its own subdirectory paired with the SVA contract that verifies it, and each proved exactly as printed by the Chapter 3 engines (make prove).

• • Chapter 3 — ch3_fv_examples/: the from-scratch proof engines of 01_proof_engines/ (CDCL, BMC, \(k\)-induction, IC3/PDR, interpolation, and an SMT / DPLL(T) solver), the elevator and FIFO designs they prove (02_elevator_proof/, 03_fifo_proof/), an SMT adder-equivalence miter (04_adder_equiv_smt_proof/), and the Lean-checked Booth multiplier (05_booth_lean_proof/).

• • Chapter 6 — actor_pkg/: the SystemVerilog actor framework — a small core plus ten extension packages — with runnable demonstrations under ch6_actor_examples/.

• • Appendix A — appA_actor_ubus/: the UVM-to-actors rewrite of the UBUS example.

• • Appendix B — appB_mini_soc/: the mini-SoC integration.

• • Appendix C — appC_earlgrey/: the twenty-eight-IP OpenTitan Earl Grey model, with its register-layer generator.

• • Appendix E — appE_synth/: the synthesizable form, a counter actor placed and routed to iCE40 silicon.

• • Appendix F — appF_synthesize_constraints/: the constrained-random samplers, from the constraint compiler through the riscv-dv capstone.

• • Appendix G — appG_firesim_substrate_swap/: the substrate-swap example, where simulation and fabric run the same graph.

• • Appendix I — appI_actor_sim/: the self-contained actor-based hardware simulator.

• • Appendices J and K — actor_pkg_systemc/ and actor_pkg_cpp/: the SystemC and pure-C++ ports of the framework.

• • Appendix L — appL_distributed_regression/: the distributed-regression demonstration across processes and languages.