Export

Exports the circuit of a Context as a JSON graph (a netlist), for drawing it as a block diagram. The module docstring below is the authoritative description of the JSON schema.

export

Exports the circuit of a Context as a JSON graph (a netlist), so that it can be drawn as a block diagram — the intrepid-vscode extension is the first consumer, but the format is generic.

The structure comes from the context's recipe (intrepyd.recipe), the record of the calls that built every net, which already holds each net's operator and its fanin as references; names come from net2name and the outputs from context.outputs. Nothing is read from the native library, so the export is pure python and works wherever a built Context does.

JSON schema (version 2)

Version 2 adds file/line to a node; version 1 is the same without them, and a reader should accept both.

::

{
  "version": 2,
  "nodes": [
    {
      "id":    <int>,         # the net, unique in the graph; edges use it
      "kind":  "input" | "latch" | "const" | "gate" | "output" | "external",
      "name":  <str|null>,    # the user's name, null if intrepyd made one up
      "op":    <str|null>,    # for a gate: "and", "add", "ite", ...; for a
                              #   boolean constant: "true"/"false"; else absent
      "type":  <str|null>,    # "bool", "int8", ..., "int", "real", "float32"
                              #   when known (input/latch/const), else absent
      "value": <str>,         # for a const: "0", "true", "?", ... (else absent)
      "group": <str>,         # the namespace of the name, e.g. "Counter" for
                              #   "Counter.q" (else absent)
      "file":  <str>,         # the source file that built the net (else absent)
      "line":  <int>,         # the line in "file" that built it (with "file")
      "output": true          # present only when the net is tagged an output
    }
  ],
  "edges": [
    { "from": <int>, "to": <int>, "port": <str> }
    # the net <from> feeds input port <port> of net <to>; ports are
    # "init"/"next" for a latch, "if"/"then"/"else" for an ite, "in" for a
    # unary operator, "a"/"b" for a binary one, else "in0", "in1", ...
  ]
}

A node is one net. Outputs are a flag on the net they tag, not separate nodes. const covers numbers and the predefined true/false/undef (whose value is "?"). A fanin that was built outside the context appears as an external node with no detail, so the graph stays connected.

If the program also builds a trace (a simulation or a counterexample), the graph carries it, so a viewer can overlay the values on the blocks over time::

"trace": {
  "depth":  <int>,                     # number of steps, 0..depth-1
  "values": { "<net id>": ["v@0", "v@1", ...], ... }  # watched nets only
}

The values are the strings the trace holds ("5", "T"/"F" for booleans, "?" for unknown). Only the nets the trace watches are present. The field is absent when the program builds no usable trace.

to_graph

to_graph(context)

The circuit of context as a JSON-able dict following the schema above.

to_json

to_json(context, indent=2)

The circuit of context as a JSON string.

dump

dump(context, path, indent=2)

Writes the circuit of context as JSON to path.

trace_payload

trace_payload(trace)

A trace's watched nets as {"depth": n, "values": {str(net): [v@0, ...]}}, to overlay a simulation or counterexample on the graph (see the schema). The values are the strings the trace holds; only the watched nets are present.

main

main(argv=None)

python -m intrepyd.export program.py [-o out.json]: run the program and export the circuit of the context it builds (the one with the most nets, if it builds several) to out.json or standard output.