Commit Graph

197 Commits

Author SHA1 Message Date
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
Miodrag Milanovic 9647f6326f Update CHANGELOG and manual 2022-02-07 17:07:48 +01:00
Miodrag Milanovic c428a894c0 Next dev cycle 2022-01-11 08:39:34 +01:00
Miodrag Milanovic 8b1eafc3ad Release version 0.13 2022-01-11 08:35:50 +01:00
Miodrag Milanovic 64972360a8 Update CHANGELOG 2022-01-11 08:21:12 +01:00
Zachary Snow aa35f24290 sv: auto add nosync to certain always_comb local vars
If a local variable is always assigned before it is used, then adding
nosync prevents latches from being needlessly generated.
2022-01-07 22:53:22 -07:00
Zachary Snow 828e85068f sv: fix size cast internal expression extension 2022-01-07 21:21:02 -07:00
Zachary Snow 8c509a5659 sv: fix size cast clipping expression width 2022-01-03 08:17:35 -07:00
Zachary Snow 7608985d2c fix width detection of array querying function in case and case item expressions
I also removed the unnecessary shadowing of `width_hint` and `sign_hint`
in the corresponding case in `simplify()`.
2021-12-17 21:22:08 -07:00
Miodrag Milanovic c23cd00f30 Next dev cycle 2021-12-03 12:51:34 +01:00
Miodrag Milanovic 2156e20db5 Release version 0.12 2021-12-03 12:48:49 +01:00
Miodrag Milanovic 4792d925fc Update CHANGELOG and CODEOWNERS 2021-12-01 08:42:37 +01:00
Miodrag Milanovic a28ee81be0 Next dev cycle 2021-11-05 12:52:24 +01:00
Miodrag Milanovic 360fed8e4d Release version 0.11 2021-11-05 12:47:38 +01:00
Miodrag Milanovic 051b234df6 Add missing changelog item 2021-11-05 10:08:50 +01:00
Miodrag Milanovic c0edfa8788 Add missing items in CHANGELOG 2021-10-29 13:31:41 +02:00