diff options
| author | Jannis Harder <me@jix.one> | 2022-08-02 16:49:36 +0200 |
|---|---|---|
| committer | Jannis Harder <me@jix.one> | 2022-08-16 13:37:30 +0200 |
| commit | f041e36c6e142878c5bca4da5b459177c4f75e07 (patch) | |
| tree | b3d9f04b93d12b593a9429e1331bfda5544b8de8 /.gitignore | |
| parent | 96a1173598ec1bf93670b2de3c8bb087f03a8528 (diff) | |
| download | yosys-f041e36c6e142878c5bca4da5b459177c4f75e07.tar.gz yosys-f041e36c6e142878c5bca4da5b459177c4f75e07.tar.bz2 yosys-f041e36c6e142878c5bca4da5b459177c4f75e07.zip | |
smtbmc: Add native json based witness format + smt2 backend support
This adds a native json based witness trace format. By having a common
format that includes everything we support, and providing a conversion
utility (yosys-witness) we no longer need to implement every format for
every tool that deals with witness traces, avoiding a quadratic
opportunity to introduce subtle bugs.
Included:
* smt2: New yosys-smt2-witness info lines containing full hierarchical
paths without lossy escaping.
* yosys-smtbmc --dump-yw trace.yw: Dump results in the new format.
* yosys-smtbmc --yw trace.yw: Read new format as constraints.
* yosys-witness: New tool to convert witness formats.
Currently this can only display traces in a human-readable-only
format and do a passthrough read/write of the new format.
* ywio.py: Small python lib for reading and writing the new format.
Used by yosys-smtbmc and yosys-witness to avoid duplication.
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore index 0460c7c13..49b886e7e 100644 --- a/.gitignore +++ b/.gitignore @@ -28,6 +28,9 @@ __pycache__ /yosys-smtbmc /yosys-smtbmc.exe /yosys-smtbmc-script.py +/yosys-witness +/yosys-witness.exe +/yosys-witness-script.py /yosys-filterlib /yosys-filterlib.exe /kernel/*.pyh |