aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2
Commit message (Collapse)AuthorAgeFilesLines
* smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFsJannis Harder2022-10-123-5/+22
| | | | | | | 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.
* smtbmc: Avoid unnecessary string copies when parsing solver outputJannis Harder2022-09-021-12/+9
|
* smtbmc: Set step range for --yw and dont skip steps for --check-witnessJannis Harder2022-08-161-2/+14
|
* yosys-witness: Add stats commandJannis Harder2022-08-161-0/+18
|
* smtbmc: Add --check-witness modeJannis Harder2022-08-161-1/+22
| | | | | This verifies that the given constraints force an assertion failure. This is useful to debug witness trace conversion (and minimization).
* aiger: Add yosys-witness supportJannis Harder2022-08-161-2/+148
| | | | | Adds a new json based aiger map file and yosys-witness converters to us this to convert between native and AIGER witness files.
* smtbmc: Add native json based witness format + smt2 backend supportJannis Harder2022-08-166-113/+968
| | | | | | | | | | | | | | | | | | | | 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.
* smt2: Support $anyinit cellsJannis Harder2022-08-161-10/+11
|
* formalff: Set new replaced_by_gclk attribute on removed dff's clksJannis Harder2022-08-161-0/+11
| | | | | | 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.
* Switched to utf-8 in smtio.pyMiodrag Milanovic2022-08-091-2/+2
|
* smt2: Fix $shift/$shiftx with negative shift ammountsJannis Harder2022-08-021-4/+4
| | | | Fixes #3431, fixes #3344
* smt2, btor: Revert calling memory_map -rom-onlyJannis Harder2022-06-291-1/+0
| | | | | | | | 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.)
* memory_map: -keepdc option for formalJannis Harder2022-06-271-1/+1
| | | | Use it when invoking memory_map -rom-only from write_{smt2,btor}.
* smt2, btor: Use memory_map -rom-only to make ROMs usable for k-inductionJannis Harder2022-06-171-0/+1
| | | | | | This avoids provability regressions now that we infer more ROMs. This fixes #3378
* smtbmc: noincr: keep solver running for post check-sat unrollingJannis Harder2022-06-081-2/+7
|
* Merge pull request #3357 from jix/smtbmc-cvc5Jannis Harder2022-06-081-3/+13
|\ | | | | smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5
| * smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5Jannis Harder2022-06-031-3/+13
| |
* | smt2: emit smtlib2_comb_expr outputs after all inputsJannis Harder2022-06-071-5/+9
| |
* | Merge pull request #3319 from programmerjake/smtlib2-expr-supportJannis Harder2022-06-071-6/+57
|\ \ | | | | | | add smtlib2_comb_expr
| * | smt2: Add smtlib2_comb_expr attribute to allow user-selected smtlib2 expressionsJacob Lifshay2022-06-021-6/+57
| |/
* / smtbmc: Force nonincremental mode when yices is used with forallJannis Harder2022-06-031-1/+4
|/
* add $divfloor support to write_smt2Jacob Lifshay2022-05-241-0/+21
| | | | Fixes: #3330
* smt2: Make write port array stores conditional on nonzero write maskJannis Harder2022-04-201-2/+4
|
* smtbmc: fix bmc with no assertionsJannis Harder2022-03-291-0/+2
| | | | this was broken by the `--keep-going` changes
* Merge pull request #3253 from jix/smtbmc-nodeepcopyJannis Harder2022-03-281-6/+6
|\ | | | | smtbmc: Avoid unnecessary deep copies during unrolling
| * smtbmc: Avoid unnecessary deep copies during unrollingJannis Harder2022-03-281-6/+6
| |
* | Merge pull request #3247 from jix/smtbmc-keepgoingJannis Harder2022-03-281-50/+143
|\ \ | |/ |/| smtbmc `--keep-going`
| * yosys-smtbmc: Option to keep going after failed assertions in BMC modeJannis Harder2022-03-241-48/+141
| |
| * yosys-smtbmc: Fix typo in help text, remove trailing whitespaceJannis Harder2022-03-241-2/+2
| |
* | ignore # comment linesN. Engelhardt2022-03-241-1/+1
|/
* Merge pull request #3186 from nakengelhardt/smtbmc_sby_print_idMiodrag Milanović2022-03-042-4/+12
|\ | | | | add argument for printing cell names in yosys-smtbmc
| * print cell name for properties in yosys-smtbmcN. Engelhardt2022-02-222-4/+12
| |
* | Add a bit of flexibilty re trace length when processing aiger witnesses in ↵Claire Xenia Wolf2022-02-111-1/+4
|/ | | | | | smtbmc.py Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
* Add $bmux and $demux cells.Marcelina Kościelnicka2022-01-281-0/+5
|
* Hook up $aldff support in various passes.Marcelina Kościelnicka2021-10-021-1/+1
|
* yosys-smtbmc: Fix reused loop variable.Marcelina Kościelnicka2021-09-101-4/+4
| | | | Fixes #2999.
* Add support for the Bitwuzla solverGCHQDeveloper5602021-07-121-5/+5
|
* Fixing old e-mail addresses and deadnamesClaire Xenia Wolf2021-06-083-3/+3
| | | | | | | | 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;
* Make a few passes auto-call Mem::narrow instead of rejecting wide ports.Marcelina Kościelnicka2021-05-281-6/+1
| | | | | | This essentially adds wide port support for free in passes that don't have a usefully better way of handling wide ports than just breaking them up to narrow ports, avoiding "please run memory_narrow" annoyance.
* Reject wide ports in some passes that will never support them.Marcelina Kościelnicka2021-05-251-0/+6
|
* kernel/rtlil: Extract some helpers for checking memory cell types.Marcelina Kościelnicka2021-05-221-2/+2
| | | | | | There will soon be more (versioned) memory cells, so handle passes that only care if a cell is memory-related by a simple helper call instead of a hardcoded list.
* btor, smt2, smv: Add a hint on how to deal with funny FF types.Marcelina Kościelnicka2021-02-251-0/+12
|
* smt2: Use Mem helper.Marcelina Kościelnicka2020-10-211-186/+244
|
* smtbmc: escape identifiers in verilog testbenchJakob Wenzel2020-10-061-11/+29
|
* use the new isPublic() in a few placesN. Engelhardt2020-09-141-2/+2
|
* write_smt2: fix SMT-LIB tutorial URLwhitequark2020-08-291-1/+1
|
* Ensure smt2 comments are associated with accessorsNoah Moroze2020-08-201-9/+20
|
* smtio: Emit `mode: start` options before `set-logic` command and any other ↵Alberto Gonzalez2020-07-201-1/+8
| | | | | | options after it. Refer to the SMT-LIB specification, section 4.1.7. According to the spec, some options can only be specified in `start` mode. Once the solver sees `set-logic`, it moves to `assert` mode.
* smtio: Add support for parsing `yosys-smt2-solver-option` info statements.Alberto Gonzalez2020-07-201-3/+10
|
* smt2: Add `-solver-option` option.Alberto Gonzalez2020-07-201-0/+13
|
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-04 20:28:28 +0000