# Open Verifier

> Automated VLSI verification assistant. Runs syntax checks, generates testbenches, executes simulations, and produces verification reports for Verilog/SystemVerilog designs. Trigger whenever a user asks to verify, test, simulate, or debug a Verilog/SystemVerilog DUT.

- **Type:** Skill
- **Install:** `agentstack add skill-aryaman9999-open-verifier-open-verifier`
- **Verified:** Yes — security-reviewed for prompt injection and unsafe behavior
- **Seller:** [Aryaman9999](https://agentstack.voostack.com/s/aryaman9999)
- **Installs:** 0
- **Category:** [Agent Skills](https://agentstack.voostack.com/c/agent-skills)
- **Latest version:** 0.1.0
- **License:** MIT
- **Upstream author:** [Aryaman9999](https://github.com/Aryaman9999)
- **Source:** https://github.com/Aryaman9999/open-verifier/tree/master/.agents/skills/open-verifier

## Install

```sh
agentstack add skill-aryaman9999-open-verifier-open-verifier
```

Requires the [AgentStack CLI](https://agentstack.voostack.com/docs/cli). Works with Claude Code, Cursor, and any MCP-compatible agent.

## About

# 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
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
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
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
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
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.

```python
# 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:

```python
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
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
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

**fetch_adjacent_pages — when a diagram spans a page boundary:**

```bash
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.
```

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

---

## STEP 6 — VALIDATE_TOP_WRAPPER

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

```bash
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
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:

```bash
# 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:

```verilog
`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 — GEN_SEQ_ITEM (`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.

```python
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`)

```python
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

```python
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`)

```python
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.

## Pricing

- **Free** — Free

## Security capabilities

Automated source analysis of v0.1.0 — what this tool can access:

- **Network access:** no
- **Filesystem access:** yes
- **Shell / process execution:** no
- **Environment & secrets:** yes
- **Dynamic code execution:** no

*"Yes" means the capability is present in the source — more access means more to trust, not that it is unsafe.*


## Versions

- **0.1.0** — security scan: passed — Imported from the upstream source.

## Links

- Listing page: https://agentstack.voostack.com/l/skill-aryaman9999-open-verifier-open-verifier
- Seller: https://agentstack.voostack.com/s/aryaman9999
- Browse the marketplace: https://agentstack.voostack.com/browse

---
Listed on AgentStack — the marketplace for AI agent skills and MCP servers. Every listing is security-reviewed. Creators keep 70%.