Open Verifier

SKILL: Open Verifier v2 — Implementation Agent

---

PRIME DIRECTIVE

You are implementing a hardware verification system, one file at a time. You are NOT allowed to:

• Read any file in src/ for any reason
• Generate more than one deliverable file per turn
• Proceed to the next step without running the validator first
• Invent your own API patterns — use only the exact patterns in this file
• Use any SystemVerilog UVM syntax in Python files

Your only sources of truth are:

1. out/state.json — tells you exactly where you are
2. out/interface.yaml — tells you DUT port names and module name
3. out/protocol_rules.yaml — tells you all rules, coverage directives, formal properties
4. out/binding_map.yaml — tells you spec→DUT signal name mappings (re-read before EVERY Python file)
5. This SKILL.md — tells you every pattern to follow

Before every single action, read out/state.json and identify the first step that is pending or stale. Work on only that step. Nothing else.

Windows/WSL environments: If tools (verilator, iverilog, cocotb-config) are installed in WSL but the project lives on a Windows filesystem, wrap ALL python3 and script invocations as bash -l -c "python3 ...". The -l login flag sources ~/.bashrc and puts WSL tools on PATH. A non-login shell silently cannot find them, producing "command not found" errors even for correctly installed tools.

---

STEP 0 — READ STATE FIRST

bash -l -c "cat out/state.json" 2>/dev/null || echo "state.json missing — run 00_check_env.sh first"

Find the first pending step. That is your only task for this turn.

---

HOW TO UPDATE STATE — USE THIS EVERY TIME

After completing any step, update state.json using the CLI script. This is the ONLY sanctioned method:

bash -l -c "python3 .agents/skills/open-verifier/scripts/update_state.py  --status complete"

Optional flags: --artifact and --hash for steps that produce primary artifacts.

Examples:

bash -l -c "python3 .agents/skills/open-verifier/scripts/update_state.py env_check --status complete"
bash -l -c "python3 .agents/skills/open-verifier/scripts/update_state.py gen_filelist --status complete --artifact out/dut.f"
bash -l -c "python3 .agents/skills/open-verifier/scripts/update_state.py gen_formal_props --status skipped"

DO NOT write to out/state.json directly via write_to_file or python3 -c. Inline Python one-liners break due to Windows↔bash↔Python triple-quoting. The script handles all edge cases (missing file, malformed JSON, missing out/ directory).

---

STEP 1 — ENV_CHECK

bash -l -c "bash .agents/skills/open-verifier/scripts/00_check_env.sh"

00_check_env.sh must mkdir -p out/ as its very first action — before writing out/.formal_available or reading out/state.json. On a fresh checkout out/ does not exist; any write to it fails. Directory creation belongs here, not in a later step.

On pass: update state.json env_check → complete. On fail: stop, show missing tool, do not proceed.

---

STEP 2 — GEN_FILELIST

bash -l -c "python3 .agents/skills/open-verifier/scripts/01_gen_filelist.py"

Script must recursively find all .v and .sv files under src/ and write to out/dut.f.

CRITICAL — path format: Write project-root-relative paths (e.g. src/dummy_alu.v), NOT absolute paths. Absolute paths on Windows/WSL contain the user's home directory (/mnt/c/Users/DELL DN/...). The space in DELL DN causes GNU Make to split the path into two tokens, breaking VERILOG_SOURCES with "No rule to make target" errors. Relative paths from the project root never traverse the user directory and are safe.

# Write relative path from project root — forward slashes only
rel = path.relative_to(project_root)
path_str = str(rel).replace("\\", "/")   # e.g. "src/dummy_alu.v"

CRITICAL — state.json defensive initialization: Every script that calls update_state() must handle a missing or malformed state.json. Before writing, check that the file exists and contains a valid steps dict. If not, create the skeleton:

import json, pathlib

STATE_PATH = pathlib.Path("out/state.json")

def load_state():
    if STATE_PATH.exists():
        try:
            data = json.loads(STATE_PATH.read_text())
            if "steps" in data:
                return data
        except json.JSONDecodeError:
            pass
    # Create skeleton if missing or malformed
    return {"schema_version": "1.0", "steps": {}}

def update_state(step_name, status="complete", **kwargs):
    state = load_state()
    state["steps"][step_name] = {"status": status, **kwargs}
    STATE_PATH.write_text(json.dumps(state, indent=2))

Without this, state["steps"][step_name] raises KeyError: 'steps' on a fresh checkout.

---

STEP 3 — ELABORATE

bash -l -c "python3 .agents/skills/open-verifier/scripts/02_elaborate.py"

Runs verilator -f out/dut.f --xml-only --top-module -o out/verilator_ast.xml, then prunes to top-level ports only → out/interface.yaml.

CRITICAL — bus width extraction: Do NOT read width from the VAR node directly. Multi-bit ports store their type via a dtype_id attribute that references the typetable section of the XML. The script must:

1. Parse the ` section first, building a dtype_id → width` map
2. For each top-level port VAR, resolve dtype_id through that map
3. Write the resolved width into interface.yaml

Skipping this step causes all multi-bit buses to appear as 1-bit wires, silently corrupting all downstream testbench signal widths.

---

STEP 4 — EXTRACT_SPEC

bash -l -c "python3 .agents/skills/open-verifier/scripts/03_extract_spec.py --list-chapters"

Two modes:

• --list-chapters: prints chapter list from PDF bookmarks
• --chapter N: returns text of chapter N

fetchadjacentpages — when a diagram spans a page boundary:

bash -l -c "python3 .agents/skills/open-verifier/scripts/03a_fetch_adjacent_pages.py \
  --pdf spec.pdf --current_page  --direction next --count 2 --out_dir out/spec_pages"

Read .txt and .png from out/spec_pages/. Clean after each chapter: rm -rf out/spec_pages/*.

Process each chapter relevant to protocol rules. Every rule in out/protocol_rules.yaml must have: id, description, type, signals, coverage, formal_property (or null). Add formal_bmc_depth: 50 at the top level.

---

STEP 5 — CRITICAL PAUSE: BINDING_REVIEW

1. Read out/interface.yaml and out/protocol_rules.yaml
2. Generate a proposed out/binding_map.yaml
3. HALT. Output exactly:

CRITICAL PAUSE — Human review required.

I have proposed signal bindings in out/binding_map.yaml.
Please review this file and:
  1. Correct any wrong signal mappings
  2. Verify the suspected clock/reset ports
  3. Save the file

When you are satisfied, tell me: "binding map approved"

Do NOT proceed until you receive this confirmation.

1. Wait. Do not generate any code. Do not run any scripts. Do not continue.

---

STEP 6 — VALIDATETOPWRAPPER

Ask the user for the path to their top-level wrapper SV file, then:

bash -l -c "python3 .agents/skills/open-verifier/scripts/05_check_top_wrapper.py "

Show diff on mismatch. Do not proceed until it passes.

---

STEP 6b — FORMAL GUARD PRE-CHECK

Run this immediately after the top wrapper validates and before generating any testbench file. Doing it here means simulation produces a VCD and formal elaboration is clean — both in the same run with no re-runs needed.

bash -l -c "python3 .agents/skills/open-verifier/scripts/06b_formal_guard_check.py"

Prefer the Python script above. It handles escaping correctly and outputs structured JSON. The grep fallback below is fragile across PowerShell→bash→grep escaping layers:

# Fallback — may need manual escaping adjustments on Windows/WSL
bash -l -c "grep -rn '\$display\|\$finish\|\$test\$plusargs\|\$dumpfile\|\$dumpvars\|\$readmemh' src/"

Two things must be present in the DUT source before proceeding:

Check 1 — VCD dump block. The DUT needs an initial block for waveform output. Without it, simulation completes but out/waves.vcd is empty, toggle coverage is skipped, and waveform debugging is impossible:

`ifndef FORMAL
initial begin
    if ($test$plusargs("vcd")) begin
        $dumpfile("waves.vcd");
        $dumpvars(0, );
    end
end
`endif

Check 2 — All simulation system tasks are guarded. Any $display, $finish, $readmemh, $test$plusargs outside a ` ifndef FORMAL ` block will cause Yosys to abort with ERROR: Found simulation-only construct` at STEP 18. Find them now and guard them before generating a single testbench file.

If either check fails: Output the exact lines that need guarding. Tell the user to add the guards. Wait for confirmation. Do NOT proceed to STEP 7 until the user confirms the DUT has been updated. Do NOT edit src/ yourself — it is read-only to the agent.

If both checks pass: Mark formal_guard_check complete in state.json and proceed to STEP 7.

---

STEPS 7–14 — TESTBENCH GENERATION

The law:

1. Re-read out/binding_map.yaml before writing any Python file — every time
2. Write one file
3. Run bash -l -c "python3 .agents/skills/open-verifier/scripts/04_validate_step.py "
4. On fail: fix specific error, retry, max 3 attempts, then halt TOPOLOGY
5. Update state.json → complete
6. Stop. Report. Wait for confirmation.

NAMING CONVENTION

Derive ProtocolName from protocol_id in protocol_rules.yaml at generation time. Convert snake_case to PascalCase: axi4_lite → Axi4Lite, i2c_master → I2cMaster, spi → Spi. Never hardcode a protocol name — always derive it fresh from the YAML.

| File | Class name pattern | | --------------- | ------------------------------------------------------------------ | | seq_item.py | {ProtocolName}SeqItem | | sequences.py | {ProtocolName}BaseSequence, {ProtocolName}Rule001Sequence, ... | | driver.py | {ProtocolName}Driver | | monitor.py | {ProtocolName}Monitor | | scoreboard.py | {ProtocolName}Scoreboard | | env.py | {ProtocolName}Env | | test.py | {ProtocolName}BaseTest |

All imports are bare: from seq_item import {ProtocolName}SeqItem. No __init__.py. Not a package.

---

STEP 7 — GENSEQITEM (uvm_tb/seq_item.py)

Before writing: read protocol_rules.yaml to get protocol_id → derive {ProtocolName}. Read binding_map.yaml to get every signal name — one field per signal.

import random
import os
from pyuvm import *

class ConstraintFailure(Exception):
    pass

SEED = int(os.environ.get("COCOTB_RANDOM_SEED", 0))
random.seed(SEED)

@uvm_object_utils
class {ProtocolName}SeqItem(uvm_sequence_item):
    def __init__(self, name="{ProtocolName}SeqItem"):
        super().__init__(name)
        # ONE field per signal in binding_map.yaml — derived at generation time
        # Default all fields to 0. Use spec signal names as field names (not DUT port names).
        # Example for a 3-signal protocol: self.valid=0, self.data=0, self.addr=0
        # DO NOT hardcode AXI or any other protocol signal names here

    def randomize(self):
        # Generate one if/continue guard per constraint_guard in protocol_rules.yaml
        # Rejection sampling — try up to 1000 combinations
        for _ in range(1000):
            # Randomize each field using its valid_range from protocol_rules.yaml
            # Example: self.burst = random.choice(valid_range)
            # Example guard: if self.burst == WRAP and self.len not in [1,3,7,15]: continue
            return True
        raise ConstraintFailure(f"{self.__class__.__name__}: unsatisfiable after 1000 attempts")

---

STEP 8 — GEN_SEQUENCES (uvm_tb/sequences.py)

from pyuvm import *
from seq_item import {ProtocolName}SeqItem   # substitute derived name

@uvm_object_utils
class {ProtocolName}BaseSequence(uvm_sequence):
    async def body(self):
        for _ in range(self.num_items):
            item = {ProtocolName}SeqItem("item")
            await self.start_item(item)
            item.randomize()
            await self.finish_item(item)

# Generate one subclass per rule of type 'handshake' or 'constraint' in protocol_rules.yaml
# Each subclass overrides body() to exercise that specific rule scenario

---

STEP 9 — GEN_DRIVER (uvm_tb/driver.py)

Before writing: read binding_map.yaml to identify:

• All input signal names (to drive to 0 before reset)
• The clock port name
• The reset port name and active level (active_level: low → assert=0, release=1)
• The valid signal(s) and corresponding ready signal(s) for handshake

import cocotb
from cocotb.triggers import RisingEdge, ReadOnly
from pyuvm import *
from seq_item import {ProtocolName}SeqItem

@uvm_component_utils
class {ProtocolName}Driver(uvm_driver):
    def __init__(self, name, parent):
        super().__init__(name, parent)

    def build_phase(self):
        super().build_phase()
        self.dut = cocotb.top

    async def run_phase(self):
        # NO raise_objection — driver runs until test drops its objection

        # Drive ALL input signals to 0 before reset
        # Substitute real port names from binding_map.yaml
        self.dut..value = 0
        self.dut..value = 0
        # ... every input signal from binding_map.yaml

        # Wait for reset release
        # Substitute clock and reset port names from binding_map.yaml
        # active_level: low → wait while reset == 0; active_level: high → wait while reset == 1
        await RisingEdge(self.dut.)
        while self.dut..value == :
            await RisingEdge(self.dut.)

        while True:
            req = await self.seq_item_port.get_next_item()
            await self._drive(req)
            self.seq_item_port.item_done()
        # NO drop_objection

    async def _drive(self, item):
        # Step 1: Assert VALID and drive all data signals
        # Substitute signal names from binding_map.yaml
        self.dut..value = 1
        self.dut..value  = item.
        # ... all other signals

        # Step 2: Hold VALID until READY — REQUIRED for any valid/ready protocol
        # Once VALID is asserted it MUST NOT be deasserted until READY is seen
        # Deasserting VALID early is a protocol violation — fix here, never in DUT
        await ReadOnly()
        while not self.dut..value:
            await RisingEdge(self.dut.)
            await ReadOnly()

        # Step 3: Deassert after handshake completes
        await RisingEdge(self.dut.)
        self.dut..value = 0

---

STEP 10 — GEN_MONITOR (uvm_tb/monitor.py)

import cocotb
from cocotb.triggers import RisingEdge, ReadOnly
from pyuvm import *
from cocotb_coverage.coverage import CoverPoint, CoverCross
from seq_item import {ProtocolName}SeqItem

@uvm_component_utils
class {ProtocolName}Monitor(uvm_monitor):
    def build_phase(self):
        super().build_phase()
        self.ap  = uvm_analysis_port("ap", self)
        self.dut = cocotb.top

    async def run_phase(self):
        # NO raise_objection — monitor runs until test drops its objection
        while True:
            await RisingEdge(self.dut.)    # substitute clock name from binding_map.yaml
            await ReadOnly()                      # REQUIRED — wait for delta cycles to resolve
            # Substitute valid/ready signal names from binding_map.yaml
            if self.dut..value and self.dut..value:
                await self._sample()
            # Do NOT add

…

## Source & license

This open-source skill is cataloged on AgentStack and links to its original source — we do not rehost the code.

- **Author:** [Aryaman9999](https://github.com/Aryaman9999)
- **Source:** [Aryaman9999/open-verifier](https://github.com/Aryaman9999/open-verifier)
- **License:** MIT

Install and usage instructions live in the source repository linked above.