aboutsummaryrefslogtreecommitdiffstats
path: root/frontends/verific/verificsva.cc
Commit message (Collapse)AuthorAgeFilesLines
* verific: Fix conditions of SVAs with explicit clocks within proceduresJannis Harder2022-05-031-3/+9
| | | | | | | | | For SVAs that have an explicit clock and are contained in a procedure which conditionally executes the assertion, verific expresses this using a mux with one input connected to constant 1 and the other output connected to an SVA_AT. The existing code only handled the case where the first input is connected to 1. This patch also handles the other case.
* Fixing old e-mail addresses and deadnamesClaire Xenia Wolf2021-06-081-1/+1
| | | | | | | | s/((Claire|Xen|Xenia|Clifford)\s+)+(Wolf|Xen)\s+<(claire|clifford)@(symbioticeda.com|clifford.at|yosyshq.com)>/Claire Xenia Wolf <claire@yosyshq.com>/gi; s/((Nina|Nak|N\.)\s+)+Engelhardt\s+<nak@(symbioticeda.com|yosyshq.com)>/N. Engelhardt <nak@yosyshq.com>/gi; s/((David)\s+)+Shah\s+<(dave|david)@(symbioticeda.com|yosyshq.com|ds0.me)>/David Shah <dave@ds0.me>/gi; s/((Miodrag)\s+)+Milanovic\s+<(miodrag|micko)@(symbioticeda.com|yosyshq.com)>/Miodrag Milanovic <micko@yosyshq.com>/gi; s,https?://www.clifford.at/yosys/,http://yosyshq.net/yosys/,g;
* Accept disable case for SVA liveness properties.Diego H2021-02-041-0/+5
|
* Better error for unsupported SVA sequenceMiodrag Milanovic2020-09-181-2/+8
|
* Add Verific support for SVA nexttime propertiesClifford Wolf2019-11-221-0/+22
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add Verific SVA support for "always" propertiesClifford Wolf2019-11-221-5/+15
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Use State::S{0,1}Eddie Hung2019-08-061-1/+1
|
* Add hack for handling SVA labels via VerificClifford Wolf2019-03-071-1/+14
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix typographical and grammatical errors and inconsistencies.whitequark2019-01-021-4/+4
| | | | | | | | | | | | The initial list of hits was generated with the codespell command below, and each hit was evaluated and fixed manually while taking context into consideration. DIRS="kernel/ frontends/ backends/ passes/ techlibs/" DIRS="${DIRS} libs/ezsat/ libs/subcircuit" codespell $DIRS -S *.o -L upto,iff,thru,synopsys,uint More hits were found by looking through comments and strings manually.
* Add "verific -L <int>" optionClifford Wolf2018-09-041-2/+3
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix handling of eventually properties in verific importerClifford Wolf2018-07-171-2/+4
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix verific eventually handlingClifford Wolf2018-06-291-6/+5
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add verific support for eventually propertiesClifford Wolf2018-06-291-5/+105
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Further improve handling of zero-length SVA consecutive repetitionClifford Wolf2018-05-051-69/+108
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix handling of zero-length SVA consecutive repetitionClifford Wolf2018-05-051-26/+46
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Remove left-over log_ping debug commands.. oops.Clifford Wolf2018-03-311-4/+0
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix handling of unclocked immediate assertions in Verific front-endClifford Wolf2018-03-261-15/+35
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Update todo for more features to verificsva.ccClifford Wolf2018-03-161-3/+3
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Update todo for more features to verificsva.ccClifford Wolf2018-03-161-0/+1
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add todo for more features to verificsva.ccClifford Wolf2018-03-161-8/+45
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* 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 Verific handling of "assert property (..);" in always blockClifford Wolf2018-03-071-6/+21
| | | | 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>
* Add proper SVA seq.triggered supportClifford Wolf2018-03-041-36/+84
| | | | 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-041-80/+24
| | | | 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>
* 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>
* Fixes and improvements in Verific SVA importerClifford Wolf2018-03-011-77/+126
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* 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-281-603/+139
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Major redesign of Verific SVA importerClifford Wolf2018-02-271-5/+573
| | | | 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 Verific SVA support for ranges in repetition operatorClifford Wolf2018-02-221-5/+26
|
* Add support for SVA throughout via VerificClifford Wolf2018-02-211-2/+6
|
* Add support for SVA sequence concatenation ranges via verificClifford Wolf2018-02-181-16/+124
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add support for SVA until statements via VerificClifford Wolf2018-02-181-11/+119
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Move Verific SVA importer to extra C++ source fileClifford Wolf2018-02-181-0/+384
Signed-off-by: Clifford Wolf <clifford@clifford.at>
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-04 02:54:43 +0000