Diagram¶

Builds, simulates and verifies a circuit drawn as a diagram, and generates MC/DC tests for it (guide): the documents (*.intrepyd.json) of the intrepid-vscode circuit editor. It is the inverse of intrepyd.export: a netlist back into a Context, ready for the Simulator. The module docstring below describes the diagram format (sub-systems included) and the command line. The library blocks a diagram may use are those of the catalogue.

diagram ¶

Builds and simulates a circuit drawn as a diagram: the documents of the intrepid-vscode circuit editor (*.intrepyd.json). It is the inverse of intrepyd.export: the export turns a Context into a netlist, this turns a netlist (with the editor's own blocks) back into a Context, ready to be simulated or verified.

Diagram format (version 3)¶

::

{
  "format": "intrepyd-diagram",
  "version": 3,
  "circuit": {
    "nodes": [ ... ],   # intrepyd.export's nodes, plus the editor's blocks
    "edges": [ ... ]    # {"from", "to", "port"[, "fromPort"]}
  },
  "layout": { ... },    # the drawing, ignored here
  "simulation": {       # optional: what Simulate runs
    "steps": 10,
    "stimuli": { "<input block id>": ["true", "false", ...], ... }
  },
  "verification": {     # optional: how Verify runs
    "engine": "portfolio",  # or one engine: bmc, kind, br, pdr
    "timeout": 30,          # seconds, per property
    "depth": 50,            # the deepest depth bmc and kind try (optional)
    "certificates": false   # proof certificates for what is proved (optional)
  },
  "testgen": {          # optional: the MC/DC tests to generate
    "decisions": [{"block": 7, "stops": [5]}, ...],
    "timeout": 30,          # seconds, per condition
    "depth": 20             # the longest test, in steps after the first
  },
  "requirement": {      # optional: the requirement the circuit implements
    "id": "LLR-012",
    "title": "Alarm on occlusion",
    "text": "The pump shall raise the occlusion alarm when ...",
    "signals": {"pressure": "int16"},
    "formula": "(pressure > 300 and infusing) or door_open",
    "built": {...}          # what the editor last built the circuit from
  }
}

The requirement section is the editor's: the circuit a requirement's formula is built into is an ordinary circuit, in circuit, and this module builds, simulates and verifies it, and generates its MC/DC tests, as any other. The section itself is not read here.

On top of the export's schema, a diagram has:

"kind": "output" blocks (an output, named, with one input in);
"kind": "component" blocks, a block of intrepyd.lib ("module", "symbol", "params"); a wire's "fromPort" picks which of a block's outputs it carries (absent: the block's primary output);
"inputs" on an and/or/xor/add/mul gate drawn with more than two inputs (in0, in1, ...), built as a chain of binary calls;
the properties to verify: "kind": "assertion" (its boolean input must always hold) and "kind": "target" (a boolean condition to reach), each named, with one input in;
"kind": "subsystem" blocks, a part of the circuit drawn as one block: the blocks inside it have "parent": <its id> (ids are unique in the whole diagram, and a wire joins two blocks of one sub-system, or two at the top). Its In blocks are its inputs, wired from outside by their name ("port": "<the In block's name>"), and its Out blocks its outputs, in id order ("fromPort": 0, 1, ...). Sub-systems nest. The names of the blocks inside are prefixed with the sub-system's ("filter.acc") when built.

The library blocks are those of intrepyd.lib.catalogue, which describes each one (its parameters, pins, outputs and types).

Command line¶

python -m intrepyd.diagram simulate FILE (- reads standard input) simulates the diagram's simulation section (--steps overrides the number of steps) and prints, as JSON::

{"steps": N, "values": {"<block id>.<output>": ["T", "F", ...], ...}}

with one entry per output of every block (booleans as T/F, numbers as the trace prints them).

python -m intrepyd.diagram verify FILE checks each property on its own (--engine, --timeout, --depth override the diagram's verification section) and prints::

{"results": [{"block": id, "kind": "assertion", "name": "safe",
              "verdict": "holds" | "fails" | "reached" | "unreachable" | "unknown",
              "engine": "pdr", "time": 0.12,
              "trace": {"steps": N, "values": {...}, "stimuli": {...}}}, ...]}

An assertion holds or fails; a target is reached or unreachable; unknown when no engine answers in time. With --certificates (or "certificates": true), a property that holds or a target unreachable also has a "certificate": the proof, an SMT-LIB 2 script each of whose check-sat must answer unsat, which any SMT solver can run to check it (null when the engine that proved it gives none). The proof is checked by intrepid before it is given; one that does not hold makes the verdict unknown. Certificates need intrepid 1.4 or newer. A failing assertion or a reached target carries its trace: the inputs that lead there (stimuli, as the simulation section takes them) and every block's values along it, its last step being where the assertion fails or the target is reached.

In a simulation, the outputs of a sub-system carry the values of its Out blocks.

python -m intrepyd.diagram mcdc FILE generates MC/DC tests (Modified Condition / Decision Coverage) for the decisions of the diagram's testgen section (--decision ID, repeated, --depth and --timeout override it). A decision is a block with a boolean output (an Out, Assertion or Target block stands for what is wired into it); its conditions are found by walking back from it through the boolean operators (and, or, not, xor, iff, implies, ite) and the pins of sub-systems, down to the first net that is none of them: an input, a latch, a comparison, the output of a library block, or a block listed in the decision's "stops". Constants are not conditions, and a net reached twice is one condition. For each condition, the tests are a pair that shows it alone decides the outcome (masking MC/DC): the condition and the decision differ between the two tests, and in each the decision would change if the condition did. It prints::

{"criterion": "masking", "results": [{
    "decision": id, "name": "and1",
    "conditions": [{"block": id, "output": 0, "name": "in1",
                    "status": "covered" | "unreachable" | "unknown",
                    "pair": [0, 1], "engine": "bmc", "time": 0.1}, ...],
    "tests": [{"steps": N, "stimuli": {...}, "values": {...},
               "conditions": ["T", "F", ...], "decision": "T"}, ...],
    "covered": 2, "total": 2}, ...]}

Each test is a run of the circuit (its inputs at each step, as stimuli, and every block's values along it, as a simulation gives them); its conditions and its decision are read at its last step. A condition is unreachable when no pair of tests can show it decides the decision (it is masked, or the logic around it is redundant), unknown when none was found within the depth and the timeout. The tests are not a minimal set: two conditions may share a test only when they happen to.

python -m intrepyd.diagram catalogue prints the library blocks a diagram may use (intrepyd.lib.catalogue), as JSON.

On an error the commands print the reason to standard error and exit with status 1.

DiagramError ¶

Bases: ValueError

A diagram that cannot be built, with a reason a user can read.

Circuit ¶

Circuit(ctx, inputs, outputs)

A diagram built in a Context: the context, the net of each block output (outputs[(block id, output index)]) and the net of each input block (inputs[block id]).

load ¶

load(source)

A diagram from a path, a file object, a JSON string or a dict, checked to be an intrepyd diagram of the version this module reads.

build ¶

build(diagram, ctx=None)

Builds the circuit of a diagram (see load) in ctx (a new Context if None) and returns a Circuit. Raises DiagramError if a block is unknown or an input is not wired; intrepyd's own errors (a type mismatch) propagate.

simulate ¶

simulate(diagram, steps=None, stimuli=None)

Simulates a diagram for steps steps with stimuli (input block id -> the value at each step, as the editor writes them: "true"/"false", numbers), by default its simulation section. Returns {"steps": n, "values": {"<id>.<output>": [value at step 0, ...]}}.

verify ¶

verify(diagram, engine=None, timeout=None, depth=None, certificates=None)

Checks each property of a diagram (its assertion and target blocks) on its own, with engine (the portfolio, or one engine), timeout seconds each and, for bmc and kind, at most depth steps — by default the diagram's verification section. Returns {"results": [...]} (see the module documentation): a verdict per property, and the trace of a failing assertion or a reached target. With certificates, a proved property comes with its proof certificate.

conditions ¶

conditions(diagram, decision, stops=())

The conditions of a decision: walking back from block decision through the boolean operators and the pins of sub-systems, the first nets that are none of them, or blocks of stops (see the module documentation). Returns [{"block": id, "output": index, "name": ...}], in the order they are met, the inputs of a block in pin order.

mcdc ¶

mcdc(diagram, decisions=None, depth=None, timeout=None)

Generates MC/DC tests for decisions (block ids, or {"block": id, "stops": [...]}), by default those of the diagram's testgen section, each test at most depth steps after the first, timeout seconds per condition. Returns {"criterion": "masking", "results": [...]} (see the module documentation).

main ¶

main(argv=None)

python -m intrepyd.diagram simulate|verify|mcdc FILE|- [options], or catalogue