mirror of https://github.com/YosysHQ/yosys.git
Update comment about supported SVA in verificsva.cc
Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
parent
03b49654b1
commit
dcc4a18d5a
|
@ -18,60 +18,17 @@
|
||||||
*/
|
*/
|
||||||
|
|
||||||
|
|
||||||
// Currently supported property styles:
|
// Currently supported SVA sequence and property syntax:
|
||||||
// seq
|
// http://symbiyosys.readthedocs.io/en/latest/verific.html
|
||||||
// not seq
|
|
||||||
// seq |-> seq
|
|
||||||
// seq |-> not seq
|
|
||||||
// seq |-> seq until expr
|
|
||||||
// seq |-> not seq until expr
|
|
||||||
//
|
//
|
||||||
// Currently supported sequence operators:
|
// Todos:
|
||||||
// seq ##[N:M] seq
|
// property and property
|
||||||
// seq or seq
|
// sequence |-> always sequence
|
||||||
// seq and seq
|
// sequence |-> eventually sequence
|
||||||
// expr throughout seq
|
// sequence implies sequence
|
||||||
// seq [*N:M]
|
// sequence iff sequence
|
||||||
//
|
|
||||||
// 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
|
|
||||||
// accept_on (expr) prop
|
// accept_on (expr) prop
|
||||||
// reject_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"
|
#include "kernel/yosys.h"
|
||||||
|
|
Loading…
Reference in New Issue