| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Add missing blackslash-to-slash convertion to smtio.py (matching ↵ | Clifford Wolf | 2019-02-06 | 1 | -1/+1 |
| | | | | | | | Smt2Worker::get_id() behavior) Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Merge pull request #693 from YosysHQ/rlimit | Clifford Wolf | 2018-11-07 | 1 | -8/+11 |
| |\ | | | | | improve rlimit handling in smtio.py | ||||
| | * | Limit stack size to 16 MB on Darwin | Clifford Wolf | 2018-11-07 | 1 | -1/+4 |
| | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| | * | Fix for improved smtio.py rlimit code | Clifford Wolf | 2018-11-06 | 1 | -1/+1 |
| | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| | * | Improve stack rlimit code in smtio.py | Clifford Wolf | 2018-11-06 | 1 | -8/+8 |
| | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | | Run solver in non-incremental mode whem smtio.py is configured for ↵ | Clifford Wolf | 2018-11-06 | 1 | -3/+12 |
| |/ | | | | | | non-incremental solving Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Use conservative stack size for SMT2 on MacOS | Arjen Roodselaar | 2018-11-04 | 1 | -1/+6 |
| | | |||||
| * | Gate POSIX-only signals and resource module to only run on POSIX Python ↵ | William D. Jones | 2018-07-06 | 1 | -9/+12 |
| | | | | | implementations. | ||||
| * | Add smtio.py support for parsing SMT2 (_ bvX n) syntax for BitVec constants | Clifford Wolf | 2018-04-04 | 1 | -0/+3 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Add smtio status msgs when --progress is inactive | Clifford Wolf | 2018-03-29 | 1 | -2/+23 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Bugfix in smtio.py VCD file generator | Clifford Wolf | 2018-03-29 | 1 | -1/+1 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Improve yosys-smtbmc log output and error handling | Clifford Wolf | 2018-03-17 | 1 | -5/+14 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Improve handling of invalid check-sat result in smtio.py | Clifford Wolf | 2018-03-17 | 1 | -1/+2 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Remove debug prints from yosys-smtbmc VCD writer | Clifford Wolf | 2018-03-08 | 1 | -2/+0 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Check results of (check-sat) in yosys-smtbmc | Clifford Wolf | 2018-03-07 | 1 | -0/+2 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Imporove yosys-smtbmc error handling, Improve VCD output | Clifford Wolf | 2018-03-05 | 1 | -20/+43 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Fix a hangup in yosys-smtbmc error handling | Clifford Wolf | 2018-03-04 | 1 | -3/+5 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Improved error handling in yosys-smtbmc | Clifford Wolf | 2018-03-03 | 1 | -1/+3 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Terminate running SMT solver when smtbmc is terminated | Clifford Wolf | 2018-03-03 | 1 | -1/+31 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Mangle names with square brackets in VCD files to work around issues in gtkwave | Clifford Wolf | 2018-03-01 | 1 | -2/+8 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Add smtbmc support for exist-forall problems | Clifford Wolf | 2018-02-23 | 1 | -4/+53 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Add support for mockup clock signals in yosys-smtbmc vcd output | Clifford Wolf | 2018-02-20 | 1 | -2/+49 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Fix smtio.py for large SMT2 S-expressions | Clifford Wolf | 2018-01-29 | 1 | -1/+12 |
| | | |||||
| * | Move user-provided smt2 info stmts to the top of the yosys-smtbmc smt2 output | Clifford Wolf | 2018-01-18 | 1 | -3/+3 |
| | | |||||
| * | Add yosys-smtbmc VCD writer support for memories with async writes | Clifford Wolf | 2017-12-14 | 1 | -1/+1 |
| | | |||||
| * | Improve smtio performance by using reader thread, not writer thread | Clifford Wolf | 2017-10-26 | 1 | -10/+30 |
| | | |||||
| * | Use separate writer thread for talking to SMT solver to avoid read/write ↵ | Clifford Wolf | 2017-10-25 | 1 | -8/+23 |
| | | | | | deadlock | ||||
| * | Improve p_* functions in smtio.py | Clifford Wolf | 2017-10-25 | 1 | -21/+19 |
| | | |||||
| * | Capsulate smt-solver read/write in separate functions | Clifford Wolf | 2017-10-25 | 1 | -8/+24 |
| | | |||||
| * | Fix generation of vlogtb output in yosys-smtbmc for "rand reg" and "rand ↵ | Clifford Wolf | 2017-06-07 | 1 | -1/+30 |
| | | | | | const reg" | ||||
| * | Change default smt2 solver to yices (Yices 2 has switched its license to GPL) | Clifford Wolf | 2017-05-27 | 1 | -4/+4 |
| | | |||||
| * | Fix boolector support in yosys-smtbmc | Clifford Wolf | 2017-05-08 | 1 | -18/+18 |
| | | |||||
| * | Add "write_smt2 -stdt" mode | Clifford Wolf | 2017-03-20 | 1 | -28/+37 |
| | | |||||
| * | Improve smt2 encodings of assert/assume/cover, better wire_smt2 help msg | Clifford Wolf | 2017-03-04 | 1 | -2/+2 |
| | | |||||
| * | Fix bug in smtio unroll code | Clifford Wolf | 2017-02-26 | 1 | -3/+2 |
| | | |||||
| * | Improve (and fix for stbv mode) SMT2 memory API | Clifford Wolf | 2017-02-26 | 1 | -3/+3 |
| | | |||||
| * | Add "write_smt2 -stbv" | Clifford Wolf | 2017-02-24 | 1 | -1/+1 |
| | | |||||
| * | Add "yosys-smtbmc -S <opt>" | Clifford Wolf | 2017-02-19 | 1 | -7/+18 |
| | | |||||
| * | Partially implement cover() support in yosys-smtbmc | Clifford Wolf | 2017-02-04 | 1 | -0/+4 |
| | | |||||
| * | Add "yosys-smtbmc --aig-noheader" and AIGER mem init support | Clifford Wolf | 2017-01-28 | 1 | -2/+22 |
| | | |||||
| * | Implicitly set "yosys-smtbmc --noprogress" on windows | Clifford Wolf | 2017-01-04 | 1 | -3/+4 |
| | | |||||
| * | Fixed "yosys-smtbmc --noprogress" | Clifford Wolf | 2017-01-04 | 1 | -1/+1 |
| | | |||||
| * | Removed shebang line from smtio.py, fixes #279 | Clifford Wolf | 2016-11-27 | 1 | -1/+0 |
| | | |||||
| * | Merge branch 'master' of github.com:cliffordwolf/yosys | Clifford Wolf | 2016-10-11 | 1 | -0/+2 |
| |\ | |||||
| | * | Added smtc support for top-level state with [], [N:] syntax | Clifford Wolf | 2016-10-08 | 1 | -0/+2 |
| | | | |||||
| * | | Bugfix in yosys-smtbmc --noincr | Clifford Wolf | 2016-10-04 | 1 | -1/+8 |
| |/ | |||||
| * | yosys-smtbmc: ABC is a QF_BV solver | Clifford Wolf | 2016-10-03 | 1 | -0/+1 |
| | | |||||
| * | Added "yosys-smtbmc --noincr" | Clifford Wolf | 2016-10-03 | 1 | -10/+39 |
| | | |||||
| * | yosys-smtbmc: added smtc [...] support for cells | Clifford Wolf | 2016-10-02 | 1 | -0/+2 |
| | | |||||
| * | Added "yosys-smtbmc -s abc" | Clifford Wolf | 2016-10-01 | 1 | -0/+4 |
| | | |||||
 |
index : iCE40/yosys | |
| [no description] |
| aboutsummaryrefslogtreecommitdiffstats |