is_implementation
Checks whether a given implementation—LTL formula, state machine, controller, or RTL module—satisfies an assume-guarantee contract, returning valid or an invalid result with a violating trace.
Instructions
Is the implementation an implementation of the contract (M |=_M C)? The
implementation is an LTL formula (implementation): implementation & A
-> G must be valid;
or a state machine, every behavior of which must satisfy A -> G. A
machine that refuses inputs can implement a contract only because of
that: check it with is_receptive. valid, or invalid with a trace and,
in details.violated, the guarantees that this trace breaks (others may
fail on other behaviors: check a term alone to know).
context: formulas that every behavior satisfies (e.g. an axiom of an
encoding, a physical law); the behaviors that violate them are left out.
The state machine is given as one of: smv, a program in SMV (the input
language of nuXmv: MODULE main with VAR/IVAR, INIT, TRANS..., no
specification) that declares the variables of the contract; machine, a
state machine in JSON {"name", "inputs", "outputs", "states", "initial",
"transitions": [{"from", "when", "outputs", "to"}]}: at each step, in its
state, the machine takes a transition whose when (a formula over the
variables) holds, sets the outputs of that step, and moves to to; or
controller, the controller returned by synthesize, with the contract it
was synthesized from in synthesized_from (default: the contract); or
rtl, a Verilog or SystemVerilog module (see rtl_ports for its ports).
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": "is_implementation"
}
}Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| rtl | No | ||
| smv | No | ||
| backend | No | auto | |
| context | No | ||
| machine | No | ||
| timeout | No | ||
| contract | Yes | ||
| controller | No | ||
| implementation | No | ||
| synthesized_from | No |