aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
* | | Fix SVA handling of NON_CONSECUTIVE_REPEAT and GOTO_REPEATClifford Wolf2018-03-101-15/+72
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Fix variable name typo in verificsva.ccClifford Wolf2018-03-101-2/+2
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Add support for trivial SVA sequences and propertiesClifford Wolf2018-03-101-12/+102
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Fix handling of src attributes in flattenClifford Wolf2018-03-101-7/+2
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Remove debug prints from yosys-smtbmc VCD writerClifford Wolf2018-03-081-2/+0
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Use Verific hier_tree component for elaborationClifford Wolf2018-03-082-1/+55
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Check results of (check-sat) in yosys-smtbmcClifford Wolf2018-03-071-0/+2
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Fix Verific handling of "assert property (..);" in always blockClifford Wolf2018-03-073-14/+60
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Add "verific -import -V"Clifford Wolf2018-03-072-6/+18
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Set Verific db_preserve_user_nets flagClifford Wolf2018-03-071-0/+1
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Add Xilinx RAM64X1D and RAM128X1D simulation modelsClifford Wolf2018-03-074-23/+30
| | |
* | | Add "memory_nordff" passClifford Wolf2018-03-062-0/+112
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Update comment about supported SVA in verificsva.ccClifford Wolf2018-03-061-51/+8
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Add SVA NON_CONSECUTIVE_REPEAT and GOTO_REPEAT supportClifford Wolf2018-03-061-20/+41
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Add SVA first_match() supportClifford Wolf2018-03-061-0/+16
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Add SVA within supportClifford Wolf2018-03-061-2/+18
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Add support for SVA sequence intersectClifford Wolf2018-03-061-36/+251
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Add get_fsm_accept_reject for parsing SVA propertiesClifford Wolf2018-03-061-73/+86
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Simplified SVA "until" handlingClifford Wolf2018-03-061-25/+16
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Imporove yosys-smtbmc error handling, Improve VCD outputClifford Wolf2018-03-052-23/+49
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Fix connwrappers help messageClifford Wolf2018-03-041-1/+1
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Improve handling of warning messagesClifford Wolf2018-03-043-12/+42
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Update copyright headerClifford Wolf2018-03-041-1/+1
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Improve SMT2 encoding of $reduce_{and,or,bool}Clifford Wolf2018-03-041-1/+9
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Fix a hangup in yosys-smtbmc error handlingClifford Wolf2018-03-041-3/+5
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Add proper SVA seq.triggered supportClifford Wolf2018-03-043-37/+102
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Add "synth -noshare"Clifford Wolf2018-03-041-2/+11
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Add Verific SVA support for "seq and seq" expressionsClifford Wolf2018-03-041-24/+94
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Refactor Verific SVA importer property parserClifford Wolf2018-03-041-56/+82
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Add VerificClocking class and refactor Verific DFF handlingClifford Wolf2018-03-043-126/+196
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Improved error handling in yosys-smtbmcClifford Wolf2018-03-031-1/+3
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Add SVA support for sequence ORClifford Wolf2018-03-031-22/+33
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Terminate running SMT solver when smtbmc is terminatedClifford Wolf2018-03-031-1/+31
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Fix smtbmc smtc/aiw parser for wire names containing []Clifford Wolf2018-03-031-1/+1
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Fix handling of SVA "until seq.triggered" propertiesClifford Wolf2018-03-021-7/+25
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Update SVA cheat sheet in verificsva.ccClifford Wolf2018-03-021-2/+4
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Fix in Verific SVA importer handling of until_withClifford Wolf2018-03-011-7/+5
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Mangle names with square brackets in VCD files to work around issues in gtkwaveClifford Wolf2018-03-011-2/+8
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Fixes and improvements in Verific SVA importerClifford Wolf2018-03-013-83/+136
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Add $rose/$fell support to Verific bindingsClifford Wolf2018-03-011-3/+22
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | 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
| | | | | | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
| * | | Add DFSM generator to verific SVA importerClifford Wolf2018-02-281-19/+272
| | | | | | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
| * | | 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>
generated by cgit v1.2.3 (git 2.25.1) at 2025-07-14 14:09:49 +0000