aboutsummaryrefslogtreecommitdiffstats
path: root/src/grt/grt-psl.adb
Commit message (Collapse)AuthorAgeFilesLines
* src: Introduce two separate PSL counters (Finish and Start).Ondrej Ille2021-04-081-7/+14
| | | | | | Finish counter corresponds to legacy count. Start counter corresponds to number of times start state is left (assertion is triggered).
* src: Adjust grt-psl to use PSL RTI type.Ondrej Ille2021-04-081-5/+5
|
* update license headersumarcor2021-01-141-11/+9
|
* Add support for PSL assumptions, used in formal verification (#880)Pepijn de Vos2019-08-071-0/+22
| | | | | | | | | | | | | | | | | | | | | | | | | | * vhdl: make the parser understand PSL assume * assume does not actually have report according to the spec. Just a property. * add SPL assume to semantic analysis * canonicalise PSL assume * add assume to annotations * add PSL assume to simulation code * statement -> directive * add assume to translation files * update ticked24 testcase * correctly parse assume * add assume testcase * refactor chunk of duplicated code
* grt: rework error API (WIP).Tristan Gingold2018-09-161-1/+1
|
* PSL: add clocked SERE, make endpoints visible from VHDL.Tristan Gingold2016-03-221-1/+1
|
* grt-psl.adb: fix build failure (unused package).Tristan Gingold2016-03-181-1/+0
|
* PSL: add counters, generate rti and add --psl-reportTristan Gingold2016-03-181-0/+217