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

---

## 🛠️ 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:
   ```powershell
   python -m venv .venv
   .\.venv\Scripts\activate
   ```
3. Install dependencies:
   ```powershell
   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:
```powershell
.\.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):

```json
{
  "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:
```powershell
.\.venv\Scripts\python -m pytest tests/
```