Commit Graph

12789 Commits

Author SHA1 Message Date
Archie e7e8e3b0f6 Adding expected error message. 2022-06-20 21:50:26 +01:00
Lofty 34804f3fb6 codeowners: adopt ABC9 and update intel_alm username 2022-06-20 15:02:50 +01:00
George Rennie 5dfad5101d chformal: Rename -coverprecond to -coverenable 2022-06-18 18:28:12 +01:00
Jannis Harder e39c422734 chformal: Test -coverprecond and reuse the src attribute 2022-06-18 18:19:26 +01:00
George Rennie c659bd1878 chformal: Add -coverprecond option
This inserts $cover cells to cover the enable signal (precondition)
for the selected formal cells.
2022-06-18 18:19:26 +01:00
github-actions[bot] 90147f5fbf Bump version 2022-06-18 00:17:32 +00:00
Archie 4542d51791 Adding testcase for issue 3374 2022-06-17 20:07:02 +01:00
Jannis Harder e6a5d84149
Merge pull request #3383 from jix/write_formal_map_roms
smt2, btor: Use memory_map -rom-only to make ROMs usable for k-induction
2022-06-17 19:08:14 +02:00
Jannis Harder 4adef63cd4 smt2, btor: Use memory_map -rom-only to make ROMs usable for k-induction
This avoids provability regressions now that we infer more ROMs.

This fixes #3378
2022-06-17 17:23:13 +02:00
Marcelina Kościelnicka ab3a9325c3 memory_map: Add -rom-only option. 2022-06-17 16:56:11 +02:00
Miodrag Milanović c23139fd98
Merge pull request #3382 from YosysHQ/micko/verific_extensions
use new verific extensions library
2022-06-17 16:20:31 +02:00
Miodrag Milanovic 607e957657 use new verific extensions library 2022-06-17 16:04:22 +02:00
Marcelina Kościelnicka 01daa077a2 memory_map: Use const drivers instead of FFs for ROMs. 2022-06-17 15:17:14 +02:00
github-actions[bot] bb634d39ef Bump version 2022-06-17 00:17:38 +00:00
Marcelina Kościelnicka d69091806a memory_libmap: Fix wrprio handling. 2022-06-17 02:09:37 +02:00
Marcelina Kościelnicka 25a4cd7020 memory_libmap: Fix params emitted for unused ports for consistency. 2022-06-16 08:14:08 +02:00
Archie b604c97b33 Add check for BLIF with no model name 2022-06-14 14:17:00 +01:00
github-actions[bot] 3046a06490 Bump version 2022-06-14 00:18:42 +00:00
Marcelina Kościelnicka 6b7efe12b7 Add a check for packed memory MEMID uniqueness 2022-06-13 19:23:55 +02:00
N. Engelhardt 3eaa9e38e0
Merge pull request #3196 from bfg86/bfg86/rename
Add -suffix option to rename -wire
2022-06-13 16:00:04 +02:00
Marcelina Kościelnicka 1ff0e1a58a opt_ffinv: Fix use after free. 2022-06-13 14:04:04 +02:00
Miodrag Milanovic ddc8044655 removed deprecated features code 2022-06-13 10:50:24 +02:00
bfg86 aedd3b7999 Updating help-text with nakengelhardts suggestion. 2022-06-13 09:35:10 +02:00
github-actions[bot] b15a46c2c0 Bump version 2022-06-11 00:17:13 +00:00
Jannis Harder 53b205c41d
Merge pull request #3368 from jix/smtbmc-unroll-noincr-traces-fix
smtbmc: noincr: keep solver running for post check-sat unrolling
2022-06-10 15:25:57 +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 d1cd24a457 Update manual 2022-06-10 15:00:07 +02:00
Miodrag Milanovic 1940bf647f Updated CHANGELOG 2022-06-10 09:08:23 +02:00
github-actions[bot] 47a99092af Bump version 2022-06-10 00:17:46 +00:00
N. Engelhardt b8ede6162b
Merge pull request #3349 from nakengelhardt/select_count_scratchpad
Make 'stat' and 'select -count' save counts to scratchpad
2022-06-09 17:15:02 +02:00
N. Engelhardt 871b277d35
Merge pull request #3359 from jix/fmcombine-memid
fmcombine: Add _gold/_gate suffix to memids
2022-06-09 17:12:34 +02:00
Henner Zeller 9c41b43191 Use compiler-generated default constructor for RTLIL::Const::Const
No need for a manual implementation.
While at it: have the constructor that takes a string take a
const string reference instead to avoid a copy.
2022-06-09 16:07:45 +01:00
Henner Zeller 9d41aa8e28 Avoid unnecessary copy of a potential large constant value.
The local variable is used just to iterate through the values, so
a const reference is all we need.
2022-06-09 16:05:51 +01:00
Miodrag Milanovic 6e8e4b4550 verific: Added "-vlog-libext" option to specify search extension for libraries 2022-06-09 08:57:48 +02:00
github-actions[bot] d1b2beab12 Bump version 2022-06-09 00:16:16 +00:00
Marcelina Kościelnicka 47efc04a7d wreduce: Introduce -mux_undef option (aligned with opt_expr). 2022-06-08 21:28:58 +02:00
Jannis Harder 0c5f62f6ff smtbmc: noincr: keep solver running for post check-sat unrolling 2022-06-08 13:20:25 +02:00
Jannis Harder 6db2948938
Merge pull request #3357 from jix/smtbmc-cvc5
smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5
2022-06-08 12:52:51 +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
Lofty aae2c01326 sta: warn on unrecognised cells only once 2022-06-08 09:31:49 +01:00
github-actions[bot] 4afb951283 Bump version 2022-06-08 00:15:24 +00:00
Jannis Harder d9bb10ba5f
Merge pull request #3367 from jix/smtlib2-module-fixes
smt2: emit smtlib2_comb_expr outputs after all inputs
2022-06-07 19:45:47 +02:00
Jannis Harder ac22f1764d smt2: emit smtlib2_comb_expr outputs after all inputs 2022-06-07 19:06:45 +02:00
Jannis Harder 5f9a97d234
Merge pull request #3319 from programmerjake/smtlib2-expr-support
add smtlib2_comb_expr
2022-06-07 16:47:10 +02:00
Jannis Harder fe048a48b3
Merge pull request #3358 from jix/smtbmc-yices-forall
smtbmc: Force nonincremental mode when yices is used with forall
2022-06-07 13:19:34 +02:00
Marcelina Kościelnicka d07828b409 opt_ffinv: Harden against simple ff/inv loop. 2022-06-07 08:20:06 +02:00
Marcelina Kościelnicka 9e8a2ac051 iopadmap: Fix z assignment removal.
Fixes #3360.
2022-06-07 04:10:50 +02:00
github-actions[bot] aa0b47c74a Bump version 2022-06-05 00:19:28 +00:00