Intrepid Circuit Editor
Write the requirements of a design, draw the circuit that implements it,
simulate it, prove its properties or get the steps that break them, and
generate the MC/DC tests that show each condition of a decision counts.
The model checker intrepyd works
underneath, out of sight.
What it does
- Circuits in the style of Simulink: inputs, gates, comparisons,
arithmetic, delays, timers and counters, wired pin to pin, grouped into
subsystems, checked as you draw.
- Simulation: give the inputs their values step by step, and see the
outputs on the canvas and the signals in a scope.
- Verification: an Assertion is proved to hold at every step, or comes
with the steps that break it; a Target is reached, or proved unreachable.
A property proved can come with its proof certificate, a script any SMT
solver checks.
- Requirements: a table of requirements, each with its text and a
formula, from which its circuit is built.
- MC/DC tests, and a report to print, a page per requirement.
- AI assistants: Claude Code, GitHub Copilot's agent mode and others
work with the tables and circuits. A requirement written in plain words
becomes a row with its formula, checked by intrepid, and marked as the
assistant's until you accept it.
- Lustre and Python: a Lustre model or an intrepyd program opens as a
circuit, and a circuit exports to a Python program.
Getting started
Install intrepyd in a Python 3.11 or newer, the one VS Code uses for
your workspace (Python: Select Interpreter):
pip install intrepyd
or let the editor do it: when that Python has none, it offers to.
The Intrepid icon appears in the Activity Bar. Help: Get Started
offers the walkthrough Get started with the Intrepid Circuit Editor;
Intrepid: New Circuit opens an empty circuit.
The documentation has a
tutorial, which takes a small project from its requirements to its report,
and the reference of the blocks, the formulas and the commands.
Requirements
- Visual Studio Code 1.85 or newer, and the Python extension, which comes
with this one;
- intrepyd in the selected Python: 0.20 or newer to simulate and verify, 0.21
for subsystems and proof certificates, 0.22 for MC/DC tests, 0.25 for the
tests of a requirement whose formula uses
next, 1.1.0 to compare two
circuits, 1.5.0 for the monitors (responds, holds_for, …). With an
older one, the editor says what is missing;
- intrepyd has its wheels for Linux (x86-64), Windows (x86-64) and macOS 13.3
or newer on Apple silicon.
License
The extension is free for noncommercial use, under the PolyForm
Noncommercial License 1.0.0; a commercial license is available on request,
from license@intrepid-studio.eu.
Verify and MC/DC tests run the engines of intrepid, inside intrepyd,
under a license of their own: intrepyd comes with a noncommercial one, and
work in a company needs a commercial one. The status bar shows the license
in use; Intrepid: Ask for a License writes the email that asks for one.
Before the first verification, the editor asks you to accept the
Intrepid End-User License Agreement.
See The engines' license.
Support
Problems and questions: support@intrepid-studio.eu.
| |
