From d1cb5150aaf1f08194385ebc88eea1168366f7d3 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 26 Feb 2018 14:31:58 +0100 Subject: [PATCH] Add "SVA syntax cheat sheet" comment to verificsva.cc Signed-off-by: Clifford Wolf --- frontends/verific/verificsva.cc | 34 +++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) 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" -- 2.30.2