aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Add SVA NON_CONSECUTIVE_REPEAT and GOTO_REPEAT supportClifford Wolf2018-03-061-20/+41
* Add SVA first_match() supportClifford Wolf2018-03-061-0/+16
* Add SVA within supportClifford Wolf2018-03-061-2/+18
* Add support for SVA sequence intersectClifford Wolf2018-03-061-36/+251
* Add get_fsm_accept_reject for parsing SVA propertiesClifford Wolf2018-03-061-73/+86
* Simplified SVA "until" handlingClifford Wolf2018-03-061-25/+16
* Imporove yosys-smtbmc error handling, Improve VCD outputClifford Wolf2018-03-052-23/+49
* Fix connwrappers help messageClifford Wolf2018-03-041-1/+1
* Improve handling of warning messagesClifford Wolf2018-03-043-12/+42
* Update copyright headerClifford Wolf2018-03-041-1/+1
* Improve SMT2 encoding of $reduce_{and,or,bool}Clifford Wolf2018-03-041-1/+9
* Fix a hangup in yosys-smtbmc error handlingClifford Wolf2018-03-041-3/+5
* Add proper SVA seq.triggered supportClifford Wolf2018-03-043-37/+102
* Add "synth -noshare"Clifford Wolf2018-03-041-2/+11
* Add Verific SVA support for "seq and seq" expressionsClifford Wolf2018-03-041-24/+94
* Refactor Verific SVA importer property parserClifford Wolf2018-03-041-56/+82
* Add VerificClocking class and refactor Verific DFF handlingClifford Wolf2018-03-043-126/+196
* Improved error handling in yosys-smtbmcClifford Wolf2018-03-031-1/+3
* Add SVA support for sequence ORClifford Wolf2018-03-031-22/+33
* Terminate running SMT solver when smtbmc is terminatedClifford Wolf2018-03-031-1/+31
* Fix smtbmc smtc/aiw parser for wire names containing []Clifford Wolf2018-03-031-1/+1
* Fix handling of SVA "until seq.triggered" propertiesClifford Wolf2018-03-021-7/+25
* Update SVA cheat sheet in verificsva.ccClifford Wolf2018-03-021-2/+4
* Fix in Verific SVA importer handling of until_withClifford Wolf2018-03-011-7/+5
* Mangle names with square brackets in VCD files to work around issues in gtkwaveClifford Wolf2018-03-011-2/+8
* Fixes and improvements in Verific SVA importerClifford Wolf2018-03-013-83/+136
* Add $rose/$fell support to Verific bindingsClifford Wolf2018-03-011-3/+22
* Merge branch 'verificsva-ng'Clifford Wolf2018-02-284-403/+752
|\
| * Add support for PRIM_SVA_UNTIL to new SVA importerClifford Wolf2018-02-281-0/+27
| * Add DFSM generator to verific SVA importerClifford Wolf2018-02-281-19/+272
| * Continue refactoring of Verific SVA importer codeClifford Wolf2018-02-283-671/+172
| * Major redesign of Verific SVA importerClifford Wolf2018-02-272-6/+574
|/
* Add -lz for verific buildsClifford Wolf2018-02-271-1/+1
* Add handling of verific OPER_REDUCE_NORClifford Wolf2018-02-261-0/+6
* Add handling of verific OPER_SELECTOR and OPER_WIDE_SELECTORClifford Wolf2018-02-261-0/+13
* Add handling of verific OPER_NTO1MUX and OPER_WIDE_NTO1MUXClifford Wolf2018-02-261-0/+25
* Add "SVA syntax cheat sheet" comment to verificsva.ccClifford Wolf2018-02-261-0/+34
* Add $dlatchsr support to clk2fflogicClifford Wolf2018-02-261-4/+25
* Small fixes and improvements in $allconst/$allseq handlingClifford Wolf2018-02-262-16/+23
* Fix opt_rmdff handling of $dlatchsrClifford Wolf2018-02-261-0/+3
* Merge branch 'forall'Clifford Wolf2018-02-2317-98/+424
|\
| * Add smtbmc support for exist-forall problemsClifford Wolf2018-02-236-89/+357
| * Add $allconst and $allseq cell typesClifford Wolf2018-02-2311-9/+67
|/
* 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
* Merge pull request #507 from cr1901/msys2Clifford Wolf2018-02-191-3/+3
|\
| * 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
* Add support for SVA until statements via VerificClifford Wolf2018-02-183-34/+138