mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-06-06 17:11:01 +00:00
Code Activity
17279 commits 132 branches 68 tags 60 MiB
Commit graph

332 commits

Author SHA1 Message Date
Jannis Harder
62afe61779 smt2: Directly implement bwmux instead of using bwmuxmap 2023-01-11 18:07:16 +01:00
Jannis Harder
be752a20dc Add bwmuxmap pass 2022-11-30 18:50:53 +01:00
Emil J
15d41041d8
Merge branch 'YosysHQ:master' into master 2022-11-08 22:02:23 +01:00
Emil J
6936394eed
Merge branch 'YosysHQ:master' into master 2022-10-20 19:36:03 +02:00
Emil Jiří Tywoniak
2ba435b6bc bugfix for mathsat counterexample vcd dump 2022-10-20 19:31:16 +02:00
Jannis Harder
96029400cb smtbmc: Do not assume skipped assertions when loading a witness trace 
This is not valid when the prefix of a trace already violates
assertions. This can happen when the trace generating solver doesn't
look for a minimal length counterexample.
 2022-10-20 13:49:47 +02:00
Emil J
8859d801c8
Temporal induction counterexample loop detection (#3504) 
I have added an optional flag to smtbmc that causes failed temporal induction counterexample traces to be checked for duplicate states and reported to the user, since loops in the counterexample mean that increasing the induction depth won't help prove a design's safety properties.
 2022-10-19 12:20:12 +02:00
Emil Jiří Tywoniak
083ca6ab06 bugfix 2022-10-18 22:58:54 +02:00
Jannis Harder
8838b1eaa4 smtbmc: Fix witness handling for k-induction failures 
The "uninitialized" value is a _list_ of chunks that are part of the
initial state for the witness trace.
 2022-10-18 19:51:36 +02:00
Jannis Harder
4d334fd3e3 smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFs 
The witness metadata was missing fine grained FFs completely and for
coarse grained FFs where the output connection has multiple chunks it
lacked the offset of the chunk within the SMT expression. This fixes
both, the later by adding an "smtoffset" field to the metadata.
 2022-10-12 19:48:36 +02:00
Emil Jiří Tywoniak
8d4000a9b7 include memory in state 2022-10-11 19:52:44 +02:00
Emil Jiří Tywoniak
0dbebea939 include memory in state 2022-10-11 19:48:16 +02:00
Emil Jiří Tywoniak
3e816e9922 experimental temporal induction counterexample loop detection 2022-10-09 18:24:43 +02:00
Jannis Harder
1d40f5e8fa smtbmc: Avoid unnecessary string copies when parsing solver output 2022-09-02 22:37:08 +02:00
Jannis Harder
66f761a8c5 smtbmc: Set step range for --yw and dont skip steps for --check-witness 2022-08-16 13:37:30 +02:00
Jannis Harder
b156fe903f yosys-witness: Add stats command 2022-08-16 13:37:30 +02:00
Jannis Harder
475267ac25 smtbmc: Add --check-witness mode 
This verifies that the given constraints force an assertion failure.
This is useful to debug witness trace conversion (and minimization).
 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
021c3c8da5 smt2: Support $anyinit cells 2022-08-16 13:37:30 +02:00
Jannis Harder
a5e1d3b997 formalff: Set new replaced_by_gclk attribute on removed dff's clks 
This attribute can be used by formal backends to indicate which clocks
were mapped to the global clock. Update the btor and smt2 backend which
already handle clock inputs to understand this attribute.
 2022-08-16 13:37:30 +02:00
Miodrag Milanovic
4444d5cf68 Switched to utf-8 in smtio.py 2022-08-09 12:54:48 +02:00
Jannis Harder
6af5e74f95 smt2: Fix $shift/$shiftx with negative shift ammounts 
Fixes #3431, fixes #3344
 2022-08-02 20:16:41 +02:00
Jannis Harder
930bcf0e75 smt2, btor: Revert calling memory_map -rom-only 
This approach had major issues with ROMs whose initialization was not
fully defined. If required, memory_map -rom-only -keepdc should be
called early in a formal flow instead. (This does require a careful
choice of optimization passes though. Sby's scripts will be updated
accordingly.)
 2022-06-29 18:28:34 +02:00
Jannis Harder
d78d807a7f memory_map: -keepdc option for formal 
Use it when invoking memory_map -rom-only from write_{smt2,btor}.
 2022-06-27 15:47:55 +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
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
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
ab9e887dee smtbmc: Force nonincremental mode when yices is used with forall 2022-06-03 16:45:23 +02:00
Jannis Harder
0207d7b0cf smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5 2022-06-03 16:24:09 +02:00
Jacob Lifshay
cd57c5adb3 smt2: Add smtlib2_comb_expr attribute to allow user-selected smtlib2 expressions 2022-06-02 22:37:29 -07:00
Jacob Lifshay
d53479a0d6 add $divfloor support to write_smt2 
Fixes: #3330
 2022-05-24 01:34:25 -07:00
Jannis Harder
c7ef0f2932 smt2: Make write port array stores conditional on nonzero write mask 2022-04-20 17:49:48 +02:00
Jannis Harder
8b15f3a548 smtbmc: fix bmc with no assertions 
this was broken by the `--keep-going` changes
 2022-03-29 20:41:50 +02:00
Jannis Harder
8cc8c5efde
Merge pull request #3253 from jix/smtbmc-nodeepcopy 
smtbmc: Avoid unnecessary deep copies during unrolling
 2022-03-28 16:59:26 +02:00
Jannis Harder
17e2a3048c
Merge pull request #3247 from jix/smtbmc-keepgoing 
smtbmc `--keep-going`
 2022-03-28 16:58:41 +02:00
Jannis Harder
d25daa6203 smtbmc: Avoid unnecessary deep copies during unrolling 2022-03-28 13:03:48 +02:00
Jannis Harder
5e4d804e53 yosys-smtbmc: Option to keep going after failed assertions in BMC mode 2022-03-24 16:01:14 +01:00
Jannis Harder
e43ebf8527 yosys-smtbmc: Fix typo in help text, remove trailing whitespace 2022-03-24 16:01:14 +01:00
N. Engelhardt
a7ee01065a ignore # comment lines 2022-03-24 10:19:17 +01:00
Miodrag Milanović
a95e5d505b
Merge pull request #3186 from nakengelhardt/smtbmc_sby_print_id 
add argument for printing cell names in yosys-smtbmc
 2022-03-04 16:39:12 +01:00
N. Engelhardt
dc739362c7 print cell name for properties in yosys-smtbmc 2022-02-22 17:00:10 +01:00
Claire Xenia Wolf
30eb7f8665 Add a bit of flexibilty re trace length when processing aiger witnesses in smtbmc.py 
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
 2022-02-11 17:24:49 +01:00
Marcelina Kościelnicka
93508d58da Add $bmux and $demux cells. 2022-01-28 23:34:41 +01:00
Marcelina Kościelnicka
e7d89e653c Hook up $aldff support in various passes. 2021-10-02 21:01:21 +02:00
Marcelina Kościelnicka
33749f1e3a yosys-smtbmc: Fix reused loop variable. 
Fixes #2999.
 2021-09-10 13:34:58 +02:00
GCHQDeveloper560
4379375d89 Add support for the Bitwuzla solver 2021-07-12 22:07:58 +02:00
Claire Xenia Wolf
72787f52fc Fixing old e-mail addresses and deadnames 
s/((Claire|Xen|Xenia|Clifford)\s+)+(Wolf|Xen)\s+<(claire|clifford)@(symbioticeda.com|clifford.at|yosyshq.com)>/Claire Xenia Wolf <claire@yosyshq.com>/gi;
s/((Nina|Nak|N\.)\s+)+Engelhardt\s+<nak@(symbioticeda.com|yosyshq.com)>/N. Engelhardt <nak@yosyshq.com>/gi;
s/((David)\s+)+Shah\s+<(dave|david)@(symbioticeda.com|yosyshq.com|ds0.me)>/David Shah <dave@ds0.me>/gi;
s/((Miodrag)\s+)+Milanovic\s+<(miodrag|micko)@(symbioticeda.com|yosyshq.com)>/Miodrag Milanovic <micko@yosyshq.com>/gi;
s,https?://www.clifford.at/yosys/,http://yosyshq.net/yosys/,g;
 2021-06-08 00:39:36 +02:00