parse_sva
Extracts SystemVerilog assume and assert property statements into an assume-guarantee contract and returns parsed properties, clocks, skipped items, and signal names for formal checks.
Instructions
Read the assume property and assert property statements of
SystemVerilog (a module, a bind file, or the statements alone; text or
a file path) as a contract: assumptions and guarantees, with the widths
of Verilog, $past, bounded sequences, and disable iff. The directions
come from the module ports, or from inputs or outputs (the other
signals are of the other kind). Returns the contract, the properties
read (label, kind, formula, from_cycle: the cycle from which a property
with $past is checked), skipped (statements not read, with the
reason), covers, the clock, and undeclared (signals read as 1
bit), and names (hierarchical names: u1__state is u1.state; give them
to to_sva). One clock per contract: clock ("posedge clk") chooses it.
Tool call template
This tool declares no required parameters. Add optional parameters from the input schema as needed.
{
"id": 1,
"jsonrpc": "2.0",
"method": "tools/call",
"params": {
"arguments": {},
"name": "parse_sva"
}
}Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| name | No | ||
| path | No | ||
| text | No | ||
| clock | No | ||
| inputs | No | ||
| outputs | No | ||
| parameters | No |