kernel.git/tools/verification/rvgen/Makefile, branch master

verification/rvgen: Add support for linear temporal logic

2025-07-24T14:42:47Z

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:46Z

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)

verification/rvgen: Restructure the templates files

2025-07-24T14:42:46Z

To simply the scripts and to allow easy integration of new monitor types, restructure the template files as followed: 1. Move the template files to be in the same directory as the rvgen package. Furthermore, the installation will now only install the templates to the package directory, not /usr/share/. This simplify templates reading, as the scripts do not need to find the templates at multiple places. 2. Move dot2k_templates/* to: - templates/dot2k/ - templates/container/ This allows sharing templates reading code between DA monitor generation and container generation (and any future generation type). For template files which can be shared between different generation types, support putting them in templates/ This restructure aligns with the recommendation from: https://python-packaging.readthedocs.io/en/latest/non-code-files.html Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/462d90273f96804d3ba850474877d5f727031258.1751634289.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google)

verification/dot2k: Prepare the frontend for LTL inclusion

2025-07-24T14:42:46Z

The dot2k tool has some code that can be reused for linear temporal logic monitor. Prepare its frontend for LTL inclusion: 1. Rename to be generic: rvgen 2. Replace the parameter --dot with 2 parameters: --class: to specific the monitor class, can be 'da' or 'ltl' --spec: the monitor specification file, .dot file for DA, and .ltl file for LTL The old command: python3 dot2/dot2k monitor -d wip.dot -t per_cpu is equivalent to the new commands: python3 rvgen monitor -c da -s wip.dot -t per_cpu Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/dea18f7a44374e4db8df5c7e785604bc3062ffc9.1751634289.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google)