RFC: pyebmc Python bindings design

[kroening]

This is a Request for Comments for the design of pyebmc, a Python bindings package for EBMC.

Summary

• EDA-familiar API (read_verilog, elaborate, prove) on a Design session object
• CBMC IR types (Expr, Type) in a separate pyebmc.cprover namespace (to eventually become its own package)
• Property iteration with full expression tree access
• Constraint API for per-time-frame assumptions
• pybind11 binding layer

Feedback requested

• API naming and conventions
• Namespace separation (pyebmc vs pyebmc.cprover)
• Engine/solver parameter design
• Expression construction API (future)

[jimgrundy]

• The reset sequence command might be a little too simple for more complex designs. Well, actually, I can't tell maybe the "*" on line 148 covers a lot. The other tools let you give a file that supplies a sequence of values to be pumped in over time to reset a device. I've had caches that took over a thousand cycles to bring to the initial state. That said, that mechanism always sucked. I would rather have been able to define my own reset state machine that I could attach to the design under verification for the reset period (after which it would detach letting the inputs it drove float (constrained by the environment).

• Among the property management APIs I'm missing a command that would convert an assert to an assume and visa versa. These are really handy for compositional verification and for sharing properties between FV and DV. I couldn't live without them.

• The "get_trace" doc string says it is to get the trace of a refuted property. Is there also a notion of a cover property and this also works for that? It doesn't look that way from the PropertyStatus type, but I find those really important for checking how far I am getting into a design with bounded model checking and convincing myself that proofs aren't vacuous.

• Is this interface rich enough to implement CAG? We built CAG for another tool using it's Tcl interface. We found it much more productive.   Maybe not yet, as it involved manipulating the net-list and I see that is a "to do" for the API.

[tautschnig]

A few themes that I think need to be settled:

1. Stringly-typed parameters (engine, solver, format, property identifiers) should be enums or typing.Literal — both for IDE autocomplete and to keep the accepted set documented in one place.
2. Property identity is handled inconsistently (sometimes name, sometimes identifier, sometimes a Property — rarely all three). Pick one and let users pass Property objects everywhere an identifier is accepted.
3. Expression construction is listed as "future" but add_property_expr is in the initial API and Design.add_constraint takes strings — there's a mismatch that needs resolving before the RFC is accepted.
4. Runtime concerns that are invisible from a Python-level design but matter a lot for usability — GIL release during long solves, SIGINT handling, multiple concurrent Design instances, cleanup — aren't mentioned. An RFC is the right time to commit to them.

It would help to add a short "Validation" section outlining how the API will be exercised before release (doctest of the examples? an examples/pyebmc/ regression target? unit tests for the binding layer?). That would also make it clear that the usage examples throughout are intended to stay runnable.

[tautschnig]

Namespace migration plan: if pyebmc.cprover is going to move to a standalone pycprover package, please commit to shipping both import paths from day 1 (with pyebmc.cprover being a thin re-export of pycprover). Otherwise every user will have a painful from pyebmc.cprover import … → from pycprover import … migration when the split happens, and that window lasts for however long it takes the ecosystem to catch up. Fixing the preferred import path now costs nothing and is the one piece of the RFC that is most expensive to change later.

[tautschnig]

Two things on the Design constructor:

1. solver: str should be Literal["minisat", "cadical", "z3", "bitwuzla"] (or an enum). A typo silently falls back to the default string otherwise, and IDEs can't autocomplete.
2. Nothing here covers cleanup. The RFC lists "context managers" as a design principle but Design has no __enter__/__exit__ and no close(). Long-running Python processes that create and discard sessions will leak solver state unless destruction is guaranteed. Please add both an explicit close() and the __enter__/__exit__ pair.

Also worth mentioning: can there be multiple Design instances alive at once? CBMC has historically carried global state (messaget, dstringt tables) that makes concurrency tricky. If only one session is supported per process, say so explicitly; if not, call out the threading guarantees.

[tautschnig]

include_dirs and defines are per-file here, which matches Tcl's read_verilog -define / -incdir but not the more common Tcl pattern of set_include_path / set_define as session state. In practice users with large designs set these once globally. Suggest adding them as Design.__init__ keyword args (session-wide defaults) that can still be overridden per-call, instead of forcing the user to pass the same include_dirs=[...] argument to every read_verilog call.

[tautschnig]

For consistency with read_verilog_string, consider adding read_smv_string as well. Users who programmatically construct SMV snippets (test harnesses, benchmarks) otherwise have to round-trip through a temp file.

[tautschnig]

As follow-up to @jimgrundy's comment: the reset API is too shallow for non-trivial designs. A single signal + polarity + cycle count doesn't cover the real-world case of caches / DMA engines that need hundreds to thousands of cycles of coordinated input sequences before reaching the initial verification state.

Two directions worth considering:

1. Accept a Trace-like object (or a list of dicts {signal: value, ...}) describing the reset stimulus per cycle. This is the "input file" pattern Jim alluded to.
2. Allow set_reset(module=<SVModule>) where the user provides a synthesizable SV module to drive reset-phase inputs, which is then composed with the DUT and detached after reset.

Even if the first release only implements option 1, the API shape should leave room for option 2 so users aren't forced to rewrite code later. Right now set_reset(signal=..., cycles=...) paints us into the simple-case corner.

[tautschnig]

The exception hierarchy is missing a TypecheckError (or similar). SystemVerilog typechecking happens inside elaborate(), and right now typecheck failures would have to be fused into ElaborationError (losing source location info) or ParseError (misleading). Also, only ParseError has structured file/line/message fields — all of the errors that originate from source code should carry that info.

Suggestion: define a small base mixin:

class EbmcSourceError(EbmcError):
    file: str | None
    line: int | None
    message: str

and inherit ParseError, TypecheckError, ElaborationError from it. That gives tooling (e.g., an IDE wrapper, pytest reporter) one predictable way to surface source locations.

[tautschnig]

Worth calling out: what does the user see in the terminal / Python logs while check_property(bound=50) runs for minutes? The RFC mentions routing EBMC messages to logging further down, but doesn't say anything about:

• GIL release during the solver call. If the pybind11 layer holds the GIL for the duration of a solve, no other Python thread (UI, progress bar, logging handler with its own thread) can make progress.
• SIGINT / Ctrl-C handling. Users running this interactively will hit Ctrl-C. Does it cancel cleanly? Does the Design remain usable afterwards?
• Progress / cancellation token. For long checks, EDA users expect to be able to pass a timeout or a callback. Consider adding timeout: float | None = None and/or on_progress: Callable[[Status], None] | None = None on check_property.

These are all implementation details, but committing to them in the RFC avoids painful retrofitting later.

[tautschnig]

This is in direct tension with Design.add_property_expr(name, expression: Expr) at line 199 and the "Build: G(counter != 0)" example on lines 903-908. Either:

1. Expression construction is in the initial release, in which case G, symbol, constant, unsigned_bv, __ne__ on Expr, etc. need real signatures in the RFC (especially: how are Verilog integer-promotion / width-matching rules handled for counter != zero?), or
2. Expression construction is explicitly deferred, in which case Design.add_property_expr should also be deferred — otherwise users have a method they can't call.

My preference is (2) for the initial release, documented as "deferred to v2". That gives time to design Expr construction properly (arguably the hardest API in the whole binding) without locking the shape in prematurely.

[tautschnig]

A few issues with the illustrative pybind11 snippet that will bite during implementation (worth fixing now so the RFC doesn't mislead):

1. e.find(dstringt(key)) — irept::find takes const irep_idt &, not dstringt. Use e.find(key) (implicit conversion) or e.find(irep_idt{key}).
2. py::cast(id2string(val.id())) — this assumes every named sub is itself an id-only irep. Many named subs hold a full expression or a string value under ID_value. .get() should probably return a richer type (str | Expr | None) or be split into get_string() / get_expr().
3. py::tuple(py::cast(e.operands())) — py::cast of std::vector<exprt> returns a py::list, not something tuple-constructible directly. Use py::cast(e.operands()).cast<py::tuple>() or iterate explicitly.
4. e.hash() returns std::size_t; Python's __hash__ wants a Py_hash_t (signed). Mask / truncate so negative-hash surprises don't show up on 32-bit platforms.

None of this changes the API shape — just marking the snippet as // illustrative; see actual binding code if you don't want to get into the weeds here.

[tautschnig]

CAG (from @jimgrundy's review): noted as requiring netlist manipulation, which is in "Future Extensions". Worth being explicit here about whether the netlist surface (read gates, insert observers, constrain nets) is something this RFC commits to eventually exposing, or whether it's out of scope. EDA users evaluating pyebmc will want to know before adopting it for CAG-style workflows.

Also missing from Future Extensions but worth having in the RFC so reviewers don't wonder: Python version support policy (the doc uses PEP 604 str | Path which is 3.10+, please state the minimum supported version), wheel/sdist distribution strategy (manylinux tags, macOS universal, Windows), and how the bundled solver licenses (MiniSat / CaDiCaL / Z3) compose with pyebmc's own license.