linux-toradex.git/tools/verification/rvgen, branch toradex_ti-linux-6.18.y

verification/rvgen: Fix ltl2k writing True as a literal

2026-06-19T11:43:57+00:00

[ Upstream commit df996599cc69a9b74ff437c67751cf8a61f62e39 ]

The rvgen parser for LTL stores literal true values in the python
representation (capitalised True), this doesn't build in C.
The Literal class should already handle this case but ASTNode skips its
strigification method and converts the value (true/false) directly.

Fix by delegating ASTNode stringification to the Literal and Variable
classes instead of bypassing them.

Fixes: 97ffa4ce6ab32 ("verification/rvgen: Add support for linear temporal logic")
Reviewed-by: Nam Cao 
Link: https://lore.kernel.org/r/20260514152055.229162-8-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco 
Signed-off-by: Sasha Levin

verification/rvgen: Fix options shared among commands

2026-06-19T11:43:57+00:00

[ Upstream commit 5f845ad706c0b394ae274e9a930044f78bef782e ]

After rvgen was refactored to use subparsers, the common options (-a and
-D) were left in the main parser. This meant that they needed to be
called /before/ the subcommand and using them without subcommand was
allowed. This is not the original intent.

  rvgen -D "some description" container -n name

Define the options as parent in the subparsers to allow them to be used
from both subcommands together with other options.

  rvgen container -n name -D "some description"

Fixes: 5270a0e3041c ("verification/dot2k: Replace is_container() hack with subparsers")
Reviewed-by: Nam Cao 
Link: https://lore.kernel.org/r/20260514152055.229162-7-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco 
Signed-off-by: Sasha Levin

rv: Return init error when registering monitors

2025-07-24T14:43:46+00:00

Monitors generated with dot2k have their registration function (the one
called during monitor initialisation) return always 0, even if the
registration failed on RV side.
This can hide potential errors.

Return the value returned by the RV register function.

Cc: Masami Hiramatsu 
Cc: Tomas Glozar 
Cc: Juri Lelli 
Cc: Clark Williams 
Cc: John Kacur 
Link: https://lore.kernel.org/20250723161240.194860-6-gmonaco@redhat.com
Reviewed-by: Nam Cao 
Signed-off-by: Gabriele Monaco 
Signed-off-by: Steven Rostedt (Google)

verification/rvgen: Organise Kconfig entries for nested monitors

2025-07-24T14:43:46+00:00

The current behaviour of rvgen when running with the -a option is to
append the necessary lines at the end of the configuration for Kconfig,
Makefile and tracepoints.
This is not always the desired behaviour in case of nested monitors:
while tracepoints are not affected by nesting and the Makefile's only
requirement is that the parent monitor is built before its children, in
the Kconfig it is better to have children defined right after their
parent, otherwise the result has wrong indentation:

[*]   foo_parent monitor
[*]     foo_child1 monitor
[*]     foo_child2 monitor
[*]   bar_parent monitor
[*]     bar_child1 monitor
[*]     bar_child2 monitor
[*]   foo_child3 monitor
[*]   foo_child4 monitor

Adapt rvgen to look for a different marker for nested monitors in the
Kconfig file and append the line right after the last sibling, instead
of the last monitor.
Also add the marker when creating a new parent monitor.

Cc: Masami Hiramatsu 
Cc: Tomas Glozar 
Cc: Juri Lelli 
Cc: Clark Williams 
Cc: John Kacur 
Link: https://lore.kernel.org/20250723161240.194860-5-gmonaco@redhat.com
Reviewed-by: Nam Cao 
Signed-off-by: Gabriele Monaco 
Signed-off-by: Steven Rostedt (Google)

tools/dot2c: Fix generated files going over 100 column limit

2025-07-24T14:43:46+00:00

The dot2c.py script generates all states in a single line. This breaks the
100 column limit when the state machines are non-trivial.

Change dot2c.py to generate the states in separate lines in case the
generated line is going to be too long.

Also adapt existing monitors with line length over the limit.

Cc: Masami Hiramatsu 
Cc: Tomas Glozar 
Cc: Juri Lelli 
Cc: Clark Williams 
Cc: John Kacur 
Link: https://lore.kernel.org/20250723161240.194860-4-gmonaco@redhat.com
Suggested-by: Nam Cao 
Signed-off-by: Gabriele Monaco 
Signed-off-by: Steven Rostedt (Google)

verification/rvgen: Do not generate unused variables

2025-07-24T14:43:23+00:00

ltl2k generates all variable definition in both ltl_start() and
ltl_possible_next_states(). However, these two functions may not use all
the variables, causing "unused variable" compiler warning.

Change the script to only generate used variables.

Cc: Masami Hiramatsu 
Cc: Mathieu Desnoyers 
Link: https://lore.kernel.org/636b2b2d99a9bd46a9f77a078d44ebd7ffc7508c.1752850449.git.namcao@linutronix.de
Signed-off-by: Nam Cao 
Reviewed-by: Gabriele Monaco 
Signed-off-by: Steven Rostedt (Google)

verification/rvgen: Generate each variable definition only once

2025-07-24T14:43:23+00:00

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)

verification/rvgen: Support the 'next' operator

2025-07-24T14:43:23+00:00

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 
Cc: Masami Hiramatsu 
Cc: Mathieu Desnoyers 
Link: https://lore.kernel.org/9c32cec04dd18d2e956fddd84b0e0a2503daa75a.1752239482.git.namcao@linutronix.de
Signed-off-by: Nam Cao 
Tested-by: Gabriele Monaco 
Signed-off-by: Steven Rostedt (Google)

verification/rvgen: Add support for linear temporal logic

2025-07-24T14:42:47+00:00

Add support for generating RV monitors from linear temporal logic, similar
to the generation of deterministic automaton monitors.

Cc: Masami Hiramatsu 
Cc: Mathieu Desnoyers 
Cc: Gabriele Monaco 
Link: https://lore.kernel.org/f3c63b363ff9c5af3302ba2b5d92a26a98700eaf.1751634289.git.namcao@linutronix.de
Signed-off-by: Nam Cao 
Signed-off-by: Steven Rostedt (Google)

verification/rvgen: Restructure the classes to prepare for LTL inclusion

2025-07-24T14:42:46+00:00

Both container generation and DA monitor generation is implemented in the
class dot2k. That requires some ugly "if is_container ... else ...". If
linear temporal logic support is added at the current state, the "if else"
chain is longer and uglier.

Furthermore, container generation is irrevelant to .dot files. It is
therefore illogical to be implemented in class "dot2k".

Clean it up, restructure the dot2k class into the following class
hierarchy:

         (RVGenerator)
              /\
             /  \
            /    \
           /      \
          /        \
    (Container)  (Monitor)
                    /\
                   /  \
                  /    \
                 /      \
              (dot2k)  [ltl2k] <- intended

This allows a simple and clean integration of LTL.

Cc: Masami Hiramatsu 
Cc: Mathieu Desnoyers 
Link: https://lore.kernel.org/692137a581ba6bee7a64d37fb7173ae137c47bbd.1751634289.git.namcao@linutronix.de
Reviewed-by: Gabriele Monaco 
Signed-off-by: Nam Cao 
Signed-off-by: Steven Rostedt (Google)