| 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> | ||||
| * | Add SVA support for sequence OR | Clifford Wolf | 2018-03-03 | 1 | -22/+33 |
| | | | | | 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> | ||||
| * | Fix handling of SVA "until seq.triggered" properties | Clifford Wolf | 2018-03-02 | 1 | -7/+25 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Update SVA cheat sheet in verificsva.cc | Clifford Wolf | 2018-03-02 | 1 | -2/+4 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Fix in Verific SVA importer handling of until_with | Clifford Wolf | 2018-03-01 | 1 | -7/+5 |
| | | | | | 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> | ||||
| * | Fixes and improvements in Verific SVA importer | Clifford Wolf | 2018-03-01 | 3 | -83/+136 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Add $rose/$fell support to Verific bindings | Clifford Wolf | 2018-03-01 | 1 | -3/+22 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Merge branch 'verificsva-ng' | Clifford Wolf | 2018-02-28 | 4 | -403/+752 |
| |\ | |||||
| | * | Add support for PRIM_SVA_UNTIL to new SVA importer | Clifford Wolf | 2018-02-28 | 1 | -0/+27 |
| | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| | * | Add DFSM generator to verific SVA importer | Clifford Wolf | 2018-02-28 | 1 | -19/+272 |
| | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| | * | Continue refactoring of Verific SVA importer code | Clifford Wolf | 2018-02-28 | 3 | -671/+172 |
| | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| | * | Major redesign of Verific SVA importer | Clifford Wolf | 2018-02-27 | 2 | -6/+574 |
| |/ | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Add -lz for verific builds | Clifford Wolf | 2018-02-27 | 1 | -1/+1 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Add handling of verific OPER_REDUCE_NOR | Clifford Wolf | 2018-02-26 | 1 | -0/+6 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Add handling of verific OPER_SELECTOR and OPER_WIDE_SELECTOR | Clifford Wolf | 2018-02-26 | 1 | -0/+13 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Add handling of verific OPER_NTO1MUX and OPER_WIDE_NTO1MUX | Clifford Wolf | 2018-02-26 | 1 | -0/+25 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Add "SVA syntax cheat sheet" comment to verificsva.cc | Clifford Wolf | 2018-02-26 | 1 | -0/+34 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Add $dlatchsr support to clk2fflogic | Clifford Wolf | 2018-02-26 | 1 | -4/+25 |
| | | |||||
| * | Small fixes and improvements in $allconst/$allseq handling | Clifford Wolf | 2018-02-26 | 2 | -16/+23 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Fix opt_rmdff handling of $dlatchsr | Clifford Wolf | 2018-02-26 | 1 | -0/+3 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Merge branch 'forall' | Clifford Wolf | 2018-02-23 | 17 | -98/+424 |
| |\ | |||||
| | * | Add smtbmc support for exist-forall problems | Clifford Wolf | 2018-02-23 | 6 | -89/+357 |
| | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| | * | Add $allconst and $allseq cell types | Clifford Wolf | 2018-02-23 | 11 | -9/+67 |
| |/ | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Add Verific SVA support for ranges in repetition operator | Clifford Wolf | 2018-02-22 | 1 | -5/+26 |
| | | |||||
| * | Add support for SVA throughout via Verific | Clifford Wolf | 2018-02-21 | 2 | -3/+7 |
| | | |||||
| * | 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> | ||||
| * | Merge pull request #507 from cr1901/msys2 | Clifford Wolf | 2018-02-19 | 1 | -3/+3 |
| |\ | | | | | Improve msys2 flags for building abc. | ||||
| | * | Improve msys2 flags for building abc. | William D. Jones | 2018-02-19 | 1 | -3/+3 |
| |/ | |||||
| * | Add support for SVA sequence concatenation ranges via verific | Clifford Wolf | 2018-02-18 | 3 | -16/+144 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Add support for SVA until statements via Verific | Clifford Wolf | 2018-02-18 | 3 | -34/+138 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Move Verific SVA importer to extra C++ source file | Clifford Wolf | 2018-02-18 | 4 | -1279/+1370 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Merge Verific SVA preprocessor and SVA importer | Clifford Wolf | 2018-02-18 | 1 | -79/+44 |
| | | |||||
| * | Merge branch 'master' of github.com:cliffordwolf/yosys | Clifford Wolf | 2018-02-16 | 1 | -0/+6 |
| |\ | |||||
| | * | Improve handling of "bus" pins in liberty front-end (some files use ↵ | Clifford Wolf | 2018-02-15 | 1 | -0/+6 |
| | | | | | | | | | | | | | bus.pin.direction) Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | | Fix verific PRIM_SVA_AT handling in properties with PRIM_SVA_DISABLE_IFF | Clifford Wolf | 2018-02-15 | 2 | -1/+35 |
| |/ | |||||
| * | Fixed yosys-config for binary distributions with Verific | Clifford Wolf | 2018-02-13 | 1 | -3/+11 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Recognize stand-alone obj pattern even when it contains a slash | Clifford Wolf | 2018-02-13 | 1 | -0/+3 |
| | | |||||
| * | 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> | ||||
| * | Merge branch 'master' of github.com:cliffordwolf/yosys | Clifford Wolf | 2018-02-03 | 1 | -0/+2 |
| |\ | |||||
| | * | Merge pull request #488 from azonenberg/for_clifford | Clifford Wolf | 2018-02-03 | 1 | -0/+2 |
| | |\ | | | | | | | coolrunner2: Move LOC attributes onto the IO cells | ||||
| | | * | coolrunner2: Move LOC attributes onto the IO cells | Robert Ou | 2018-01-17 | 1 | -0/+2 |
| | | | | |||||
| * | | | Do not create deep backtraces unless in ENABLE_DEBUG mode | Clifford Wolf | 2018-02-03 | 2 | -2/+6 |
| | | | | | | | | | | | | | 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 single-bit $stable handling in verific front-end | Clifford Wolf | 2018-02-01 | 1 | -0/+22 |
| | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | | Add Verific attribute handling for assert/assume/cover/live/fair cells | Clifford Wolf | 2018-01-31 | 1 | -10/+16 |
| | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | | Fix smtio.py for large SMT2 S-expressions | Clifford Wolf | 2018-01-29 | 1 | -1/+12 |
| | | | |||||
| * | | Fix permissions on verific vdb files | Clifford Wolf | 2018-01-28 | 1 | -0/+1 |
| | | | |||||
 |
index : iCE40/yosys | |
| [no description] |
| aboutsummaryrefslogtreecommitdiffstats |