| Commit message (Collapse) | Author | Age | Files | Lines | ||
|---|---|---|---|---|---|---|
| ... | ||||||
| * | 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 | |||||
| | * | Updated `yosys-smtbmc` to optionally dump raw bit strings, and fixed hole ↵ | Alberto Gonzalez | 2020-04-04 | 1 | -3/+15 | |
| | | | | | | | | | value recovery using that mode. | |||||
| * | | Support custom PROGRAM_PREFIX | Miodrag Milanovic | 2020-04-10 | 2 | -9/+8 | |
| | | | ||||||
| * | | kernel: big fat patch to use more ID::*, otherwise ID(*) | Eddie Hung | 2020-04-02 | 1 | -135/+135 | |
| | | | ||||||
| * | | kernel: use more ID::* | Eddie Hung | 2020-04-02 | 1 | -37/+37 | |
| | | | ||||||
| * | | Update `RTLIL::id2cstr()` usage to `log_id`. | Alberto Gonzalez | 2020-04-01 | 1 | -2/+2 | |
| |/ | ||||||
| * | Do not change solver output parsing for non-exists-forall problems. | Alberto Gonzalez | 2020-03-26 | 1 | -2/+6 | |
| | | ||||||
| * | Skip reading stdout from the solver that if it isn't a line reading only ↵ | Alberto Gonzalez | 2020-03-26 | 1 | -1/+3 | |
| | | | | | "sat", "unsat", or "unknown". | |||||
| * | Revert part of 0fda8308 from #1746 that broke other smtbmc flows | Claire Wolf | 2020-03-24 | 1 | -3/+1 | |
| | | | | | Signed-off-by: Claire Wolf <claire@symbioticeda.com> | |||||
| * | fix typo in `write_smt2` help | Teguh Hofstee | 2020-03-23 | 1 | -1/+1 | |
| | | ||||||
| * | Merge pull request #1768 from boqwxp/smt2_cleanup | N. Engelhardt | 2020-03-16 | 1 | -5/+5 | |
| |\ | | | | | Clean up pseudo-private member usage in `backends/smt2/smt2.cc`. | |||||
| | * | Clean up pseudo-private member usage in `backends/smt2/smt2.cc`. | Alberto Gonzalez | 2020-03-13 | 1 | -5/+5 | |
| | | | ||||||
| * | | Add support for optimizing exists-forall problems. | Alberto Gonzalez | 2020-03-13 | 3 | -1/+33 | |
| |/ | | | | | | Modifies smt2 backend to recognize `$anyconst` etc. assigned to a wire with the `maximize` or `minimize` attribute and emit `; yosys-smt2-maximize` or `; yosys-smt2-minimize` directives as appropriate. Modifies `backends/smt2/smtbmc.py` and `smtio.py` to recognize those directives and emit a `(maximize ...)` or `(minimize ...)` command at the end of `smt_forall_assert()`, as described in the paper "νZ - An Optimizing SMT Solver" by Nikolaj Bjørner et al. Adds an example `examples/smtbmc/demo9.v` to show how it can be used. | |||||
| * | Improve yosys-smtbmc "solver not found" handling | Claire Wolf | 2020-01-27 | 1 | -1/+5 | |
| | | | | | Signed-off-by: Claire Wolf <clifford@clifford.at> | |||||
| * | Bugfix in smtio vcd handling of $-identifiers | Clifford Wolf | 2019-10-23 | 1 | -6/+9 | |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | |||||
| * | Change smtbmc "Warmup failed" status to "PREUNSAT" | Clifford Wolf | 2019-10-03 | 1 | -14/+14 | |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | |||||
| * | backends: smt2: use $(CXX) variable for compiler | Sean Cross | 2019-09-08 | 1 | -1/+1 | |
| | | | | | | | | | | | | The Makefile assumes the compiler is called `gcc`, which isn't always true. In fact, if we're building on msys2 or msys2-64, the compiler is called `i686-w64-mingw32-g++` or `x86_64-w64-mingw32-g++`. Use the variable instead of hardcoding the name, to fix building on these systems. Signed-off-by: Sean Cross <sean@xobs.io> | |||||
| * | substr() -> compare() | Eddie Hung | 2019-08-07 | 1 | -1/+1 | |
| | | ||||||
| * | Make liberal use of IdString.in() | Eddie Hung | 2019-08-06 | 1 | -1/+1 | |
| | | ||||||
| * | Add $_NMUX_, add "abc -g cmos", add proper cmos cell costs | Clifford Wolf | 2019-08-06 | 1 | -0/+1 | |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | |||||
| * | smt: handle failure of setrlimit syscall | N. Engelhardt | 2019-07-15 | 1 | -1/+5 | |
| | | ||||||
| * | Escape scope names starting with dollar sign in smtio.py | Clifford Wolf | 2019-06-26 | 1 | -1/+4 | |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | |||||
| * | Add timescale and generated-by header to yosys-smtbmc MkVcd | Clifford Wolf | 2019-06-16 | 1 | -0/+2 | |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | |||||
| * | Add "whitebox" attribute, add "read_verilog -wb" | Clifford Wolf | 2019-04-18 | 1 | -1/+1 | |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | |||||
| * | Fix smtbmc.py handling of zero appended steps | Clifford Wolf | 2019-03-14 | 1 | -5/+5 | |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | |||||
| * | Install launcher executable when running yosys-smtbmc on Windows. | William D. Jones | 2019-03-13 | 1 | -1/+17 | |
| | | | | | Signed-off-by: William D. Jones <thor0505@comcast.net> | |||||
 |
index : iCE40/yosys | |
| [no description] |
| aboutsummaryrefslogtreecommitdiffstats |