aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Continue refactoring of Verific SVA importer codeClifford Wolf2018-02-283-671/+172
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Major redesign of Verific SVA importerClifford Wolf2018-02-272-6/+574
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add -lz for verific buildsClifford Wolf2018-02-271-1/+1
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add handling of verific OPER_REDUCE_NORClifford Wolf2018-02-261-0/+6
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add handling of verific OPER_SELECTOR and OPER_WIDE_SELECTORClifford Wolf2018-02-261-0/+13
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add handling of verific OPER_NTO1MUX and OPER_WIDE_NTO1MUXClifford Wolf2018-02-261-0/+25
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add "SVA syntax cheat sheet" comment to verificsva.ccClifford Wolf2018-02-261-0/+34
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add $dlatchsr support to clk2fflogicClifford Wolf2018-02-261-4/+25
|
* Small fixes and improvements in $allconst/$allseq handlingClifford Wolf2018-02-262-16/+23
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix opt_rmdff handling of $dlatchsrClifford Wolf2018-02-261-0/+3
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Merge branch 'forall'Clifford Wolf2018-02-2317-98/+424
|\
| * Add smtbmc support for exist-forall problemsClifford Wolf2018-02-236-89/+357
| | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
| * Add $allconst and $allseq cell typesClifford Wolf2018-02-2311-9/+67
|/ | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add Verific SVA support for ranges in repetition operatorClifford Wolf2018-02-221-5/+26
|
* Add support for SVA throughout via VerificClifford Wolf2018-02-212-3/+7
|
* Add support for mockup clock signals in yosys-smtbmc vcd outputClifford Wolf2018-02-203-6/+111
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Merge pull request #507 from cr1901/msys2Clifford Wolf2018-02-191-3/+3
|\ | | | | Improve msys2 flags for building abc.
| * Improve msys2 flags for building abc.William D. Jones2018-02-191-3/+3
|/
* Add support for SVA sequence concatenation ranges via verificClifford Wolf2018-02-183-16/+144
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add support for SVA until statements via VerificClifford Wolf2018-02-183-34/+138
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Move Verific SVA importer to extra C++ source fileClifford Wolf2018-02-184-1279/+1370
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Merge Verific SVA preprocessor and SVA importerClifford Wolf2018-02-181-79/+44
|
* Merge branch 'master' of github.com:cliffordwolf/yosysClifford Wolf2018-02-161-0/+6
|\
| * Improve handling of "bus" pins in liberty front-end (some files use ↵Clifford Wolf2018-02-151-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_IFFClifford Wolf2018-02-152-1/+35
|/
* Fixed yosys-config for binary distributions with VerificClifford Wolf2018-02-131-3/+11
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Recognize stand-alone obj pattern even when it contains a slashClifford Wolf2018-02-131-0/+3
|
* Fix handling of zero-length cell connections in SMT2 back-endClifford Wolf2018-02-081-0/+8
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Merge branch 'master' of github.com:cliffordwolf/yosysClifford Wolf2018-02-031-0/+2
|\
| * Merge pull request #488 from azonenberg/for_cliffordClifford Wolf2018-02-031-0/+2
| |\ | | | | | | coolrunner2: Move LOC attributes onto the IO cells
| | * coolrunner2: Move LOC attributes onto the IO cellsRobert Ou2018-01-171-0/+2
| | |
* | | Do not create deep backtraces unless in ENABLE_DEBUG modeClifford Wolf2018-02-032-2/+6
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Fixed gcc 7.2 "statement will never be executed" warningClifford Wolf2018-02-031-1/+1
|/ /
* | Fix single-bit $stable handling in verific front-endClifford Wolf2018-02-011-0/+22
| | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | Add Verific attribute handling for assert/assume/cover/live/fair cellsClifford Wolf2018-01-311-10/+16
| | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | Fix smtio.py for large SMT2 S-expressionsClifford Wolf2018-01-291-1/+12
| |
* | Fix permissions on verific vdb filesClifford Wolf2018-01-281-0/+1
| |
* | Fixed handling of synchronous and asynchronous assertion/assumption/cover in ↵Clifford Wolf2018-01-231-27/+29
| | | | | | | | | | | | verific bindings Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | Use "strip -S" instead of "strip -d" for Mac OS X compatibilityClifford Wolf2018-01-191-2/+2
| | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | Improve log messages in equiv_makeClifford Wolf2018-01-191-2/+2
| | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | Move user-provided smt2 info stmts to the top of the yosys-smtbmc smt2 outputClifford Wolf2018-01-181-3/+3
|/
* Strip debug symbols from binaries on installClifford Wolf2018-01-171-1/+12
|
* Add "dffinit -highlow" and fix synth_intelClifford Wolf2018-01-092-1/+21
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add support for "yosys -E"Clifford Wolf2018-01-0713-4/+53
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Bugfix in hierarchy blackbox module port width handlingClifford Wolf2018-01-071-1/+2
|
* Update ABC to hg rev 6e3c24b3308aClifford Wolf2018-01-071-1/+1
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Merge pull request #479 from Fatsie/latch_without_dataClifford Wolf2018-01-051-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 Verhaegen2018-01-031-4/+23
| |
* | Bugfix in hierarchy handling of blackbox module portsClifford Wolf2018-01-055-9/+10
| | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | Merge pull request #480 from Fatsie/liberty_value_expressionClifford Wolf2018-01-041-2/+22
|\ \ | | | | | | Value of properties can be expression.