diff options
| author | Clifford Wolf <clifford@clifford.at> | 2018-03-16 12:15:36 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2018-03-16 12:15:36 +0100 |
| commit | 462e9f7bd4e072bee5ac7a9552086db5dc09ae67 (patch) | |
| tree | d31bede383c30e94d9da6494e9e626ac32f2902f /frontends | |
| parent | 7cf9d8802832a12b46a32cebb039d161586f414f (diff) | |
| download | yosys-462e9f7bd4e072bee5ac7a9552086db5dc09ae67.tar.gz yosys-462e9f7bd4e072bee5ac7a9552086db5dc09ae67.tar.bz2 yosys-462e9f7bd4e072bee5ac7a9552086db5dc09ae67.zip | |
Add todo for more features to verificsva.cc
Signed-off-by: Clifford Wolf <clifford@clifford.at>
Diffstat (limited to 'frontends')
| -rw-r--r-- | frontends/verific/verificsva.cc | 53 |
1 files changed, 45 insertions, 8 deletions
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index 5abe0eb35..c56854acc 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -21,14 +21,51 @@ // Currently supported SVA sequence and property syntax: // http://symbiyosys.readthedocs.io/en/latest/verific.html // -// Todos: -// property and property -// sequence |-> always sequence -// sequence |-> eventually sequence -// sequence implies sequence -// sequence iff sequence -// accept_on (expr) prop -// reject_on (expr) prop +// Next gen property syntax: +// basic_property +// [antecedent_condition] property +// [antecedent_condition] always.. property +// [antecedent_condition] eventually.. basic_property +// [antecedent_condition] property until.. expression +// [antecedent_condition] basic_property until.. basic_property +// +// antecedent_condition: +// sequence |-> +// sequence |=> +// +// basic_property: +// sequence +// sequence #-# basic_property +// sequence #=# basic_property +// basic_property or basic_property (cover only) +// basic_property and basic_property (assert/assume only) +// basic_property implies basic_property +// basic_property iff basic_property +// +// sequence: +// expression +// sequence ##N sequence +// sequence ##[*] sequence +// sequence ##[+] sequence +// sequence ##[N:M] sequence +// sequence ##[N:$] sequence +// sequence [*] +// sequence [+] +// sequence [*N] +// sequence [*N:M] +// sequence [*N:$] +// sequence or sequence +// sequence and sequence +// expression throughout sequence +// sequence intersect sequence +// sequence within sequence +// first_match( sequence ) +// expression [=N] +// expression [=N:M] +// expression [=N:$] +// expression [->N] +// expression [->N:M] +// expression [->N:$] #include "kernel/yosys.h" |