verification/rvgen: Support the 'next' operator

The 'next' operator is a unary operator. It is defined as: "next time, the
operand must be true".

Support this operator. For RV monitors, "next time" means the next
invocation of ltl_validate().

Cc: John Ogness <john.ogness@linutronix.de>
Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Link: https://lore.kernel.org/9c32cec04dd18d2e956fddd84b0e0a2503daa75a.1752239482.git.namcao@linutronix.de
Signed-off-by: Nam Cao <namcao@linutronix.de>
Tested-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>

diff --git a/Documentation/trace/rv/linear_temporal_logic.rst b/Documentation/trace/rv/linear_temporal_logic.rst
index 57f107fcf6dd72baf7d0bbb7062c3dc8d80ae61a..9eee09d9cacf2f976cf6524909c27e5ada5f6bfe 100644 (file)
--- a/Documentation/trace/rv/linear_temporal_logic.rst
+++ b/Documentation/trace/rv/linear_temporal_logic.rst
@@ -41,6 +41,7 @@ Operands (opd):
 Unary Operators (unop):
     always
     eventually
+    next
     not
 
 Binary Operators (binop):

diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py
index d11840af7f5fd3e2bde2c396f1df150bddcce2a6..f14e6760ac3db8a39823f35aaec4ce8541691deb 100644 (file)
--- a/tools/verification/rvgen/rvgen/ltl2ba.py
+++ b/tools/verification/rvgen/rvgen/ltl2ba.py
@@ -19,6 +19,7 @@ from ply.yacc import yacc
 # Unary Operators (unop):
 #       always
 #       eventually
+#       next
 #       not
 #
 # Binary Operators (binop):
@@ -35,6 +36,7 @@ tokens = (
    'UNTIL',
    'ALWAYS',
    'EVENTUALLY',
+   'NEXT',
    'VARIABLE',
    'LITERAL',
    'NOT',
@@ -48,6 +50,7 @@ t_OR = r'or'
 t_IMPLY = r'imply'
 t_UNTIL = r'until'
 t_ALWAYS = r'always'
+t_NEXT = r'next'
 t_EVENTUALLY = r'eventually'
 t_VARIABLE = r'[A-Z_0-9]+'
 t_LITERAL = r'true|false'
@@ -327,6 +330,26 @@ class AlwaysOp(UnaryOp):
         # ![]F == <>(!F)
         return EventuallyOp(self.child.negate()).normalize()
 
+class NextOp(UnaryOp):
+    def normalize(self):
+        return self
+
+    def _is_temporal(self):
+        return True
+
+    def negate(self):
+        # not (next A) == next (not A)
+        self.child = self.child.negate()
+        return self
+
+    @staticmethod
+    def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+        tmp = GraphNode(node.incoming,
+                        node.new,
+                        node.old | {n},
+                        node.next | {n.op.child})
+        return tmp.expand(node_set)
+
 class NotOp(UnaryOp):
     def __str__(self):
         return "!" + str(self.child)
@@ -452,12 +475,15 @@ def p_unop(p):
     '''
     unop : ALWAYS ltl
          | EVENTUALLY ltl
+         | NEXT ltl
          | NOT ltl
     '''
     if p[1] == "always":
         op = AlwaysOp(p[2])
     elif p[1] == "eventually":
         op = EventuallyOp(p[2])
+    elif p[1] == "next":
+        op = NextOp(p[2])
     elif p[1] == "not":
         op = NotOp(p[2])
     else: