Commit Graph

212 Commits

Author SHA1 Message Date
Miodrag Milanovic 7ce5011c24 Release version 0.23 2022-11-08 07:55:31 +01:00
Miodrag Milanovic cff42f0af5 Update CHANGELOG 2022-11-07 13:16:38 +01:00
Miodrag Milanovic 9470ef9efe Update CHANGELOG 2022-11-07 12:13:19 +01:00
Jannis Harder ac906d15ce Add YOSYS_ABORT_ON_LOG_ERROR environment variable for debugging. 2022-10-07 15:02:33 +02:00
Miodrag Milanovic a5172df9e9 Next dev cycle 2022-10-05 11:32:11 +02:00
Miodrag Milanovic f109fa3d4c Release version 0.22 2022-10-05 11:30:38 +02:00
Miodrag Milanovic 7db26a8e59 Update CHANGELOG 2022-10-05 11:28:48 +02:00
Miodrag Milanovic 07d9924a1b Next dev cycle 2022-09-06 08:26:44 +02:00
Miodrag Milanovic e6d2a900a9 Release version 0.21 2022-09-06 08:23:30 +02:00
Miodrag Milanovic 0ff129c10b Update Changelog 2022-09-06 08:22:23 +02:00
Jannis Harder f7023d06a2 sim: -hdlname option to preserve flattened hierarchy in sim output 2022-08-16 13:37:30 +02:00
Jannis Harder 65145db7e7 rename: Add -witness mode 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
Jannis Harder a2f9ebe43a memory_map: Add -formal option
This maps memories for a global clock based formal verification flow.
This implies -keepdc, uses $ff cells for ROMs and sets hdlname
attributes.
2022-08-16 13:37:30 +02:00
Jannis Harder c0063288d6 Add the $anyinit cell and the formalff pass
These can be used to protect undefined flip-flop initialization values
from optimizations that are not sound for formal verification and can
help mapping all solver-provided values in witness traces for flows that
use different backends simultaneously.
2022-08-16 13:37:30 +02:00
Miodrag Milanovic 733902c81e Next dev cycle 2022-08-03 13:57:14 +02:00
Miodrag Milanovic 4fcb95ed08 Release version 0.20 2022-08-03 13:53:41 +02:00
Miodrag Milanovic a07b06d5e7 Update Changelog 2022-08-03 13:52:01 +02:00
Miodrag Milanovic 6a1d98b816 Update manual and changelog 2022-08-03 10:30:58 +02:00
Miodrag Milanovic da0682b99a Next dev cycle 2022-07-04 14:08:53 +02:00
Miodrag Milanovic a45c131b37 Release version 0.19 2022-07-04 14:07:01 +02:00
Jannis Harder 5343911263 Mention smtlib2_module in README.md and CHANGELOG 2022-07-04 13:54:49 +02:00
Miodrag Milanovic 59b96bb1f8 Upadte documentation and changelog 2022-07-04 11:09:06 +02:00
Miodrag Milanovic 4b423dcfb4 Next dev cycle 2022-06-10 15:05:09 +02:00
Miodrag Milanovic 19ce3b45d6 Release version 0.18 2022-06-10 15:01:40 +02:00
Miodrag Milanovic 1940bf647f Updated CHANGELOG 2022-06-10 09:08:23 +02:00
Miodrag Milanovic 6e8e4b4550 verific: Added "-vlog-libext" option to specify search extension for libraries 2022-06-09 08:57:48 +02:00
Miodrag Milanovic a0172e68c5 More updates on CHANGELOG 2022-06-08 11:41:13 +02:00
Miodrag Milanovic 096f3d2aa4 Update changelog and manual 2022-06-08 11:28:06 +02:00
Zachary Snow a650d9079f verilog: fix width/sign detection for functions 2022-05-30 16:45:39 -04:00
Jannis Harder 4bfaaea0d5 verilog: fix size and signedness of array querying functions
genrtlil.cc and simplify.cc had inconsistent and slightly broken
handling of signedness for array querying functions. These functions are
defined to return a signed result. Simplify always produced an unsigned
and genrtlil always a signed 32-bit result ignoring the context.

Includes tests for the the relvant edge cases for context dependent
conversions.
2022-05-30 09:11:31 -04:00
Jannis Harder b75fa62e9b verilog: fix $past's signedness 2022-05-25 16:32:08 -04:00
Jannis Harder cffec1f95f verilog: fix signedness when removing unreachable cases 2022-05-24 23:03:31 -04:00
Miodrag Milanovic d562bfd165 Next dev cycle 2022-05-09 10:12:32 +02:00
Miodrag Milanovic 6f9602b4cf Release version 0.17 2022-05-09 10:11:04 +02:00
Miodrag Milanovic 72d2efeb32 Update CHANGELOG 2022-05-09 10:06:15 +02:00
Zachary Snow bf15dbd0f7 sv: fix always_comb auto nosync for nested and function blocks 2022-04-05 14:43:48 -06:00
Miodrag Milanovic 957fdb328a Next dev cycle 2022-04-05 11:50:49 +02:00
Miodrag Milanovic b63e0a0cae Release version 0.16 2022-04-05 11:49:37 +02:00
Miodrag Milanovic 0d3bf9e725 Update CHANGELOG and manual 2022-04-04 16:53:47 +02:00
Miodrag Milanovic 7be7f5e02e Next dev cycle 2022-03-04 11:37:18 +01:00
Miodrag Milanovic 07a43689d8 Release version 0.15 2022-03-04 11:36:03 +01:00
Miodrag Milanovic 3818e1160d Update CHANGELOG 2022-03-02 14:26:15 +01:00
Zachary Snow 15a4e900b2 verilog: support for time scale delay values 2022-02-14 15:58:31 +01:00
Kamil Rakoczy 68c67c40ec
Fix access to whole sub-structs (#3086)
* Add support for accessing whole struct
* Update tests

Signed-off-by: Kamil Rakoczy <krakoczy@antmicro.com>
2022-02-14 14:34:20 +01:00
Zachary Snow 15eb66b99d verilog: fix dynamic dynamic range asgn elab 2022-02-11 22:54:55 +01:00
Zachary Snow 90bb47d181 verilog: fix const func eval with upto variables 2022-02-11 21:01:51 +01:00
Miodrag Milanovic 818060880d Next dev cycle 2022-02-07 17:10:50 +01:00
Miodrag Milanovic a4522d6282 Release version 0.14 2022-02-07 17:08:39 +01:00