From f041e36c6e142878c5bca4da5b459177c4f75e07 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 2 Aug 2022 16:49:36 +0200 Subject: 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. --- .gitignore | 3 +++ 1 file changed, 3 insertions(+) (limited to '.gitignore') 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 -- cgit v1.2.3