CHASE MCP Server

Overview Schema Source Related Servers Discussions Admin

to_sva

Read-onlyIdempotent

Converts an assume-guarantee LTL contract into a SystemVerilog checker module with assume/assert properties, reset handling, and optional bind statements for design integration.

Instructions

Write a contract as a SystemVerilog checker module: assumptions as assume property, guarantees as assert property, clocked by @(edge clock); a formula G p is checked at every cycle, any other once (initial). reset (e.g. "rst" or "!rst_n") disables the properties while it holds; bind, the name of a design module, adds a bind statement (ports connected by name; names, from parse_sva, connects the hierarchical names). Any tool that reads SVA can check the module. Real variables cannot be written.

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": {
      "contract": "<contract>"
    },
    "name": "to_sva"
  }
}

Input Schema

Name	Required	Default
`bind`	No
`edge`	No	posedge
`clock`	No	clk
`names`	No
`reset`	No
`module`	No
`contract`	Yes

Output Schema

Name	Required	Description	Default
`result`	Yes

Schema Changelog

Changes observed during successful MCP inspections.

Changed1 schema field changedv0.7.0Nov 2, 2026

addedInput schema / $defs / ContractSpec / properties / constants

Added value: +{
+  "additionalProperties": {
+    "anyOf": [
+      {
+        "type": "integer"
+      },
+      {
+        "type": "number"
+      }
+    ]
+  },
+  "description": "Named constants: name -> value; the formulas use the names (repair changes them)",
+  "title": "Constants",
+  "type": "object"
+}

Addedv0.4.2Oct 29, 2026

TDQS

A4.5/5.0

Behavior5/5

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

Annotations only declare readOnly/idempotent/openWorld=false; the description adds substantial behavior: G p is checked every cycle while other formulas are checked once (initial), `reset` disables properties while asserted, and bind injects a bind statement with by-name port connection. It also flags a real constraint: "Real variables cannot be written." This is exactly the kind of context annotations cannot carry.

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

Conciseness4/5

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

Front-loaded with the core action, then parameter behavior in roughly the order an agent would need it. Dense without being padded, though the middle clause run about G p versus initial timing is compressed enough to require a second read.

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

Completeness4/5

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

With an output schema present, return values need not be described, and the nested ContractSpec fields carry their own descriptions. The description covers the awkward top-level knobs well; only `module` and the precise relationship between `module` and `bind` are left unexplained for a 7-parameter tool.

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

Parameters4/5

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

Schema coverage of the top-level properties is 0%, so the description is the primary source, and it delivers: `edge` and `clock` drive the @(edge clock) sampling, `reset` is explained with concrete examples ("rst" or "!rst_n"), `bind` and `names` are described in terms of port connection and their parse_sva origin. The `module` parameter is never mentioned, leaving one meaningful gap.

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?

States a specific verb and resource ("Write a contract as a SystemVerilog checker module") and immediately specifies the mapping: assumptions become assume property, guarantees become assert property. That level of detail lets an agent distinguish this from parse_sva (the inverse direction) and from to_spec without opening a schema.

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

Usage Guidelines4/5

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

Gives clear operating context: `names` comes from parse_sva, and `bind` names the design module so ports are connected by name, which is effectively a workflow prescription. It also notes the output is consumable by "any tool that reads SVA". No explicit when-not-to-use or exclusion versus to_spec, so not a 5.

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