6 Commits

Author	SHA1	Message	Date
Jannis Harder	dcc4d6e90b	yosys-witness: Don't treat aiw x-bits as don't change ... While treating initialization only bits as don't change during later cycles is correct, actual x-bits should be kept as x-bits.	2023-06-09 15:21:22 +02:00
Jannis Harder	7ddec5093f	sim: Improvements and fixes for yw cosim ... * Fixed $cover handling * Improved sparse memory handling when writing traces * JSON summary output	2023-01-11 18:07:16 +01:00
Jannis Harder	636b9f2705	Support for BTOR witness to Yosys witness conversion	2023-01-11 18:07:16 +01:00
Jannis Harder	b156fe903f	yosys-witness: Add stats command	2022-08-16 13:37:30 +02:00
Jannis Harder	efd5b86eb9	aiger: Add yosys-witness support ... Adds a new json based aiger map file and yosys-witness converters to us this to convert between native and AIGER witness files.	2022-08-16 13:37:30 +02:00
Jannis Harder	f041e36c6e	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.	2022-08-16 13:37:30 +02:00