VLSI Formal Verification MCP Server

A domain-specific Model Context Protocol (MCP) server that empowers LLMs (such as Claude, Gemini, or ChatGPT) to interact directly with hardware designs (Verilog/SystemVerilog), formal verification tools, waveform logs, protocol specifications, regressions, and historical bug repositories.

This server abstracts complex EDA (Electronic Design Automation) workflows into 34 structured, reusable tools so engineers can inspect hardware designs, analyze failures, generate assertions, and query protocol rules using natural language.

🏗️ Architecture Overview

                 +----------------------+
                 |      LLM Client      |
                 | (e.g. Claude Desktop)|
                 +----------+-----------+
                            |
                       MCP Protocol
                            |
                 +----------+-----------+
                 |  Formal Verification |
                 |      MCP Server      |
                 +----------+-----------+
                            |
   +------------------------+-------------------------+
   |          |             |             |           |
RTL Parser  Waveform      Specs RAG   Bug database  Git CLI
 (Verilog)   Parser       (SQLite DB)  (SQLite DB)  Wrapper

The server is built with:

• FastMCP (Python): Main host application.

• Pure Python RTL Parser: Lightweight regex-based AST compiler mapping ports, parameters, internal registers, submodules, and FSM controllers.

• Waveform Timeline Parser: Decodes VCD value changes and reconstructs signal values over simulation time.

• Semantic Databases: SQLite databases using local-embedding/Gemini-embedding vectors to query protocol specs and historical bugs.

• EDA Solver Connectors: Subprocess command wrappers for Cadence JasperGold, Synopsys VC Formal, and Siemens Questa Formal, featuring simulated execution fallbacks if the tools are unlicensed or offline.

Related MCP server: Verilator MCP Server

🛠️ Feature Areas & Key Tools

The server registers 34 distinct tools across 9 primary domains:

1. RTL Design Exploration

• list_modules: Lists all Verilog modules in the workspace.

• find_module: Extracts module parameters, ports, and submodules.

• find_signal: Resolves a signal declaration, its bit width, driver logic, and fanout.

• show_hierarchy: Builds a recursive instantiation hierarchy tree.

• show_fsm: Extracts FSM states and transitions from case blocks.

• find_clock_domains & find_reset_tree: Identifies clocking networks and reset polarities.

2. Assertion Authoring & Linting

• generate_assertion: Translates natural language requirements into SystemVerilog Assertions (SVA).

• lint_assertion: Inspects SVA syntax, unclosed braces, and vacuity risks (e.g. antecedent constants).

• explain_assertion: Explains the temporal logic of an SVA property in plain English.

• optimize_assertion: Suggests simpler properties to reduce formal solver search spaces.

3. Formal Solver Wrappers

• run_formal: Runs formal verification runs (JasperGold, VC Formal, Questa) and parses log status.

• generate_constraints: Automatically infers resets and clocks to spit out a constraints template.

• analyze_counterexample: Summarizes root-cause signals and cycles from failing solver traces.

• compare_runs: Highlights status changes and runtime trends between two verification runs.

4. Waveform Log Analysis

• parse_vcd & parse_fsdb: Parses signal metadata and simulation times from waveform dumps.

• signal_history: Retrieves historical values of a signal across cycle intervals.

• explain_waveform: Explains digital handshakes in plain English from raw waveform transitions.

• compare_waveforms: Runs differential checks between two traces to identify cycle-by-cycle mismatches.

5. Specification RAG (Retrieval-Augmented Generation)

• search_spec: Searches indexed protocol spec sheets (AXI, APB, PCIe, USB, DDR, RISC-V).

• explain_protocol: Explains specific protocol constraints using spec context.

• requirement_to_property: Automatically aligns NL verification requirements with spec segments to write SVAs.

6. Verification Coverage

• analyze_coverage: Displays functional, assertion, and proof coverage percentages.

• uncovered_properties: Pinpoints assertions that are unproven or inactive.

• recommend_tests: Recommends solver stimulus updates to resolve uncovered nodes.

7. Bug Database

• search_bug: Semantic search over historical design bugs.

• similar_failures: Correlates new assertion failures with historical bugs.

• regression_summary: Summarizes overnight test runs.

8. Git Version Tracking

• search_commits: Finds commits affecting specific design files.

• blame_signal: Identifies which commits modified the lines declaring a given signal.

• recent_changes: Lists recent repository logs.

9. Utility Docs & Summary

• summarize_design: Creates high-level block architecture summaries.

• explain_module: Generates port-by-port interface descriptions.

• generate_documentation: Generates structured Markdown documentation files.

• dependency_graph: Maps module instantiation connections.

🚀 Installation & Local Execution

Prerequisites

• Python 3.12+

• Node.js (required for the interactive MCP inspector GUI)

Setup Virtual Environment

1. Clone this repository and open the workspace.

2. Initialize and load the Python virtual environment:

   python -m venv .venv
   .\.venv\Scripts\activate

3. Install dependencies:

   pip install -r requirements.txt
   pip install "mcp[cli]"

Running Locally (Interactive Inspector GUI)

You can test the server and run all 34 tools directly in your browser using the FastMCP developer console:

.\.venv\Scripts\mcp dev app/server.py

This automatically boots a local proxy server and opens a web interface showing tool signatures, inputs, and outputs.

🤖 Claude Desktop Configuration

To connect this MCP server directly to Claude Desktop so it can interact with your RTL files:

1. Locate your Claude configuration file at %APPDATA%\Claude\claude_desktop_config.json.

2. Add the following config block inside the "mcpServers" object (replace paths with your absolute workspace paths):

{
  "mcpServers": {
    "vlsi-formal-verification": {
      "command": "d:/VLSI-MCP/.venv/Scripts/python.exe",
      "args": [
        "d:/VLSI-MCP/app/server.py"
      ],
      "env": {
        "GEMINI_API_KEY": "your-gemini-api-key"
      }
    }
  }
}

3. Restart Claude Desktop. You should see the hammer icon active in the chat panel.

🧪 Running Automated Tests

We maintain a unit test suite using pytest that validates parsers, data models, linters, RAG semantic searches, and sqlite databases:

.\.venv\Scripts\python -m pytest tests/