diff options
| author | Nam Cao <namcao@linutronix.de> | 2025-07-11 15:17:38 +0200 |
|---|---|---|
| committer | Steven Rostedt (Google) <rostedt@goodmis.org> | 2025-07-24 10:43:23 -0400 |
| commit | 8cfcf9b0e92f917fd3eee19a46924ad3a2f31259 (patch) | |
| tree | e719b52e1afeb93cf49262787625125d1650d3ec | |
| parent | e93648e86273a5d74b4fb96b645950249668093c (diff) | |
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>
| -rw-r--r-- | Documentation/trace/rv/linear_temporal_logic.rst | 1 | ||||
| -rw-r--r-- | tools/verification/rvgen/rvgen/ltl2ba.py | 26 |
2 files changed, 27 insertions, 0 deletions
diff --git a/Documentation/trace/rv/linear_temporal_logic.rst b/Documentation/trace/rv/linear_temporal_logic.rst index 57f107fcf6dd7..9eee09d9cacf2 100644 --- 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 d11840af7f5fd..f14e6760ac3db 100644 --- 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: |