| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | smtbmc: noincr: keep solver running for post check-sat unrolling | Jannis Harder | 2022-06-08 | 1 | -2/+7 |
| | | |||||
| * | Merge pull request #3357 from jix/smtbmc-cvc5 | Jannis Harder | 2022-06-08 | 1 | -3/+13 |
| |\ | | | | | smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5 | ||||
| | * | smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5 | Jannis Harder | 2022-06-03 | 1 | -3/+13 |
| | | | |||||
| * | | smt2: emit smtlib2_comb_expr outputs after all inputs | Jannis Harder | 2022-06-07 | 1 | -5/+9 |
| | | | |||||
| * | | Merge pull request #3319 from programmerjake/smtlib2-expr-support | Jannis Harder | 2022-06-07 | 1 | -6/+57 |
| |\ \ | | | | | | | add smtlib2_comb_expr | ||||
| | * | | smt2: Add smtlib2_comb_expr attribute to allow user-selected smtlib2 expressions | Jacob Lifshay | 2022-06-02 | 1 | -6/+57 |
| | |/ | |||||
| * / | smtbmc: Force nonincremental mode when yices is used with forall | Jannis Harder | 2022-06-03 | 1 | -1/+4 |
| |/ | |||||
| * | add $divfloor support to write_smt2 | Jacob Lifshay | 2022-05-24 | 1 | -0/+21 |
| | | | | | Fixes: #3330 | ||||
| * | smt2: Make write port array stores conditional on nonzero write mask | Jannis Harder | 2022-04-20 | 1 | -2/+4 |
| | | |||||
| * | smtbmc: fix bmc with no assertions | Jannis Harder | 2022-03-29 | 1 | -0/+2 |
| | | | | | this was broken by the `--keep-going` changes | ||||
| * | Merge pull request #3253 from jix/smtbmc-nodeepcopy | Jannis Harder | 2022-03-28 | 1 | -6/+6 |
| |\ | | | | | smtbmc: Avoid unnecessary deep copies during unrolling | ||||
| | * | smtbmc: Avoid unnecessary deep copies during unrolling | Jannis Harder | 2022-03-28 | 1 | -6/+6 |
| | | | |||||
| * | | Merge pull request #3247 from jix/smtbmc-keepgoing | Jannis Harder | 2022-03-28 | 1 | -50/+143 |
| |\ \ | |/ |/| | smtbmc `--keep-going` | ||||
| | * | yosys-smtbmc: Option to keep going after failed assertions in BMC mode | Jannis Harder | 2022-03-24 | 1 | -48/+141 |
| | | | |||||
| | * | yosys-smtbmc: Fix typo in help text, remove trailing whitespace | Jannis Harder | 2022-03-24 | 1 | -2/+2 |
| | | | |||||
| * | | ignore # comment lines | N. Engelhardt | 2022-03-24 | 1 | -1/+1 |
| |/ | |||||
| * | Merge pull request #3186 from nakengelhardt/smtbmc_sby_print_id | Miodrag Milanović | 2022-03-04 | 2 | -4/+12 |
| |\ | | | | | add argument for printing cell names in yosys-smtbmc | ||||
| | * | print cell name for properties in yosys-smtbmc | N. Engelhardt | 2022-02-22 | 2 | -4/+12 |
| | | | |||||
| * | | Add a bit of flexibilty re trace length when processing aiger witnesses in ↵ | Claire Xenia Wolf | 2022-02-11 | 1 | -1/+4 |
| |/ | | | | | | smtbmc.py Signed-off-by: Claire Xenia Wolf <claire@clairexen.net> | ||||
| * | Add $bmux and $demux cells. | Marcelina Kościelnicka | 2022-01-28 | 1 | -0/+5 |
| | | |||||
| * | Hook up $aldff support in various passes. | Marcelina Kościelnicka | 2021-10-02 | 1 | -1/+1 |
| | | |||||
| * | yosys-smtbmc: Fix reused loop variable. | Marcelina Kościelnicka | 2021-09-10 | 1 | -4/+4 |
| | | | | | Fixes #2999. | ||||
| * | Add support for the Bitwuzla solver | GCHQDeveloper560 | 2021-07-12 | 1 | -5/+5 |
| | | |||||
| * | Fixing old e-mail addresses and deadnames | Claire Xenia Wolf | 2021-06-08 | 3 | -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ścielnicka | 2021-05-28 | 1 | -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ścielnicka | 2021-05-25 | 1 | -0/+6 |
| | | |||||
| * | kernel/rtlil: Extract some helpers for checking memory cell types. | Marcelina Kościelnicka | 2021-05-22 | 1 | -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ścielnicka | 2021-02-25 | 1 | -0/+12 |
| | | |||||
| * | smt2: Use Mem helper. | Marcelina Kościelnicka | 2020-10-21 | 1 | -186/+244 |
| | | |||||
| * | smtbmc: escape identifiers in verilog testbench | Jakob Wenzel | 2020-10-06 | 1 | -11/+29 |
| | | |||||
| * | use the new isPublic() in a few places | N. Engelhardt | 2020-09-14 | 1 | -2/+2 |
| | | |||||
| * | write_smt2: fix SMT-LIB tutorial URL | whitequark | 2020-08-29 | 1 | -1/+1 |
| | | |||||
| * | Ensure smt2 comments are associated with accessors | Noah Moroze | 2020-08-20 | 1 | -9/+20 |
| | | |||||
| * | smtio: Emit `mode: start` options before `set-logic` command and any other ↵ | Alberto Gonzalez | 2020-07-20 | 1 | -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 Gonzalez | 2020-07-20 | 1 | -3/+10 |
| | | |||||
| * | smt2: Add `-solver-option` option. | Alberto Gonzalez | 2020-07-20 | 1 | -0/+13 |
| | | |||||
| * | Only allow "sat" and "unsat" smt solver responses in yosys-smtbmc | Claire Wolf | 2020-07-20 | 2 | -4/+4 |
| | | | | | Signed-off-by: Claire Wolf <claire@symbioticeda.com> | ||||
| * | Use C++11 final/override keywords. | whitequark | 2020-06-18 | 1 | -2/+2 |
| | | |||||
| * | more reasonable numbers for memory | Yehowshua Immanuel | 2020-06-04 | 1 | -1/+1 |
| | | |||||
| * | MacOS has even stricter stack limits in catalina. | Yehowshua Immanuel | 2020-06-04 | 1 | -1/+1 |
| | | | | Invoking sby in macOS Catalina fails because of bizarre stack limits in Catalina. | ||||
| * | Merge pull request #2018 from boqwxp/qbfsat-timeout | clairexen | 2020-05-30 | 2 | -5/+31 |
| |\ | | | | | smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, and CVC4. | ||||
| | * | smtbmc: Remove superfluous `yosys-smt2-timeout` file macro. | Alberto Gonzalez | 2020-05-29 | 1 | -4/+0 |
| | | | | | | | | | Co-Authored-By: clairexen <claire@symbioticeda.com> | ||||
| | * | smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, ↵ | Alberto Gonzalez | 2020-05-25 | 2 | -5/+35 |
| | | | | | | | | | and CVC4. | ||||
| * | | Merge pull request #1885 from Xiretza/mod-rem-cells | clairexen | 2020-05-29 | 1 | -0/+10 |
| |\ \ | |/ |/| | Fix modulo/remainder semantics | ||||
| | * | Add flooring modulo operator | Xiretza | 2020-05-28 | 1 | -0/+10 |
| | | | | | | | | | | | | | | | | | | | | | | | The $div and $mod cells use truncating division semantics (rounding towards 0), as defined by e.g. Verilog. Another rounding mode, flooring (rounding towards negative infinity), can be used in e.g. VHDL. The new $modfloor cell provides this flooring modulo (also known as "remainder" in several languages, but this name is ambiguous). This commit also fixes the handling of $mod in opt_expr, which was previously optimized as if it was $modfloor. | ||||
| * | | qbfsat: Move SMT2 info statements back to the top of the file. | Alberto Gonzalez | 2020-05-25 | 1 | -3/+3 |
| | | | |||||
| * | | qbfsat: Add `-solver` option and allow choice of Z3 or Yices, making Yices ↵ | Alberto Gonzalez | 2020-05-25 | 1 | -3/+7 |
| |/ | | | | | | the default. Ensures that "BV" is the logic whenever solving an exists-forall problem with Yices, moves the "(set-logic ...)" directive above any non-info line, sets the `ef-max-iters` parameter to a very high number when using Yices in exists-forall mode so as not to prematurely abandon difficult problems, and does not provide the incompatible "--incremental" Yices argument when in exists-forall mode. | ||||
| * | smtbmc: Fix typo in error message. | Alberto Gonzalez | 2020-05-19 | 1 | -1/+1 |
| | | | | | Co-Authored-By: N. Engelhardt <nak@symbioticeda.com> | ||||
| * | smtbmc: Fix return status handling. | Alberto Gonzalez | 2020-05-14 | 1 | -2/+2 |
| | | |||||
| * | Merge pull request #1830 from boqwxp/qbfsat | N. Engelhardt | 2020-04-15 | 1 | -3/+15 |
| |\ | | | | | Add `qbfsat` command to integrate exists-forall solving and specialization | ||||
 |
index : iCE40/yosys | |
| [no description] |
| aboutsummaryrefslogtreecommitdiffstats |