From 6fb37c2a27ebdddddcc36dbdfb6b88cc9f932895 Mon Sep 17 00:00:00 2001 From: Nam Cao Date: Fri, 18 Jul 2025 16:58:10 +0200 Subject: [PATCH] verification/rvgen: Generate each variable definition only once If a variable appears multiple times in the specification, ltl2k generates multiple variable definitions. This fails the build. Make sure each variable is only defined once. Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Cc: Gabriele Monaco Link: https://lore.kernel.org/107dcf0d0aa8482d5fbe0314c3138f61cd284e91.1752850449.git.namcao@linutronix.de Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- tools/verification/rvgen/rvgen/ltl2k.py | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/rvgen/rvgen/ltl2k.py index 92e713861d86..59da351792ec 100644 --- a/tools/verification/rvgen/rvgen/ltl2k.py +++ b/tools/verification/rvgen/rvgen/ltl2k.py @@ -112,14 +112,16 @@ class ltl2k(generator.Monitor): if node.op.is_temporal(): continue - if isinstance(node.op, ltl2ba.Variable): - buf.append("\tbool %s = test_bit(LTL_%s, mon->atoms);" % (node, node.op.name)) - elif isinstance(node.op, ltl2ba.AndOp): + if isinstance(node.op, ltl2ba.AndOp): buf.append("\tbool %s = %s && %s;" % (node, node.op.left, node.op.right)) elif isinstance(node.op, ltl2ba.OrOp): buf.append("\tbool %s = %s || %s;" % (node, node.op.left, node.op.right)) elif isinstance(node.op, ltl2ba.NotOp): buf.append("\tbool %s = !%s;" % (node, node.op.child)) + + for atom in self.atoms: + buf.append("\tbool %s = test_bit(LTL_%s, mon->atoms);" % (atom.lower(), atom)) + buf.reverse() buf2 = [] -- 2.47.2