Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
* | 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 | |
| | | ||||||
* | | Fixed handling of synchronous and asynchronous assertion/assumption/cover in ↵ | Clifford Wolf | 2018-01-23 | 1 | -27/+29 | |
| | | | | | | | | | | | | verific bindings Signed-off-by: Clifford Wolf <clifford@clifford.at> | |||||
* | | Use "strip -S" instead of "strip -d" for Mac OS X compatibility | Clifford Wolf | 2018-01-19 | 1 | -2/+2 | |
| | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | |||||
* | | Improve log messages in equiv_make | Clifford Wolf | 2018-01-19 | 1 | -2/+2 | |
| | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | |||||
* | | Move user-provided smt2 info stmts to the top of the yosys-smtbmc smt2 output | Clifford Wolf | 2018-01-18 | 1 | -3/+3 | |
|/ | ||||||
* | Strip debug symbols from binaries on install | Clifford Wolf | 2018-01-17 | 1 | -1/+12 | |
| | ||||||
* | Add "dffinit -highlow" and fix synth_intel | Clifford Wolf | 2018-01-09 | 2 | -1/+21 | |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | |||||
* | Add support for "yosys -E" | Clifford Wolf | 2018-01-07 | 13 | -4/+53 | |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | |||||
* | Bugfix in hierarchy blackbox module port width handling | Clifford Wolf | 2018-01-07 | 1 | -1/+2 | |
| | ||||||
* | Update ABC to hg rev 6e3c24b3308a | Clifford Wolf | 2018-01-07 | 1 | -1/+1 | |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | |||||
* | Merge pull request #479 from Fatsie/latch_without_data | Clifford Wolf | 2018-01-05 | 1 | -4/+23 | |
|\ | | | | | Some standard cell libraries include a latch with only set/reset. | |||||
| * | Some standard cell libraries include a latch with only set/reset. | Staf Verhaegen | 2018-01-03 | 1 | -4/+23 | |
| | | ||||||
* | | Bugfix in hierarchy handling of blackbox module ports | Clifford Wolf | 2018-01-05 | 5 | -9/+10 | |
| | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | |||||
* | | Merge pull request #480 from Fatsie/liberty_value_expression | Clifford Wolf | 2018-01-04 | 1 | -2/+22 | |
|\ \ | | | | | | | Value of properties can be expression. | |||||
| * | | Value of properties can be expression. | Staf Verhaegen | 2018-01-03 | 1 | -2/+22 | |
| |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | Example found in the 2007.03 Liberty Reference Manual that was also found in the wild: input_voltage(CMOS) { vil : 0.3 * VDD ; vih : 0.7 * VDD ; vimin : -0.5 ; vimax : VDD + 0.5 ; } Current implementation just parses the expression but no interpretation is done. | |||||
* / | Temporarily derive blackbox modules in hierarchy to evaluate port widths | Clifford Wolf | 2018-01-04 | 1 | -1/+14 | |
|/ | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> |