| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | 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> | ||||
| * | Fixed gcc 7.2 "statement will never be executed" warning | Clifford Wolf | 2018-02-03 | 1 | -1/+1 |
| | | |||||
| * | 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 "no driver for signal bit" error msg to btor back-end | Clifford Wolf | 2017-12-24 | 1 | -0/+2 |
| | | |||||
| * | Simple fix BTOR memory encoding | Clifford Wolf | 2017-12-17 | 1 | -2/+2 |
| | | |||||
| * | Improve BTOR memory encoding | Clifford Wolf | 2017-12-17 | 1 | -2/+16 |
| | | |||||
| * | Add array support to btor back-end | Clifford Wolf | 2017-12-15 | 1 | -6/+169 |
| | | |||||
| * | Add $anyconst/$anyseq support to btor back-end | Clifford Wolf | 2017-12-15 | 1 | -13/+51 |
| | | |||||
| * | Merge branch 'master' into btor-ng | Clifford Wolf | 2017-12-14 | 3 | -7/+11 |
| |\ | |||||
| | * | Add yosys-smtbmc VCD writer support for memories with async writes | Clifford Wolf | 2017-12-14 | 3 | -7/+11 |
| | | | |||||
| * | | Merge branch 'master' into btor-ng | Clifford Wolf | 2017-12-14 | 1 | -14/+53 |
| |\| | |||||
| | * | 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 |
| | | | |||||
| * | | Add "write_btor -s" mode | Clifford Wolf | 2017-12-13 | 1 | -6/+50 |
| | | | |||||
| * | | Add state initval handling to btor back-end | Clifford Wolf | 2017-12-12 | 1 | -0/+25 |
| | | | |||||
| * | | Add btor back-end support for 'x' constants | Clifford Wolf | 2017-12-12 | 1 | -1/+54 |
| | | | |||||
| * | | Add btor $shift/$shiftx support | Clifford Wolf | 2017-12-11 | 2 | -7/+37 |
| | | | |||||
| * | | Fix btor back-end shift handling | Clifford Wolf | 2017-12-10 | 2 | -5/+7 |
| | | | |||||
| * | | Add support for $pmux in btor back-end | Clifford Wolf | 2017-12-10 | 1 | -0/+23 |
| | | | |||||
| * | | Add support for more cell types to btor back-end | Clifford Wolf | 2017-12-10 | 2 | -6/+245 |
| | | | |||||
| * | | Fix btor concat | Clifford Wolf | 2017-12-09 | 1 | -1/+1 |
| | | | |||||
| * | | Fixed "yosys-smtbmc -g" handling of no solution | Clifford Wolf | 2017-11-27 | 1 | -1/+1 |
| | | | |||||
| * | | Bugfixes in new BTOR back-end | Clifford Wolf | 2017-11-24 | 1 | -2/+3 |
| | | | |||||
| * | | Progress in new BTOR back-end | Clifford Wolf | 2017-11-23 | 1 | -36/+97 |
| | | | |||||
| * | | Progress in new BTOR back-end | Clifford Wolf | 2017-11-23 | 1 | -3/+95 |
| | | | |||||
| * | | Progress in new BTOR back-end | Clifford Wolf | 2017-11-23 | 1 | -14/+72 |
| | | | |||||
| * | | Progress with new BTOR backend | Clifford Wolf | 2017-11-23 | 1 | -8/+109 |
| | | | |||||
| * | | Add skeleton for new BTOR back-end | Clifford Wolf | 2017-11-23 | 2 | -0/+216 |
| | | | |||||
| * | | Remove old BTOR back-end | Clifford Wolf | 2017-11-23 | 4 | -1174/+0 |
| |/ | |||||
| * | 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 |
| | | |||||
| * | Add $shiftx support to verilog front-end | Clifford Wolf | 2017-10-07 | 1 | -0/+17 |
| | | |||||
| * | Rename "write_verilog -nobasenradix" to "write_verilog -decimal" | Clifford Wolf | 2017-10-03 | 1 | -16/+13 |
| | | |||||
| * | Fixed wrong declaration in Verilog backend | dh73 | 2017-10-01 | 1 | -3/+3 |
| | | |||||
| * | Adding Cyclone IV (E, GX), Arria 10, Cyclone V and LPM functions (ALTPLL and ↵ | dh73 | 2017-10-01 | 1 | -3/+16 |
| | | | | | M9K); M9K is not finished yet. Achronix Speedster also in this commit. Both Arria10 and Speedster-i are still experimental due complexity, but you can experiment around those devices right now | ||||
| * | 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 |
| | | |||||
 |
index : iCE40/yosys | |
| [no description] |
| aboutsummaryrefslogtreecommitdiffstats |