| Commit message (Collapse) | Author | Age | Files | Lines | ||
|---|---|---|---|---|---|---|
| ... | ||||||
| * | 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 | 2 | -23/+49 | |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | |||||
| * | Improve SMT2 encoding of $reduce_{and,or,bool} | Clifford Wolf | 2018-03-04 | 1 | -1/+9 | |
| | | | | | 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> | |||||
| * | Fix smtbmc smtc/aiw parser for wire names containing [] | Clifford Wolf | 2018-03-03 | 1 | -1/+1 | |
| | | | | | 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> | |||||
| * | Small fixes and improvements in $allconst/$allseq handling | Clifford Wolf | 2018-02-26 | 1 | -12/+18 | |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | |||||
| * | Add smtbmc support for exist-forall problems | Clifford Wolf | 2018-02-23 | 3 | -87/+334 | |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | |||||
| * | Add support for mockup clock signals in yosys-smtbmc vcd output | Clifford Wolf | 2018-02-20 | 3 | -6/+111 | |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | |||||
| * | Fix handling of zero-length cell connections in SMT2 back-end | Clifford Wolf | 2018-02-08 | 1 | -0/+8 | |
| | | | | | 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 | 3 | -7/+11 | |
| | | ||||||
| * | Add smt2 back-end support for async write memories | Clifford Wolf | 2017-12-14 | 1 | -14/+53 | |
| | | ||||||
| * | Fixed "yosys-smtbmc -g" handling of no solution | Clifford Wolf | 2017-11-27 | 1 | -1/+1 | |
| | | ||||||
| * | Fix SMT2 handling of initstate in sub-modules | Clifford Wolf | 2017-10-29 | 1 | -0/+3 | |
| | | ||||||
| * | 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 a bug in yosys-smtbmc in ROM handling | Clifford Wolf | 2017-10-25 | 1 | -0/+3 | |
| | | ||||||
| * | Fix bug in write_smt2 (export logic driving hierarchical cells before ↵ | Clifford Wolf | 2017-08-25 | 1 | -34/+34 | |
| | | | | | exporting regs) | |||||
| * | Add "yosys-smtbmc --smtc-init --smtc-top --noinit" | Clifford Wolf | 2017-08-04 | 1 | -20/+66 | |
| | | ||||||
| * | Add verilator support to testbenches generated by yosys-smtbmc | Clifford Wolf | 2017-07-21 | 1 | -3/+15 | |
| | | ||||||
| * | Generate FSM-style testbenches in smtbmc | Clifford Wolf | 2017-07-12 | 1 | -5/+23 | |
| | | ||||||
| * | Change s/asserts/assertions/ in yosys-smtbmc log messages | Clifford Wolf | 2017-07-07 | 1 | -2/+2 | |
| | | ||||||
| * | Add "yosys-smtbmc --presat" | Clifford Wolf | 2017-07-07 | 1 | -3/+23 | |
| | | ||||||
| * | Remove unneeded delays in smtbmc vlogtb | Clifford Wolf | 2017-07-03 | 1 | -1/+1 | |
| | | ||||||
| * | Add "yosys-smtbmc --vlogtb-top" | Clifford Wolf | 2017-07-01 | 1 | -15/+32 | |
| | | ||||||
| * | Fix smtbmc vlogtb bug in $anyseq handling | Clifford Wolf | 2017-07-01 | 1 | -3/+3 | |
| | | ||||||
| * | Fix generation of vlogtb output in yosys-smtbmc for "rand reg" and "rand ↵ | Clifford Wolf | 2017-06-07 | 3 | -4/+53 | |
| | | | | | const reg" | |||||
| * | Change default smt2 solver to yices (Yices 2 has switched its license to GPL) | Clifford Wolf | 2017-05-27 | 1 | -4/+4 | |
| | | ||||||
| * | Add $_ANDNOT_ and $_ORNOT_ gates | Clifford Wolf | 2017-05-17 | 1 | -0/+2 | |
| | | ||||||
| * | Fix boolector support in yosys-smtbmc | Clifford Wolf | 2017-05-08 | 1 | -18/+18 | |
| | | ||||||
| * | Add "write_smt2 -stdt" mode | Clifford Wolf | 2017-03-20 | 2 | -37/+84 | |
| | | ||||||
| * | Improve smt2 encodings of assert/assume/cover, better wire_smt2 help msg | Clifford Wolf | 2017-03-04 | 2 | -33/+87 | |
| | | ||||||
| * | Use hex addresses in smtbmc vcd mem traces | Clifford Wolf | 2017-02-28 | 1 | -1/+1 | |
| | | ||||||
| * | Add smtbmc support for memory vcd dumping | Clifford Wolf | 2017-02-26 | 1 | -0/+98 | |
| | | ||||||
| * | Fix extra newline bug in write_smt2 | Clifford Wolf | 2017-02-26 | 1 | -1/+1 | |
| | | ||||||
| * | Fix bug in smtio unroll code | Clifford Wolf | 2017-02-26 | 1 | -3/+2 | |
| | | ||||||
| * | Fix assert checking in "yosys-smtbmc -c --append" | Clifford Wolf | 2017-02-26 | 1 | -1/+1 | |
| | | ||||||
| * | Improve (and fix for stbv mode) SMT2 memory API | Clifford Wolf | 2017-02-26 | 3 | -47/+51 | |
| | | ||||||
| * | Add support for "yosys-smtbmc -c --append" | Clifford Wolf | 2017-02-25 | 1 | -1/+13 | |
| | | ||||||
| * | Add "write_smt2 -stbv" | Clifford Wolf | 2017-02-24 | 3 | -49/+179 | |
| | | ||||||
| * | Add SMT2 statebv mode (inactive for now) | Clifford Wolf | 2017-02-24 | 1 | -20/+47 | |
| | | ||||||
| * | Add "yosys-smtbmc -S <opt>" | Clifford Wolf | 2017-02-19 | 1 | -7/+18 | |
| | | ||||||
| * | Add assert check in "yosys-smtbmc -c" | Clifford Wolf | 2017-02-04 | 1 | -7/+28 | |
| | | ||||||
 |
index : iCE40/yosys | |
| [no description] |
| aboutsummaryrefslogtreecommitdiffstats |