aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2
Commit message (Expand)AuthorAgeFilesLines
* 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
* Add support for the Bitwuzla solverGCHQDeveloper5602021-07-121-5/+5
* Fixing old e-mail addresses and deadnamesClaire Xenia Wolf2021-06-083-3/+3
* Make a few passes auto-call Mem::narrow instead of rejecting wide ports.Marcelina Kościelnicka2021-05-281-6/+1
* 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
* 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 op...Alberto Gonzalez2020-07-201-1/+8
* 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
* Only allow "sat" and "unsat" smt solver responses in yosys-smtbmcClaire Wolf2020-07-202-4/+4
* Use C++11 final/override keywords.whitequark2020-06-181-2/+2
* more reasonable numbers for memoryYehowshua Immanuel2020-06-041-1/+1
* MacOS has even stricter stack limits in catalina.Yehowshua Immanuel2020-06-041-1/+1
* Merge pull request #2018 from boqwxp/qbfsat-timeoutclairexen2020-05-302-5/+31
|\
| * smtbmc: Remove superfluous `yosys-smt2-timeout` file macro.Alberto Gonzalez2020-05-291-4/+0
| * smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, a...Alberto Gonzalez2020-05-252-5/+35
* | Merge pull request #1885 from Xiretza/mod-rem-cellsclairexen2020-05-291-0/+10
|\ \ | |/ |/|
| * Add flooring modulo operatorXiretza2020-05-281-0/+10
* | qbfsat: Move SMT2 info statements back to the top of the file.Alberto Gonzalez2020-05-251-3/+3
* | qbfsat: Add `-solver` option and allow choice of Z3 or Yices, making Yices th...Alberto Gonzalez2020-05-251-3/+7
|/
* smtbmc: Fix typo in error message.Alberto Gonzalez2020-05-191-1/+1
* smtbmc: Fix return status handling.Alberto Gonzalez2020-05-141-2/+2
* Merge pull request #1830 from boqwxp/qbfsatN. Engelhardt2020-04-151-3/+15
|\
| * Updated `yosys-smtbmc` to optionally dump raw bit strings, and fixed hole val...Alberto Gonzalez2020-04-041-3/+15
* | Support custom PROGRAM_PREFIXMiodrag Milanovic2020-04-102-9/+8
* | kernel: big fat patch to use more ID::*, otherwise ID(*)Eddie Hung2020-04-021-135/+135
* | kernel: use more ID::*Eddie Hung2020-04-021-37/+37
* | Update `RTLIL::id2cstr()` usage to `log_id`.Alberto Gonzalez2020-04-011-2/+2
|/
* Do not change solver output parsing for non-exists-forall problems.Alberto Gonzalez2020-03-261-2/+6
* Skip reading stdout from the solver that if it isn't a line reading only "sat...Alberto Gonzalez2020-03-261-1/+3
* Revert part of 0fda8308 from #1746 that broke other smtbmc flowsClaire Wolf2020-03-241-3/+1
* fix typo in `write_smt2` helpTeguh Hofstee2020-03-231-1/+1
* Merge pull request #1768 from boqwxp/smt2_cleanupN. Engelhardt2020-03-161-5/+5
|\
| * Clean up pseudo-private member usage in `backends/smt2/smt2.cc`.Alberto Gonzalez2020-03-131-5/+5
* | Add support for optimizing exists-forall problems.Alberto Gonzalez2020-03-133-1/+33
|/
* Improve yosys-smtbmc "solver not found" handlingClaire Wolf2020-01-271-1/+5
* Bugfix in smtio vcd handling of $-identifiersClifford Wolf2019-10-231-6/+9
* Change smtbmc "Warmup failed" status to "PREUNSAT"Clifford Wolf2019-10-031-14/+14
* backends: smt2: use $(CXX) variable for compilerSean Cross2019-09-081-1/+1
* substr() -> compare()Eddie Hung2019-08-071-1/+1
* Make liberal use of IdString.in()Eddie Hung2019-08-061-1/+1
* Add $_NMUX_, add "abc -g cmos", add proper cmos cell costsClifford Wolf2019-08-061-0/+1
* smt: handle failure of setrlimit syscallN. Engelhardt2019-07-151-1/+5