Skip to main content
Glama
Sign In
mcp-formal

mcp-formal

by zesun33
OverviewSchemaSourceRelated ServersDiscussionsAdmin
TypeScript
Local

formal_lint_sva

Elaborates RTL with embedded SVA via Yosys to report syntax and elaboration errors with file:line diagnostics, serving as a pre-check before formal proof.

Instructions

Elaborates RTL with embedded SVA in Yosys to catch syntax and elaboration errors before solver time. Reports file:line diagnostics. Does not prove anything; use formal_prove for verdicts.

Tool call template

Replace each placeholder with a value matching the input schema. Only required parameters are included; add optional parameters as needed.

{
  "id": 1,
  "jsonrpc": "2.0",
  "method": "tools/call",
  "params": {
    "arguments": {
      "verilog_sources": "<verilog_sources>",
      "top_module": "<top_module>"
    },
    "name": "formal_lint_sva"
  }
}

Input Schema

NameRequiredDescriptionDefault
cwdNoOptional working directory.
top_moduleYesTop module name.
verilog_sourcesYesRTL files to elaborate.

Schema Changelog

Changes observed during successful MCP inspections.

  1. First observedv0.1.0

TDQS

A4.7/5.0
Behavior5/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

With no annotations provided, the description carries the full burden of behavioral transparency. It discloses that it reports file:line diagnostics and explicitly states it does not prove anything, making the tool's behavior and limitations clear.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is two sentences, front-loaded with the primary verb and purpose, and contains no redundant or extraneous information. It efficiently conveys the tool's function and its relationship to the sibling tool.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness5/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

The description is complete for the tool's complexity: it states what it does, what it outputs (file:line diagnostics), what it does not do (prove), and the context of use (before solver time). No additional context is needed for correct invocation.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

The input schema already provides descriptive text for all three parameters (cwd, top_module, verilog_sources), achieving 100% schema coverage. The description does not add extra parameter semantics, so the baseline score of 3 is appropriate.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the tool's purpose with a specific verb ('Elaborates RTL with embedded SVA in Yosys') and its scope ('catch syntax and elaboration errors before solver time'). It explicitly distinguishes itself from sibling tool formal_prove by noting it does not prove anything.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines5/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description provides explicit guidance on when to use it (before solver time for syntax/elaboration checks) and when not to use it, directing the agent to formal_prove for verdicts. This directly addresses the alternative tool and the condition for selecting it.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

Deploy Server

Other Tools