diff options
| author | Clifford Wolf <clifford@clifford.at> | 2018-03-06 15:47:33 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2018-03-06 15:47:33 +0100 |
| commit | dcc4a18d5a4a4827704b81400c8f479da5ecc349 (patch) | |
| tree | 5bbabb5afabd113fef35c551fb8d01ba1cebb233 /frontends/verific/verificsva.cc | |
| parent | 03b49654b1573dfea94f589d24415bf256150165 (diff) | |
| download | yosys-dcc4a18d5a4a4827704b81400c8f479da5ecc349.tar.gz yosys-dcc4a18d5a4a4827704b81400c8f479da5ecc349.tar.bz2 yosys-dcc4a18d5a4a4827704b81400c8f479da5ecc349.zip | |
Update comment about supported SVA in verificsva.cc
Signed-off-by: Clifford Wolf <clifford@clifford.at>
Diffstat (limited to 'frontends/verific/verificsva.cc')
| -rw-r--r-- | frontends/verific/verificsva.cc | 59 |
1 files changed, 8 insertions, 51 deletions
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index f89595714..da320019b 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -18,60 +18,17 @@ */ -// Currently supported property styles: -// seq -// not seq -// seq |-> seq -// seq |-> not seq -// seq |-> seq until expr -// seq |-> not seq until expr +// Currently supported SVA sequence and property syntax: +// http://symbiyosys.readthedocs.io/en/latest/verific.html // -// Currently supported sequence operators: -// seq ##[N:M] seq -// seq or seq -// seq and seq -// expr throughout seq -// seq [*N:M] -// -// Notes: -// |-> is a placeholder for |-> and |=> -// "until" is a placeholder for all until operators -// ##[N:M] includes ##N, ##[*], ##[+] -// [*N:M] includes [*N], [*], [+] -// [=N:M], [->N:M] includes [=N], [->N] -// -// Expressions can be any boolean expression, including expressions -// that use $past, $rose, $fell, $stable, and sequence.triggered. -// -// ------------------------------------------------------- -// -// SVA Properties Simplified Syntax (essentially a todo-list): -// -// prop: -// not prop -// prop or prop -// prop and prop -// seq |-> prop -// if (expr) prop [else prop] -// always prop -// prop until prop -// prop implies prop -// prop iff prop +// Todos: +// property and property +// sequence |-> always sequence +// sequence |-> eventually sequence +// sequence implies sequence +// sequence iff sequence // accept_on (expr) prop // reject_on (expr) prop -// -// seq: -// expr -// seq ##[N:M] seq -// seq or seq -// seq and seq -// seq intersect seq -// first_match (seq) -// expr throughout seq -// seq within seq -// seq [*N:M] -// expr [=N:M] -// expr [->N:M] #include "kernel/yosys.h" |