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
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
