aboutsummaryrefslogtreecommitdiffstats
path: root/frontends/verific/verificsva.cc
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2018-02-26 14:31:58 +0100
committerClifford Wolf <clifford@clifford.at>2018-02-26 14:31:58 +0100
commitd1cb5150aaf1f08194385ebc88eea1168366f7d3 (patch)
treefe7d98b4985a65f390a6943c60a2be48178adecf /frontends/verific/verificsva.cc
parentd31584c649c54641f497244b3bee5067801251e7 (diff)
downloadyosys-d1cb5150aaf1f08194385ebc88eea1168366f7d3.tar.gz
yosys-d1cb5150aaf1f08194385ebc88eea1168366f7d3.tar.bz2
yosys-d1cb5150aaf1f08194385ebc88eea1168366f7d3.zip
Add "SVA syntax cheat sheet" comment to verificsva.cc
Signed-off-by: Clifford Wolf <clifford@clifford.at>
Diffstat (limited to 'frontends/verific/verificsva.cc')
-rw-r--r--frontends/verific/verificsva.cc34
1 files changed, 34 insertions, 0 deletions
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index d970756ac..94443cd3e 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -17,6 +17,40 @@
*
*/
+
+// SVA Properties Simplified Syntax:
+//
+// prop:
+// not prop
+// prop or prop
+// prop and prop
+// seq |-> prop
+// seq |=> prop
+// if (expr) prop [else prop]
+// prop until prop
+// prop implies prop
+// prop iff prop
+// accept_on (expr) prop
+// reject_on (expr) prop
+//
+// seq:
+// expr
+// expr ##N seq
+// expr ##[N:M] seq
+// seq or seq
+// seq and seq
+// seq intersect seq
+// first_match (seq)
+// expr throughout seq
+// seq within seq
+// seq [*N]
+// seq [*N:M]
+// expr [=N]
+// expr [=N:M]
+// expr [->N]
+// expr [->N:M]
+
+
#include "kernel/yosys.h"
#include "frontends/verific/verific.h"