drm/mediatek: Add missing IS_ERR check for ovl_adaptor platform devicegrafted

platform_device_register_data() can fail and return an ERR_PTR, but the
return value is used without checking, leading to an invalid pointer
being stored in ddp_comp[].dev and passed to component_match_add() and
mtk_ddp_comp_init(), which could result in a kernel crash.

Add an IS_ERR() check to jump to the error handling path on failure.

Fixes: 0d9eee9118b7 ("drm/mediatek: Add drm ovl_adaptor sub driver for MT8195")
Cc: stable@vger.kernel.org
Signed-off-by: Haojie Li <lihaojie@kylinos.cn>
Reviewed-by: CK Hu <ck.hu@mediatek.com>
Link: https://patchwork.kernel.org/project/linux-mediatek/patch/20260825100845.438893-1-lihaojie@kylinos.cn/
Signed-off-by: Chun-Kuang Hu <chunkuang.hu@kernel.org>

92 files changed, 6451 insertions, 0 deletions

diff --git a/tools/verification/rvgen/.gitignore b/tools/verification/rvgen/.gitignore
new file mode 100644
index 000000000..1e288a076
--- /dev/null
+++ b/tools/verification/rvgen/.gitignore
@@ -0,0 +1,3 @@
+__pycache__/
+parser.out
+parsetab.py
diff --git a/tools/verification/rvgen/Makefile b/tools/verification/rvgen/Makefile
new file mode 100644
index 000000000..48d0376a5
--- /dev/null
+++ b/tools/verification/rvgen/Makefile
@@ -0,0 +1,32 @@
+INSTALL=install
+
+prefix  ?= /usr
+bindir  ?= $(prefix)/bin
+mandir  ?= $(prefix)/share/man
+srcdir  ?= $(prefix)/src
+
+PYLIB  ?= $(shell python3 -c 'import sysconfig;  print (sysconfig.get_path("purelib"))')
+
+.PHONY: all
+all:
+
+.PHONY: clean
+clean:
+
+.PHONY: check
+check:
+	prove -o --directives -f tests/
+
+.PHONY: install
+install:
+	$(INSTALL) rvgen/automata.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/automata.py
+	$(INSTALL) rvgen/dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2c.py
+	$(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/
+	$(INSTALL) rvgen/dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2k.py
+	$(INSTALL) rvgen/kunit.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/kunit.py
+	$(INSTALL) rvgen/container.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/container.py
+	$(INSTALL) rvgen/generator.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/generator.py
+	$(INSTALL) rvgen/ltl2ba.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/ltl2ba.py
+	$(INSTALL) rvgen/ltl2k.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/ltl2k.py
+	$(INSTALL) __main__.py -D -m 755 $(DESTDIR)$(bindir)/rvgen
+	cp -rp rvgen/templates $(DESTDIR)$(PYLIB)/rvgen/
diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py
new file mode 100644
index 000000000..246b43fa2
--- /dev/null
+++ b/tools/verification/rvgen/__main__.py
@@ -0,0 +1,86 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
+#
+# dot2k: transform dot files into a monitor for the Linux kernel.
+#
+# For further information, see:
+#   Documentation/trace/rv/monitor_synthesis.rst
+
+if __name__ == '__main__':
+    from rvgen.dot2k import da2k, ha2k
+    from rvgen.generator import Monitor
+    from rvgen.container import Container
+    from rvgen.ltl2k import ltl2k
+    from rvgen.kunit import KUnit, KUnitError
+    from rvgen.automata import AutomataError
+    from rvgen.ltl2ba import LTLError
+    import argparse
+    import sys
+
+    parser = argparse.ArgumentParser(description='Generate kernel rv monitor')
+
+    parent_parser = argparse.ArgumentParser(add_help=False)
+    parent_parser.add_argument("-D", "--description", dest="description", required=False)
+    parent_parser.add_argument("-a", "--auto_patch", dest="auto_patch",
+                        action="store_true", required=False,
+                        help="Patch the kernel in place")
+
+    subparsers = parser.add_subparsers(dest="subcmd", required=True)
+
+    monitor_parser = subparsers.add_parser("monitor", parents=[parent_parser])
+    monitor_parser.add_argument('-n', "--model_name", dest="model_name")
+    monitor_parser.add_argument("-p", "--parent", dest="parent",
+                                required=False, help="Create a monitor nested to parent")
+    monitor_parser.add_argument('-c', "--class", dest="monitor_class", required=True,
+                                help="Monitor class, either \"da\", \"ha\" or \"ltl\"")
+    monitor_parser.add_argument('-s', "--spec", dest="spec", required=True,
+                                help="Monitor specification file")
+    monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type", required=True,
+                                help=f"Available options: {', '.join(Monitor.monitor_types.keys())}")
+
+    container_parser = subparsers.add_parser("container", parents=[parent_parser])
+    container_parser.add_argument('-n', "--model_name", dest="model_name", required=True)
+
+    kunit_parser = subparsers.add_parser("kunit", parents=[parent_parser])
+    kunit_parser.add_argument('-n', "--model_name", dest="model_name", required=True)
+    kunit_parser.add_argument('-l', "--local", dest="local", action="store_true", required=False,
+                               help="Force looking for the monitor in the current directory only")
+
+    params = parser.parse_args()
+
+    try:
+        if params.subcmd == "monitor":
+            print(f"Opening and parsing the specification file {params.spec}")
+            if params.monitor_class == "da":
+                monitor = da2k(params.spec, params.monitor_type, vars(params))
+            elif params.monitor_class == "ha":
+                monitor = ha2k(params.spec, params.monitor_type, vars(params))
+            elif params.monitor_class == "ltl":
+                monitor = ltl2k(params.spec, params.monitor_type, vars(params))
+            else:
+                print("Unknown monitor class:", params.monitor_class)
+                sys.exit(1)
+        elif params.subcmd == "container":
+            monitor = Container(vars(params))
+        elif params.subcmd == "kunit":
+            monitor = KUnit(vars(params))
+            monitor.print_files()
+            sys.exit(0)
+    except (AutomataError, LTLError) as e:
+        print(f"There was an error processing {params.spec}:\n{e}", file=sys.stderr)
+        sys.exit(1)
+    except KUnitError as e:
+        print(f"There was an error generating KUnit files:\n{e}", file=sys.stderr)
+        sys.exit(1)
+
+    print(f"Writing the monitor into the directory {monitor.name}")
+    monitor.print_files()
+    print("Almost done, checklist")
+    if params.subcmd == "monitor":
+        print(f"  - Edit the {monitor.name}/{monitor.name}.c to add the instrumentation")
+        print(monitor.fill_tracepoint_tooltip())
+    print(monitor.fill_makefile_tooltip())
+    print(monitor.fill_kconfig_tooltip())
+    print(monitor.fill_monitor_tooltip())
diff --git a/tools/verification/rvgen/dot2c b/tools/verification/rvgen/dot2c
new file mode 100644
index 000000000..1012becc7
--- /dev/null
+++ b/tools/verification/rvgen/dot2c
@@ -0,0 +1,25 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
+#
+# dot2c: parse an automata in dot file digraph format into a C
+#
+# This program was written in the development of this paper:
+#  de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S.
+#  "Efficient Formal Verification for the Linux Kernel." International
+#  Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.
+#
+# For further information, see:
+#   Documentation/trace/rv/deterministic_automata.rst
+
+if __name__ == '__main__':
+    from rvgen import dot2c
+    import argparse
+
+    parser = argparse.ArgumentParser(description='dot2c: converts a .dot file into a C structure')
+    parser.add_argument('dot_file',  help='The dot file to be converted')
+
+    args = parser.parse_args()
+    d = dot2c.Dot2c(args.dot_file)
+    d.print_model_classic()
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
new file mode 100644
index 000000000..fd37ce304
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -0,0 +1,549 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
+#
+# Automata class: parse an automaton in dot file digraph format into a python object
+#
+# For further information, see:
+#   Documentation/trace/rv/deterministic_automata.rst
+
+import ntpath
+
+import lark
+
+class ParseTree:
+    # based on https://graphviz.org/doc/info/lang.html
+    # with the irrelevant stuffs (port and compass) removed
+    grammar = r'''
+    start: "strict"? ("graph" | "digraph") ID? "{" stmt_list "}"
+
+    stmt_list: (stmt ";"? stmt_list)?
+
+    stmt: node_stmt
+        | edge_stmt
+        | attr_stmt
+        | ID "=" ID
+        | subgraph
+
+    attr_stmt: attr_type attr_list
+
+    attr_type: "graph" -> graph
+            | "node"  -> node
+            | "edge"  -> edge
+
+    attr_list: "[" a_list? "]" attr_list?
+
+    a_list: ID "=" ID (";" | ",")? a_list?
+
+    edge_stmt: (node_id | subgraph) edgerhs attr_list?
+
+    edgerhs: edgeop (node_id | subgraph) edgerhs?
+
+    edgeop: "->" | "--"
+
+    node_stmt: node_id attr_list?
+
+    node_id: ID
+
+    subgraph: ("subgraph" ID?)? "{" stmt_list "}"
+
+    ID: CNAME
+      | /-?(\.[0-9]+|[0-9]+(\.[0-9]*))/
+      | ESCAPED_STRING
+
+    %import common.CNAME
+    %import common.ESCAPED_STRING
+    %import common.WS
+    %ignore WS
+    '''
+
+    @staticmethod
+    def parse_edge(tree: lark.Tree) -> tuple[str, str]:
+        # only support a simple node-to-node edge
+        nodes = []
+        for node in tree.iter_subtrees_topdown():
+            if node.data == "node_id":
+                nodes.append(node.children[0].strip('"'))
+
+        if len(nodes) != 2:
+            raise AutomataError("Only state-to-state transition is supported")
+
+        return tuple(nodes)
+
+    class ParseNodes(lark.visitors.Visitor):
+        def __init__(self, *args, **kwargs):
+            self.nodes = set()
+            super().__init__(*args, **kwargs)
+
+        def node_stmt(self, tree):
+            node_id = tree.children[0]
+            node = node_id.children[0].strip('"')
+            self.nodes.add(node)
+
+    class ParseEdges(lark.visitors.Visitor):
+        def __init__(self, *args, **kwargs):
+            self.edges = set()
+            super().__init__(*args, **kwargs)
+
+        def edge_stmt(self, tree):
+            edge = ParseTree.parse_edge(tree)
+            self.edges.add(edge)
+
+    class ParseAttributes(lark.visitors.Interpreter):
+        def __init__(self, *args, **kwargs):
+            '''
+            Stacks of default attributes. [0] is the default
+            attributes for the outermost scope, while [-1] is the
+            default attributes for the current scope.
+            '''
+            self.default_node_attrs = [{}]
+            self.default_edge_attrs = [{}]
+
+            self.node_attrs = {}
+            self.edge_attrs = {}
+
+            super().__init__(*args, **kwargs)
+
+        @staticmethod
+        def __get_attrs(stmt: lark.Tree) -> dict[str, str]:
+            attrs = {}
+
+            for node in stmt.iter_subtrees():
+                if node.data == "a_list":
+                    attrs[node.children[0]] = node.children[1].strip('"')
+
+            return attrs
+
+
+        def subgraph(self, tree):
+            # We are entering a new scope, inherit the default
+            # attributes of the outer scope
+            self.default_node_attrs.append(self.default_node_attrs[-1].copy())
+            self.default_edge_attrs.append(self.default_edge_attrs[-1].copy())
+
+            children = self.visit_children(tree)
+
+            # Exiting the scope
+            del self.default_node_attrs[-1]
+            del self.default_edge_attrs[-1]
+
+            return children
+
+        def node_stmt(self, tree):
+            node_id = tree.children[0]
+            node = node_id.children[0].strip('"')
+
+            attrs = self.default_node_attrs[-1].copy()
+            attrs |= self.__get_attrs(tree)
+
+            if attrs:
+                if node in self.node_attrs:
+                    self.node_attrs[node] = attrs | self.node_attrs[node]
+                else:
+                    self.node_attrs[node] = attrs
+
+            return self.visit_children(tree)
+
+        def edge_stmt(self, tree):
+            edge = ParseTree.parse_edge(tree)
+
+            attrs = self.default_edge_attrs[-1].copy()
+            attrs |= self.__get_attrs(tree)
+
+            if attrs:
+                if edge in self.edge_attrs:
+                    self.edge_attrs[edge] = attrs | self.edge_attrs[edge]
+                else:
+                    self.edge_attrs[edge] = attrs
+
+            return self.visit_children(tree)
+
+        def attr_stmt(self, tree):
+            attr_type = tree.children[0].data
+            attrs = self.__get_attrs(tree)
+
+            if attr_type == "node":
+                self.default_node_attrs[-1] |= attrs
+            elif attr_type == "edge":
+                self.default_edge_attrs[-1] |= attrs
+            else:
+                # graph attributes are irrelevant
+                pass
+
+            self.visit_children(tree)
+
+    def __init__(self, dot_file):
+        parser = lark.Lark(self.grammar, parser='lalr')
+        node_parser = self.ParseNodes()
+        edge_parser = self.ParseEdges()
+        attributes_parser = self.ParseAttributes()
+
+        try:
+            with open(dot_file, "r") as f:
+                tree = parser.parse(f.read())
+                attributes_parser.visit(tree)
+                node_parser.visit(tree)
+                edge_parser.visit(tree)
+        except OSError as exc:
+            raise AutomataError(exc.strerror) from exc
+        except lark.exceptions.UnexpectedInput as exc:
+            raise AutomataError(str(exc))
+
+        self.nodes = node_parser.nodes
+        self.edges = edge_parser.edges
+        self.node_attrs = attributes_parser.node_attrs
+        self.edge_attrs = attributes_parser.edge_attrs
+
+class ConstraintCondition:
+    def __init__(self, env: str, op: str, val: str, unit=None):
+        self.env = env
+        self.op = op
+        self.val = val
+        self.unit = unit
+        if unit is None:
+            # try to infer unit from constants or parameters
+            val_for_unit = val.lower().replace("()", "")
+            if val_for_unit.endswith("_ns"):
+                self.unit = "ns"
+            if val_for_unit.endswith("_jiffies"):
+                self.unit = "j"
+
+class ConstraintRule:
+    grammar = r'''
+        rule: condition (OP condition)*
+
+        OP: "&&" | "||"
+
+        condition: ENV CMP_OP VAL UNIT?
+
+        ENV: CNAME
+
+        CMP_OP: "==" | "!=" | "<=" | "<" | ">=" | ">"
+
+        VAL: /[0-9]+/
+           | /[A-Z_]+\(\)/
+           | /[A-Z_]+/
+           | /[a-z_]+\(\)/
+           | /[a-z_]+/
+
+        UNIT: "ns" | "us" | "ms" | "s" | "j"
+    '''
+
+    def __init__(self, c: ConstraintCondition):
+        '''
+        A list of pairs of
+          - the condition (e.g. is_constr_dl == 1)
+          - the logical operator ("||" or "&&") combining this
+            condition with the next one if it exists, otherwise None
+
+        TODO: Perhaps use an abstract syntax tree instead, because
+              this representation cannot capture precedence
+        '''
+        self.rules = [[c, None]]
+
+    def chain(self, op: str, c: ConstraintCondition):
+        self.rules[-1][1] = op
+        self.rules.append([c, None])
+
+class ConstraintReset:
+    def __init__(self, env):
+        self.env = env
+
+class StateLabelParser:
+    grammar = r'''
+    label: CNAME ("\\n" condition)?
+
+    %import common.CNAME
+    %import common.WS
+    %ignore WS
+    ''' + ConstraintRule.grammar
+
+    parser = lark.Lark(grammar, parser='lalr', start="label")
+
+    def __init__(self, label: str):
+        try:
+            tree = self.parser.parse(label)
+        except lark.exceptions.UnexpectedInput as exc:
+            raise(AutomataError(f"Unrecognised state \"{label}\"\n{exc}"))
+
+        self.state = tree.children[0]
+        self.constraint = None
+
+        if len(tree.children) == 2:
+            self.constraint = ConstraintCondition(*tree.children[1].children)
+            if self.constraint.op not in ("<", "<="):
+                raise AutomataError("State constraints must be clock expirations like"
+                                    f" clk<N ({label})")
+
+class EventLabelParser:
+    grammar = r'''
+    events: event ("\\n" event)*
+
+    event: name (";" guard)?
+
+    guard: reset
+         | rule
+         | rule ";" reset
+         | reset ";" rule
+
+    name: CNAME
+
+    reset: "reset" "(" ENV ")"
+
+    %import common.CNAME
+    %import common.WS
+    %ignore WS
+    ''' + ConstraintRule.grammar
+
+    parser = lark.Lark(grammar, parser='lalr', start="events")
+
+    class GetEvents(lark.visitors.Transformer):
+        def guard(self, args):
+            reset = None
+            rule = None
+            for arg in args:
+                if arg.data == "reset":
+                    reset = ConstraintReset(arg.children[0])
+                elif arg.data == "rule":
+                    conditions = arg.children
+                    rule = ConstraintRule(conditions[0])
+                    for i in range(1, len(conditions), 2):
+                        rule.chain(conditions[i], conditions[i + 1])
+            return reset, rule
+
+        def OP(self, args):
+            return args
+
+        def condition(self, args):
+            return ConstraintCondition(*args)
+
+        def event(self, args):
+            assert(len(args) <= 2)
+            name = args[0]
+            rule, reset = None, None
+            if len(args) == 2:
+                reset, rule = args[1]
+            return name, reset, rule
+
+        def events(self, args):
+            return args
+
+        def name(self, args):
+            return args[0]
+
+    def __init__(self, label: str):
+        try:
+            tree = self.parser.parse(label)
+            self.events = self.GetEvents().transform(tree)
+        except lark.exceptions.UnexpectedInput as exc:
+            raise(AutomataError(f"Unrecognised event \"{label}\"\n{exc}"))
+
+class Transition:
+    def __init__(self, src: str, dst: str, event: str,
+                 reset: ConstraintReset, rule: ConstraintRule):
+        self.src = src
+        self.dst = dst
+        self.event = event
+        self.rule = rule
+        self.reset = reset
+
+class State:
+    def __init__(self, name: str, inv: ConstraintCondition):
+        self.name = name
+        self.inv = inv
+
+class AutomataError(Exception):
+    """Exception raised for errors in automata parsing and validation.
+
+    Raised when DOT file processing fails due to invalid format, I/O errors,
+    or malformed automaton definitions.
+    """
+
+class Automata:
+    """Automata class: Reads a dot file and parses it as an automaton.
+
+    It supports both deterministic and hybrid automata.
+
+    Attributes:
+        dot_file: A dot file with an state_automaton definition.
+    """
+
+    invalid_state_str = "INVALID_STATE"
+    init_marker = "__init_"
+
+    def __init__(self, file_path, model_name=None):
+        self.__dot_path = file_path
+        self.name = model_name or self.__get_model_name()
+        self.__parse_tree = ParseTree(file_path)
+        self.transitions = self.__parse_transitions()
+        self.states, self.initial_state, self.final_states = self.__parse_states()
+        self.env_types = {}
+        self.env_stored = set()
+        self.constraint_vars = set()
+        self.self_loop_reset_events = set()
+        self.events, self.envs = self.__get_event_variables()
+        self.function = self.__create_matrix()
+        self.events_start, self.events_start_run = self.__store_init_events()
+        self.env_stored = sorted(self.env_stored)
+        self.constraint_vars = sorted(self.constraint_vars)
+        self.self_loop_reset_events = sorted(self.self_loop_reset_events)
+
+    def __get_model_name(self) -> str:
+        basename = ntpath.basename(self.__dot_path)
+        if not basename.endswith(".dot") and not basename.endswith(".gv"):
+            print("not a dot file")
+            raise AutomataError(f"not a dot file: {self.__dot_path}")
+
+        model_name = ntpath.splitext(basename)[0]
+        if not model_name:
+            raise AutomataError(f"not a dot file: {self.__dot_path}")
+
+        return model_name
+
+    def __parse_transitions(self):
+        transitions = []
+
+        for edge in self.__parse_tree.edges:
+            attr = self.__parse_tree.edge_attrs.get(edge)
+            if not attr:
+                continue
+
+            label = attr.get("label")
+
+            src, dst = edge
+
+            parser = EventLabelParser(label)
+            for event, reset, rule in parser.events:
+                transitions.append(Transition(src, dst, event, reset, rule))
+
+        transitions.sort(key=lambda t : (t.src, t.event))
+        return transitions
+
+    def __parse_states(self):
+        initial_state = ""
+        states = []
+        final_states = []
+
+        for node in self.__parse_tree.nodes:
+            attr = self.__parse_tree.node_attrs[node]
+            label = attr.get("label")
+
+            if node.startswith(Automata.init_marker):
+                initial_state = node[len(Automata.init_marker):]
+
+            if not label:
+                continue
+
+            parser = StateLabelParser(label)
+            state = State(parser.state, parser.constraint)
+
+            states.append(state)
+
+            shape = attr.get("shape")
+            if shape in ("doublecircle", "ellipse"):
+                final_states.append(state)
+
+
+        initial_state = next((s for s in states if s.name == initial_state), None)
+        if not initial_state:
+            raise AutomataError("The automaton doesn't have an initial state")
+
+        if not final_states:
+            final_states.append(initial_state)
+
+        states.remove(initial_state)
+        states.sort(key=lambda s : s.name)
+        states.insert(0, initial_state)
+        return states, initial_state, final_states
+
+    def __get_event_variables(self) -> tuple[list[str], list[str]]:
+        events: list[str] = []
+        envs: list[str] = []
+
+        for transition in self.transitions:
+            events.append(transition.event)
+
+            if transition.reset:
+                envs.append(transition.reset.env)
+                self.env_stored.add(transition.reset.env)
+            if transition.rule:
+                for c, _ in transition.rule.rules:
+                    envs.append(c.env)
+                    self.__extract_env_var(c)
+
+        for state in self.states:
+            if state.inv:
+                envs.append(state.inv.env)
+                self.__extract_env_var(state.inv)
+
+        return sorted(set(events)), sorted(set(envs))
+
+    def __extract_env_var(self, constraint: ConstraintCondition):
+        if constraint.unit:
+            self.env_types[constraint.env] = constraint.unit
+        if constraint.val[0].isalpha():
+            self.constraint_vars.add(constraint.val)
+
+    def __create_matrix(self) -> list[list[str]]:
+        # transform the array into a dictionary
+        events = self.events
+        states = [s.name for s in self.states]
+        events_dict = {}
+        states_dict = {}
+        nr_event = 0
+        for event in events:
+            events_dict[event] = nr_event
+            nr_event += 1
+
+        nr_state = 0
+        for state in states:
+            states_dict[state] = nr_state
+            nr_state += 1
+
+        # declare the matrix....
+        matrix = [[self.invalid_state_str for _ in range(nr_event)] for _ in range(nr_state)]
+
+        for transition in self.transitions:
+            src, dst = transition.src, transition.dst
+            event = transition.event
+            if src == dst and transition.reset:
+                # those events reset also on self loops
+                self.self_loop_reset_events.add(event)
+            matrix[states_dict[src]][events_dict[event]] = dst
+
+        return matrix
+
+    def __store_init_events(self) -> tuple[list[bool], list[bool]]:
+        events_start = [False] * len(self.events)
+        events_start_run = [False] * len(self.events)
+        for i in range(len(self.events)):
+            curr_event_will_init = 0
+            curr_event_from_init = False
+            curr_event_used = 0
+            for j in range(len(self.states)):
+                if self.function[j][i] != self.invalid_state_str:
+                    curr_event_used += 1
+                if self.function[j][i] == self.initial_state.name:
+                    curr_event_will_init += 1
+            if self.function[0][i] != self.invalid_state_str:
+                curr_event_from_init = True
+            # this event always leads to init
+            if curr_event_will_init and curr_event_used == curr_event_will_init:
+                events_start[i] = True
+            # this event is only called from init
+            if curr_event_from_init and curr_event_used == 1:
+                events_start_run[i] = True
+        return events_start, events_start_run
+
+    def is_start_event(self, event: str) -> bool:
+        return self.events_start[self.events.index(event)]
+
+    def is_start_run_event(self, event: str) -> bool:
+        # prefer handle_start_event if there
+        if any(self.events_start):
+            return False
+        return self.events_start_run[self.events.index(event)]
+
+    def is_hybrid_automata(self) -> bool:
+        return bool(self.envs)
diff --git a/tools/verification/rvgen/rvgen/container.py b/tools/verification/rvgen/rvgen/container.py
new file mode 100644
index 000000000..51f188530
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/container.py
@@ -0,0 +1,32 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
+#
+# Generator for runtime verification monitor container
+
+from . import generator
+
+
+class Container(generator.RVGenerator):
+    template_dir = "container"
+
+    def __init__(self, extra_params={}):
+        super().__init__(extra_params)
+        self.name = extra_params.get("model_name")
+        self.main_h = self._read_template_file("main.h")
+
+    def fill_model_h(self):
+        main_h = self.main_h
+        main_h = main_h.replace("%%MODEL_NAME%%", self.name)
+        return main_h
+
+    def fill_kconfig_tooltip(self):
+        """Override to produce a marker for this container in the Kconfig"""
+        container_marker = self._kconfig_marker(self.name) + "\n"
+        result = super().fill_kconfig_tooltip()
+        if self.auto_patch:
+            self._patch_file("Kconfig",
+                             self._kconfig_marker(), container_marker)
+            return result
+        return result + container_marker
diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py
new file mode 100644
index 000000000..22938ce1b
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/dot2c.py
@@ -0,0 +1,268 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
+#
+# dot2c: parse an automaton in dot file digraph format into a C
+#
+# This program was written in the development of this paper:
+#  de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S.
+#  "Efficient Formal Verification for the Linux Kernel." International
+#  Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.
+#
+# For further information, see:
+#   Documentation/trace/rv/deterministic_automata.rst
+
+from .automata import Automata, AutomataError
+
+class Dot2c(Automata):
+    enum_suffix = ""
+    enum_states_def = "states"
+    enum_events_def = "events"
+    enum_envs_def = "envs"
+    struct_automaton_def = "automaton"
+    var_automaton_def = "aut"
+
+    def __init__(self, file_path, model_name=None):
+        super().__init__(file_path, model_name)
+        self.line_length = 100
+
+    def __get_enum_states_content(self) -> list[str]:
+        buff = []
+        buff.append(f"\t{self.initial_state.name}{self.enum_suffix},")
+        for state in self.states:
+            if state != self.initial_state:
+                buff.append(f"\t{state.name}{self.enum_suffix},")
+        buff.append(f"\tstate_max{self.enum_suffix},")
+
+        return buff
+
+    def format_states_enum(self) -> list[str]:
+        buff = []
+        buff.append(f"enum {self.enum_states_def} {{")
+        buff += self.__get_enum_states_content()
+        buff.append("};\n")
+
+        return buff
+
+    def __get_enum_events_content(self) -> list[str]:
+        buff = []
+        for event in self.events:
+            buff.append(f"\t{event}{self.enum_suffix},")
+
+        buff.append(f"\tevent_max{self.enum_suffix},")
+
+        return buff
+
+    def format_events_enum(self) -> list[str]:
+        buff = []
+        buff.append(f"enum {self.enum_events_def} {{")
+        buff += self.__get_enum_events_content()
+        buff.append("};\n")
+
+        return buff
+
+    def __get_non_stored_envs(self) -> list[str]:
+        return [e for e in self.envs if e not in self.env_stored]
+
+    def __get_enum_envs_content(self) -> list[str]:
+        buff = []
+        # We first place env variables that have a u64 storage.
+        # Those are limited by MAX_HA_ENV_LEN, other variables
+        # are read only and don't require a storage.
+        unstored = self.__get_non_stored_envs()
+        for env in list(self.env_stored) + unstored:
+            buff.append(f"\t{env}{self.enum_suffix},")
+
+        buff.append(f"\tenv_max{self.enum_suffix},")
+        max_stored = unstored[0] if len(unstored) else "env_max"
+        buff.append(f"\tenv_max_stored{self.enum_suffix} = {max_stored}{self.enum_suffix},")
+
+        return buff
+
+    def format_envs_enum(self) -> list[str]:
+        buff = []
+        if self.is_hybrid_automata():
+            buff.append(f"enum {self.enum_envs_def} {{")
+            buff += self.__get_enum_envs_content()
+            buff.append("};\n")
+            buff.append(f"_Static_assert(env_max_stored{self.enum_suffix} <= MAX_HA_ENV_LEN,"
+                        ' "Not enough slots");')
+            if {"ns", "us", "ms", "s"}.intersection(self.env_types.values()):
+                buff.append("#define HA_CLK_NS")
+            buff.append("")
+        return buff
+
+    def get_minimun_type(self) -> str:
+        min_type = "unsigned char"
+
+        if len(self.states) > 255:
+            min_type = "unsigned short"
+
+        if len(self.states) > 65535:
+            min_type = "unsigned int"
+
+        if len(self.states) > 1000000:
+            raise AutomataError(f"Too many states: {len(self.states)}")
+
+        return min_type
+
+    def format_automaton_definition(self) -> list[str]:
+        min_type = self.get_minimun_type()
+        buff = []
+        buff.append(f"struct {self.struct_automaton_def} {{")
+        buff.append(f"\tchar *state_names[state_max{self.enum_suffix}];")
+        buff.append(f"\tchar *event_names[event_max{self.enum_suffix}];")
+        if self.is_hybrid_automata():
+            buff.append(f"\tchar *env_names[env_max{self.enum_suffix}];")
+        buff.append(f"\t{min_type} function[state_max{self.enum_suffix}][event_max{self.enum_suffix}];")
+        buff.append(f"\t{min_type} initial_state;")
+        buff.append(f"\tbool final_states[state_max{self.enum_suffix}];")
+        buff.append("};\n")
+        return buff
+
+    def format_aut_init_header(self) -> list[str]:
+        buff = []
+        buff.append(f"static const struct {self.struct_automaton_def} {self.var_automaton_def} = {{")
+        return buff
+
+    def __get_string_vector_per_line_content(self, entries: list[str]) -> str:
+        buff = []
+        for entry in entries:
+            buff.append(f"\t\t\"{entry}\",")
+        return "\n".join(buff)
+
+    def format_aut_init_events_string(self) -> list[str]:
+        buff = []
+        buff.append("\t.event_names = {")
+        buff.append(self.__get_string_vector_per_line_content(self.events))
+        buff.append("\t},")
+        return buff
+
+    def format_aut_init_states_string(self) -> list[str]:
+        buff = []
+        buff.append("\t.state_names = {")
+        buff.append(self.__get_string_vector_per_line_content([s.name for s in self.states]))
+        buff.append("\t},")
+
+        return buff
+
+    def format_aut_init_envs_string(self) -> list[str]:
+        buff = []
+        if self.is_hybrid_automata():
+            buff.append("\t.env_names = {")
+            # maintain consistent order with the enum
+            ordered_envs = list(self.env_stored) + self.__get_non_stored_envs()
+            buff.append(self.__get_string_vector_per_line_content(ordered_envs))
+            buff.append("\t},")
+
+        return buff
+
+    def __get_max_strlen_of_states(self) -> int:
+        max_state_name = max((len(s.name) for s in self.states))
+        return max(max_state_name, len(self.invalid_state_str))
+
+    def get_aut_init_function(self) -> str:
+        nr_states = len(self.states)
+        nr_events = len(self.events)
+        buff = []
+
+        maxlen = self.__get_max_strlen_of_states() + len(self.enum_suffix)
+        tab_braces = 2 * 8 + 2 + 1  # "\t\t{ " ... "}"
+        comma_space = 2  # ", " count last comma here
+        linetoolong = tab_braces + (maxlen + comma_space) * nr_events > self.line_length
+        for x in range(nr_states):
+            line = "\t\t{\n" if linetoolong else "\t\t{ "
+            for y in range(nr_events):
+                next_state = self.function[x][y]
+                if next_state != self.invalid_state_str:
+                    next_state = self.function[x][y] + self.enum_suffix
+
+                if linetoolong:
+                    line += f"\t\t\t{next_state}"
+                else:
+                    line += f"{next_state:>{maxlen}}"
+                if y != nr_events - 1:
+                    line += ",\n" if linetoolong else ", "
+                else:
+                    line += ",\n\t\t}," if linetoolong else " },"
+            buff.append(line)
+
+        return '\n'.join(buff)
+
+    def format_aut_init_function(self) -> list[str]:
+        buff = []
+        buff.append("\t.function = {")
+        buff.append(self.get_aut_init_function())
+        buff.append("\t},")
+
+        return buff
+
+    def get_aut_init_initial_state(self) -> str:
+        return self.initial_state.name
+
+    def format_aut_init_initial_state(self) -> list[str]:
+        buff = []
+        initial_state = self.get_aut_init_initial_state()
+        buff.append("\t.initial_state = " + initial_state + self.enum_suffix + ",")
+
+        return buff
+
+    def get_aut_init_final_states(self) -> str:
+        line = ""
+        first = True
+        for state in self.states:
+            if not first:
+                line = line + ', '
+            else:
+                first = False
+
+            if state in self.final_states:
+                line = line + '1'
+            else:
+                line = line + '0'
+        return line
+
+    def format_aut_init_final_states(self) -> list[str]:
+       buff = []
+       buff.append(f"\t.final_states = {{ {self.get_aut_init_final_states()} }},")
+
+       return buff
+
+    def __get_automaton_initialization_footer_string(self) -> str:
+        footer = "};\n"
+        return footer
+
+    def format_aut_init_footer(self) -> list[str]:
+        buff = []
+        buff.append(self.__get_automaton_initialization_footer_string())
+
+        return buff
+
+    def format_invalid_state(self) -> list[str]:
+        buff = []
+        buff.append(f"#define {self.invalid_state_str} state_max{self.enum_suffix}\n")
+
+        return buff
+
+    def format_model(self) -> list[str]:
+        buff = []
+        buff += self.format_states_enum()
+        buff += self.format_invalid_state()
+        buff += self.format_events_enum()
+        buff += self.format_envs_enum()
+        buff += self.format_automaton_definition()
+        buff += self.format_aut_init_header()
+        buff += self.format_aut_init_states_string()
+        buff += self.format_aut_init_events_string()
+        buff += self.format_aut_init_envs_string()
+        buff += self.format_aut_init_function()
+        buff += self.format_aut_init_initial_state()
+        buff += self.format_aut_init_final_states()
+        buff += self.format_aut_init_footer()
+
+        return buff
+
+    def print_model_classic(self):
+        buff = self.format_model()
+        print('\n'.join(buff))
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
new file mode 100644
index 000000000..fd3254ea5
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -0,0 +1,512 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
+#
+# dot2k: transform dot files into a monitor for the Linux kernel.
+#
+# For further information, see:
+#   Documentation/trace/rv/monitor_synthesis.rst
+
+from .dot2c import Dot2c
+from .generator import Monitor
+from .automata import ConstraintCondition, AutomataError
+
+class dot2k(Monitor, Dot2c):
+    template_dir = "dot2k"
+
+    # only needed for the per-obj cleanup hook
+    cleanup_marker = "obj_cleanup"
+
+    def __init__(self, file_path, MonitorType, extra_params={}):
+        self.monitor_type = MonitorType
+        Monitor.__init__(self, extra_params)
+        Dot2c.__init__(self, file_path, extra_params.get("model_name"))
+        self.enum_suffix = f"_{self.name}"
+        self.enum_suffix = f"_{self.name}"
+        self.monitor_class = extra_params["monitor_class"]
+
+    def fill_monitor_type(self) -> str:
+        buff = [ self.monitor_type.upper() ]
+        buff += self._fill_timer_type()
+        if self.monitor_type == "per_obj":
+            buff.append("typedef /* XXX: define the target type */ *monitor_target;")
+        return "\n".join(buff)
+
+    def fill_tracepoint_handlers_skel(self) -> str:
+        buff = []
+        buff += self._fill_hybrid_definitions()
+        for event in self.events:
+            buff.append(f"static void handle_{event}(void *data, /* XXX: fill header */)")
+            buff.append("{")
+            handle = "handle_event"
+            if self.is_start_event(event):
+                buff.append("\t/* XXX: validate that this event always leads to the initial state */")
+                handle = "handle_start_event"
+            elif self.is_start_run_event(event):
+                buff.append("\t/* XXX: validate that this event is only valid in the initial state */")
+                handle = "handle_start_run_event"
+            if self.monitor_type == "per_task":
+                buff.append("\tstruct task_struct *p = /* XXX: how do I get p? */;")
+                buff.append(f"\tda_{handle}(p, {event}{self.enum_suffix});")
+            elif self.monitor_type == "per_obj":
+                buff.append("\tint id = /* XXX: how do I get the id? */;")
+                buff.append("\tmonitor_target t = /* XXX: how do I get t? */;")
+                buff.append(f"\tda_{handle}(id, t, {event}{self.enum_suffix});")
+            else:
+                buff.append(f"\tda_{handle}({event}{self.enum_suffix});")
+            buff.append("}")
+            buff.append("")
+        if self.monitor_type == "per_obj":
+            buff.append("/* XXX: obj is being destroyed, remove if not required (e.g. obj is static) */")
+            buff.append(f"static void handle_{self.cleanup_marker}(void *data, /* XXX: fill header */)")
+            buff.append("{")
+            buff.append("\tint id = /* XXX: how do I get the id? */;")
+            buff.append("\tda_destroy_storage(id);")
+            buff.append("}")
+            buff.append("")
+        return '\n'.join(buff)
+
+    def fill_tracepoint_attach_probe(self) -> str:
+        buff = []
+        for event in self.events:
+            buff.append(f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_{event});")
+        if self.monitor_type == "per_obj":
+            buff.append(f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: cleanup tracepoint */, handle_{self.cleanup_marker});")
+        return '\n'.join(buff)
+
+    def fill_tracepoint_detach_helper(self) -> str:
+        buff = []
+        for event in self.events:
+            buff.append(f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_{event});")
+        if self.monitor_type == "per_obj":
+            buff.append(f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: cleanup tracepoint */, handle_{self.cleanup_marker});")
+        return '\n'.join(buff)
+
+    def fill_model_h_header(self) -> list[str]:
+        buff = []
+        buff.append("/* SPDX-License-Identifier: GPL-2.0 */")
+        buff.append("/*")
+        buff.append(f" * Automatically generated C representation of {self.name} automaton")
+        buff.append(" * For further information about this format, see kernel documentation:")
+        buff.append(" *   Documentation/trace/rv/deterministic_automata.rst")
+        buff.append(" */")
+        buff.append("")
+        buff.append(f"#define MONITOR_NAME {self.name}")
+        buff.append("")
+
+        return buff
+
+    def fill_model_h(self) -> str:
+        #
+        # Adjust the definition names
+        #
+        self.enum_states_def = f"states_{self.name}"
+        self.enum_events_def = f"events_{self.name}"
+        self.enum_envs_def = f"envs_{self.name}"
+        self.struct_automaton_def = f"automaton_{self.name}"
+        self.var_automaton_def = f"automaton_{self.name}"
+
+        buff = self.fill_model_h_header()
+        buff += self.format_model()
+
+        return '\n'.join(buff)
+
+    def _is_id_monitor(self) -> bool:
+        return self.monitor_type in ("per_task", "per_obj")
+
+    def fill_monitor_class_type(self) -> str:
+        if self._is_id_monitor():
+            return "DA_MON_EVENTS_ID"
+        return "DA_MON_EVENTS_IMPLICIT"
+
+    def fill_monitor_class(self) -> str:
+        if self._is_id_monitor():
+            return "da_monitor_id"
+        return "da_monitor"
+
+    def fill_tracepoint_args_skel(self, tp_type: str) -> str:
+        buff = []
+        tp_args_event = [
+                ("char *", "state"),
+                ("char *", "event"),
+                ("char *", "next_state"),
+                ("bool ",  "final_state"),
+                ]
+        tp_args_error = [
+                ("char *", "state"),
+                ("char *", "event"),
+                ]
+        tp_args_error_env = tp_args_error + [("char *", "env")]
+        tp_args_dict = {
+                "event": tp_args_event,
+                "error": tp_args_error,
+                "error_env": tp_args_error_env
+                }
+        tp_args_id = ("int ", "id")
+        tp_args = tp_args_dict[tp_type]
+        if self._is_id_monitor():
+            tp_args.insert(0, tp_args_id)
+        tp_proto_c = ", ".join([a + b for a, b in tp_args])
+        tp_args_c = ", ".join([b for a, b in tp_args])
+        buff.append(f"	     TP_PROTO({tp_proto_c}),")
+        buff.append(f"	     TP_ARGS({tp_args_c})")
+        return '\n'.join(buff)
+
+    def _fill_hybrid_definitions(self) -> list:
+        """Stub, not valid for deterministic automata"""
+        return []
+
+    def _fill_timer_type(self) -> list:
+        """Stub, not valid for deterministic automata"""
+        return []
+
+    def fill_main_c(self) -> str:
+        main_c = super().fill_main_c()
+
+        min_type = self.get_minimun_type()
+        nr_events = len(self.events)
+        monitor_type = self.fill_monitor_type()
+
+        main_c = main_c.replace("%%MIN_TYPE%%", min_type)
+        main_c = main_c.replace("%%NR_EVENTS%%", str(nr_events))
+        main_c = main_c.replace("%%MONITOR_TYPE%%", monitor_type)
+        main_c = main_c.replace("%%MONITOR_CLASS%%", self.monitor_class)
+
+        return main_c
+
+class da2k(dot2k):
+    """Deterministic automata only"""
+    def __init__(self, *args, **kwargs):
+        super().__init__(*args, **kwargs)
+        if self.is_hybrid_automata():
+            raise AutomataError("Detected hybrid automaton, use the 'ha' class")
+
+class ha2k(dot2k):
+    """Hybrid automata only"""
+    def __init__(self, *args, **kwargs):
+        super().__init__(*args, **kwargs)
+        if not self.is_hybrid_automata():
+            raise AutomataError("Detected deterministic automaton, use the 'da' class")
+        self.trace_h = self._read_template_file("trace_hybrid.h")
+        self.has_invariant = False
+        self.has_guard = False
+        for state in self.states:
+            if state.inv:
+                self.has_invariant = True
+        for transition in self.transitions:
+            if transition.rule or transition.reset:
+                self.has_guard = True
+
+    def fill_monitor_class_type(self) -> str:
+        if self._is_id_monitor():
+            return "HA_MON_EVENTS_ID"
+        return "HA_MON_EVENTS_IMPLICIT"
+
+    def fill_monitor_class(self) -> str:
+        """
+        Used for tracepoint classes, since they are shared we keep da
+        instead of ha (also for the ha specific tracepoints).
+        The tracepoint class is not visible to the tools.
+        """
+        return super().fill_monitor_class()
+
+    def __adjust_value(self, value: str | int, unit: str | None) -> str:
+        """Adjust the value in ns"""
+        try:
+            value = int(value)
+        except ValueError:
+            # it's a constant, a parameter or a function
+            if value.endswith("()"):
+                return value.replace("()", "(ha_mon)")
+            return value
+        match unit:
+            case "us":
+                value *= 10**3
+            case "ms":
+                value *= 10**6
+            case "s":
+                value *= 10**9
+        return str(value) + "ull"
+
+    def __parse_guard_rule(self, rule) -> list[str]:
+        buff = []
+        for c, sep in rule.rules:
+            env = c.env + self.enum_suffix
+            op = c.op
+            val = self.__adjust_value(c.val, c.unit)
+
+            cond = f"ha_get_env(ha_mon, {env}, time_ns) {op} {val}"
+            if sep:
+                cond += f" {sep}"
+            buff.append(cond)
+        return buff
+
+    def __start_to_invariant_check(self, inv: ConstraintCondition) -> str:
+        # by default assume the timer has ns expiration
+        clock_type = "ns"
+        if inv.unit == "j":
+            clock_type = "jiffy"
+
+        value = self.__adjust_value(inv.val, inv.unit)
+
+        return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_{self.name}, time_ns, {value})"
+
+    def __parse_invariant(self, inv):
+        # by default assume the timer has ns expiration
+        clock_type = "ns"
+        if inv.unit == "j":
+            clock_type = "jiffy"
+
+        env = inv.env + self.enum_suffix
+        try:
+            val = int(inv.val)
+        except ValueError:
+            # it's a constant, a parameter or a function
+            val = inv.val.replace("()", "(ha_mon)")
+
+        match inv.unit:
+            case "us":
+                val *= 10**3
+            case "ms":
+                val *= 10**6
+            case "s":
+                val *= 10**9
+
+        return (f"ha_start_timer_{clock_type}(ha_mon, {env},"
+                f" {val}, time_ns)")
+
+    def __format_guard_rules(self, rules: list[str]) -> list[str]:
+        """
+        Merge guard constraints as a single C return statement.
+        If the rules include a stored env, also check its validity.
+        Break lines in a best effort way that tries to keep readability.
+        """
+        if not rules:
+            return []
+
+        invalid_checks = [f"ha_monitor_env_invalid(ha_mon, {env}{self.enum_suffix}) ||"
+                          for env in self.env_stored if any(env in rule for rule in rules)]
+        if invalid_checks and len(rules) > 1:
+            rules[0] = "(" + rules[0]
+            rules[-1] = rules[-1] + ")"
+        rules = invalid_checks + rules
+
+        separator = "\n\t\t      " if sum(len(r) for r in rules) > 80 else " "
+        return ["res = " + separator.join(rules) + ";"]
+
+    def __fill_verify_invariants_func(self) -> list[str]:
+        if not self.has_invariant:
+            return []
+
+        buff = [
+f"""static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
+\t\t\t\t\tenum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
+\t\t\t\t\tenum {self.enum_states_def} next_state, u64 time_ns)
+{{"""]
+
+        _else = ""
+        for state in self.states:
+            if not state.inv:
+                continue
+
+            check_str = self.__start_to_invariant_check(state.inv)
+            buff.append(f"\t{_else}if (curr_state == {state.name}{self.enum_suffix})")
+            buff.append(f"\t\t{check_str};")
+            _else = "else "
+
+        buff.append("\treturn true;\n}\n")
+        return buff
+
+    def __fill_verify_guards_func(self) -> list[str]:
+        buff = []
+
+        if not self.has_guard:
+            return []
+
+        buff.append(
+f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
+\t\t\t\t    enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
+\t\t\t\t    enum {self.enum_states_def} next_state, u64 time_ns)
+{{
+\tbool res = true;
+""")
+
+        _else = ""
+        for transition in self.transitions:
+            if not transition.rule and not transition.reset:
+                continue
+
+            buff.append(f"\t{_else}if (curr_state == "
+                        f"{transition.src}{self.enum_suffix} && "
+                        f"event == {transition.event}{self.enum_suffix})")
+            rule = transition.rule
+            reset = transition.reset
+            if rule and reset:
+                buff[-1] += " {"
+            if rule:
+                buff.append("\t\t" + self.__format_guard_rules(self.__parse_guard_rule(rule))[0])
+            if reset:
+                buff.append(f"\t\tha_reset_env(ha_mon, {reset.env}{self.enum_suffix}, time_ns);")
+            if rule and reset:
+                _else = "} else "
+            else:
+                _else = "else "
+        if _else[0] == "}":
+            buff.append("\t}")
+        buff.append("\treturn res;\n}\n")
+        return buff
+
+    def __fill_setup_invariants_func(self) -> list[str]:
+        if not self.has_invariant:
+            return []
+
+        buff = [
+f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
+\t\t\t\t       enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
+\t\t\t\t       enum {self.enum_states_def} next_state, u64 time_ns)
+{{"""]
+
+        conditions = ["next_state == curr_state"]
+        conditions += [f"event != {e}{self.enum_suffix}"
+                       for e in self.self_loop_reset_events]
+        condition_str = " && ".join(conditions)
+        buff.append(f"\tif ({condition_str})\n\t\treturn;")
+
+        _else = ""
+        for state in self.states:
+            inv = state.inv
+            if not inv:
+                continue
+            inv = self.__parse_invariant(inv)
+            buff.append(f"\t{_else}if (next_state == {state.name}{self.enum_suffix})")
+            buff.append(f"\t\t{inv};")
+            _else = "else "
+
+        for state in self.states:
+            inv = state.inv
+            if not inv:
+                continue
+            buff.append(f"\telse if (curr_state == {state.name}{self.enum_suffix})")
+            buff.append("\t\tha_cancel_timer(ha_mon);")
+
+        buff.append("}\n")
+        return buff
+
+    def __fill_constr_func(self) -> list[str]:
+        buff = []
+        if not self.has_invariant and not self.has_guard:
+            return []
+
+        buff.append(
+"""/*
+ * These functions are used to validate state transitions.
+ *
+ * They are generated by parsing the model, there is usually no need to change them.
+ * If the monitor requires a timer, there are functions responsible to arm it when
+ * the next state has a constraint, cancel it in any other case and to check
+ * that it didn't expire before the callback run. Transitions to the same state
+ * without a reset never affect timers.
+ */""")
+
+        buff += self.__fill_verify_invariants_func()
+        buff += self.__fill_verify_guards_func()
+        buff += self.__fill_setup_invariants_func()
+
+        buff.append(
+f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon,
+\t\t\t\t enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
+\t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns)
+{{""")
+
+        if self.has_invariant:
+            buff.append("\tif (!ha_verify_invariants(ha_mon, curr_state, "
+                        "event, next_state, time_ns))\n\t\treturn false;\n")
+
+        if self.has_guard:
+            buff.append("\tif (!ha_verify_guards(ha_mon, curr_state, event, "
+                        "next_state, time_ns))\n\t\treturn false;\n")
+
+        if self.has_invariant:
+            buff.append("\tha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns);\n")
+
+        buff.append("\treturn true;\n}\n")
+        return buff
+
+    def __fill_env_getter(self, env: str) -> str:
+        if env in self.env_types:
+            match self.env_types[env]:
+                case "ns" | "us" | "ms" | "s":
+                    return "ha_get_clk_ns(ha_mon, env, time_ns);"
+                case "j":
+                    return "ha_get_clk_jiffy(ha_mon, env);"
+        return f"/* XXX: how do I read {env}? */"
+
+    def __fill_env_resetter(self, env: str) -> str:
+        if env in self.env_types:
+            match self.env_types[env]:
+                case "ns" | "us" | "ms" | "s":
+                    return "ha_reset_clk_ns(ha_mon, env, time_ns);"
+                case "j":
+                    return "ha_reset_clk_jiffy(ha_mon, env);"
+        return f"/* XXX: how do I reset {env}? */"
+
+    def __fill_hybrid_get_reset_functions(self) -> list[str]:
+        buff = []
+        if self.is_hybrid_automata():
+            for var in self.constraint_vars:
+                if var.endswith("()"):
+                    func_name = var.replace("()", "")
+                    if func_name.isupper():
+                        buff.append(f"#define {func_name}(ha_mon) "
+                                    f"/* XXX: what is {func_name}(ha_mon)? */\n")
+                    else:
+                        buff.append(f"static inline u64 {func_name}(struct ha_monitor *ha_mon)\n{{")
+                        buff.append(f"\treturn /* XXX: what is {func_name}(ha_mon)? */;")
+                        buff.append("}\n")
+                elif var.isupper():
+                    buff.append(f"#define {var} /* XXX: what is {var}? */\n")
+                else:
+                    buff.append(f"static u64 {var} = /* XXX: default value */;")
+                    buff.append(f"module_param({var}, ullong, 0644);\n")
+            buff.append("""/*
+ * These functions define how to read and reset the environment variable.
+ *
+ * Common environment variables like ns-based and jiffy-based clocks have
+ * pre-define getters and resetters you can use. The parser can infer the type
+ * of the environment variable if you supply a measure unit in the constraint.
+ * If you define your own functions, make sure to add appropriate memory
+ * barriers if required.
+ * Some environment variables don't require a storage as they read a system
+ * state (e.g. preemption count). Those variables are never reset, so we don't
+ * define a reset function on monitors only relying on this type of variables.
+ */""")
+            buff.append("static u64 ha_get_env(struct ha_monitor *ha_mon, "
+                        f"enum envs{self.enum_suffix} env, u64 time_ns)\n{{")
+            _else = ""
+            for env in self.envs:
+                buff.append(f"\t{_else}if (env == {env}{self.enum_suffix})")
+                buff.append(f"\t\treturn {self.__fill_env_getter(env)}")
+                _else = "else "
+            buff.append("\treturn ENV_INVALID_VALUE;\n}\n")
+            if len(self.env_stored):
+                buff.append("static void ha_reset_env(struct ha_monitor *ha_mon, "
+                            f"enum envs{self.enum_suffix} env, u64 time_ns)\n{{")
+                _else = ""
+                for env in self.env_stored:
+                    buff.append(f"\t{_else}if (env == {env}{self.enum_suffix})")
+                    buff.append(f"\t\t{self.__fill_env_resetter(env)}")
+                    _else = "else "
+                buff.append("}\n")
+        return buff
+
+    def _fill_hybrid_definitions(self) -> list[str]:
+        return self.__fill_hybrid_get_reset_functions() + self.__fill_constr_func()
+
+    def _fill_timer_type(self) -> list:
+        if self.has_invariant:
+            return [
+                    "/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */",
+                    "#define HA_TIMER_TYPE HA_TIMER_HRTIMER"
+                    ]
+        return []
diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py
new file mode 100644
index 000000000..45e2bab26
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/generator.py
@@ -0,0 +1,250 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
+#
+# Abstract class for generating kernel runtime verification monitors from specification file
+
+import platform
+from pathlib import Path
+
+
+class RVGenerator:
+    rv_dir = "kernel/trace/rv"
+
+    def __init__(self, extra_params={}):
+        self.name = extra_params.get("model_name")
+        self.parent = extra_params.get("parent")
+        self.abs_template_dir = \
+            Path(__file__).resolve().parent / "templates" / self.template_dir
+        self.main_c = self._read_template_file("main.c")
+        self.kconfig = self._read_template_file("Kconfig")
+        self.description = extra_params.get("description", self.name) or "auto-generated"
+        self.auto_patch = extra_params.get("auto_patch")
+        if self.auto_patch:
+            self._fill_rv_kernel_dir()
+
+    def _fill_rv_kernel_dir(self):
+        # find the kernel tree root relative to this file's location
+        resolved_path = Path(__file__).resolve()
+        if len(resolved_path.parents) > 4:
+            kernel_root = resolved_path.parents[4]
+            kernel_path = kernel_root / self.rv_dir
+
+            if kernel_path.exists():
+                self.rv_dir = str(kernel_path)
+                return
+
+        # best effort if rvgen is installed and we are at the root of a kernel tree
+        if Path(self.rv_dir).exists():
+            return
+
+        if platform.system() != "Linux":
+            raise OSError("I can only run on Linux.")
+
+        kernel_path = Path(f"/lib/modules/{platform.release()}/build") / self.rv_dir
+
+        # if the current kernel is from a distro this may not be a full kernel tree
+        # verify that one of the files we are going to modify is available
+        if (kernel_path / "rv_trace.h").exists():
+            self.rv_dir = str(kernel_path)
+            return
+
+        raise FileNotFoundError("Could not find the rv directory, do you have the kernel source installed?")
+
+    def _read_file(self, path):
+        with open(path, 'r') as fd:
+            content = fd.read()
+        return content
+
+    def _read_template_file(self, file):
+        try:
+            path = self.abs_template_dir / file
+            return self._read_file(path)
+        except OSError:
+            # Specific template file not found. Try the generic template file in the template/
+            # directory, which is one level up
+            path = self.abs_template_dir.parent / file
+            return self._read_file(path)
+
+    def fill_parent(self):
+        return f"&rv_{self.parent}" if self.parent else "NULL"
+
+    def fill_include_parent(self):
+        if self.parent:
+            return f"#include <monitors/{self.parent}/{self.parent}.h>\n"
+        return ""
+
+    def fill_tracepoint_handlers_skel(self):
+        return "NotImplemented"
+
+    def fill_tracepoint_attach_probe(self):
+        return "NotImplemented"
+
+    def fill_tracepoint_detach_helper(self):
+        return "NotImplemented"
+
+    def fill_main_c(self):
+        main_c = self.main_c
+        tracepoint_handlers = self.fill_tracepoint_handlers_skel()
+        tracepoint_attach = self.fill_tracepoint_attach_probe()
+        tracepoint_detach = self.fill_tracepoint_detach_helper()
+        parent = self.fill_parent()
+        parent_include = self.fill_include_parent()
+
+        main_c = main_c.replace("%%MODEL_NAME%%", self.name)
+        main_c = main_c.replace("%%TRACEPOINT_HANDLERS_SKEL%%", tracepoint_handlers)
+        main_c = main_c.replace("%%TRACEPOINT_ATTACH%%", tracepoint_attach)
+        main_c = main_c.replace("%%TRACEPOINT_DETACH%%", tracepoint_detach)
+        main_c = main_c.replace("%%DESCRIPTION%%", self.description)
+        main_c = main_c.replace("%%PARENT%%", parent)
+        main_c = main_c.replace("%%INCLUDE_PARENT%%", parent_include)
+
+        return main_c
+
+    def fill_model_h(self):
+        return "NotImplemented"
+
+    def fill_monitor_class_type(self):
+        return "NotImplemented"
+
+    def fill_monitor_class(self):
+        return "NotImplemented"
+
+    def fill_tracepoint_args_skel(self, tp_type):
+        return "NotImplemented"
+
+    def fill_monitor_deps(self):
+        buff = []
+        buff.append("	# XXX: add dependencies if there")
+        if self.parent:
+            buff.append(f"	depends on RV_MON_{self.parent.upper()}")
+            buff.append("	default y")
+        return '\n'.join(buff)
+
+    def fill_kconfig(self):
+        kconfig = self.kconfig
+        monitor_class_type = self.fill_monitor_class_type()
+        monitor_deps = self.fill_monitor_deps()
+        kconfig = kconfig.replace("%%MODEL_NAME%%", self.name)
+        kconfig = kconfig.replace("%%MODEL_NAME_UP%%", self.name.upper())
+        kconfig = kconfig.replace("%%MONITOR_CLASS_TYPE%%", monitor_class_type)
+        kconfig = kconfig.replace("%%DESCRIPTION%%", self.description)
+        kconfig = kconfig.replace("%%MONITOR_DEPS%%", monitor_deps)
+        return kconfig
+
+    def _patch_file(self, file, marker, line):
+        assert self.auto_patch
+        file_to_patch = Path(self.rv_dir) / file
+        content = self._read_file(file_to_patch)
+        content = content.replace(marker, line + "\n" + marker)
+        self.__write_file(file_to_patch, content)
+
+    def fill_tracepoint_tooltip(self):
+        monitor_class_type = self.fill_monitor_class_type()
+        if self.auto_patch:
+            self._patch_file("rv_trace.h",
+                            f"// Add new monitors based on CONFIG_{monitor_class_type} here",
+                            f"#include <monitors/{self.name}/{self.name}_trace.h>")
+            return f"  - Patching {self.rv_dir}/rv_trace.h, double check the result"
+
+        return f"""  - Edit {self.rv_dir}/rv_trace.h:
+Add this line where other tracepoints are included and {monitor_class_type} is defined:
+#include <monitors/{self.name}/{self.name}_trace.h>
+"""
+
+    def _kconfig_marker(self, container=None) -> str:
+        return f"# Add new {container + ' ' if container else ''}monitors here"
+
+    def fill_kconfig_tooltip(self):
+        if self.auto_patch:
+            # monitors with a container should stay together in the Kconfig
+            self._patch_file("Kconfig",
+                             self._kconfig_marker(self.parent),
+                            f"source \"kernel/trace/rv/monitors/{self.name}/Kconfig\"")
+            return f"  - Patching {self.rv_dir}/Kconfig, double check the result"
+
+        return f"""  - Edit {self.rv_dir}/Kconfig:
+Add this line where other monitors are included:
+source \"kernel/trace/rv/monitors/{self.name}/Kconfig\"
+"""
+
+    def fill_makefile_tooltip(self):
+        name = self.name
+        name_up = name.upper()
+        if self.auto_patch:
+            self._patch_file("Makefile",
+                            "# Add new monitors here",
+                            f"obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o")
+            return f"  - Patching {self.rv_dir}/Makefile, double check the result"
+
+        return f"""  - Edit {self.rv_dir}/Makefile:
+Add this line where other monitors are included:
+obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o
+"""
+
+    def fill_monitor_tooltip(self):
+        if self.auto_patch:
+            return f"  - Monitor created in {self.rv_dir}/monitors/{self.name}"
+        return f"  - Move {self.name}/ to the kernel's monitor directory ({self.rv_dir}/monitors)"
+
+    def __create_directory(self):
+        path = Path(self.name)
+        if self.auto_patch:
+            path = Path(self.rv_dir) / "monitors" / path
+        path.mkdir(exist_ok=True)
+
+    def __write_file(self, file_name, content):
+        with open(file_name, 'w') as file:
+            file.write(content)
+
+    def _create_file(self, file_name, content):
+        path = Path(self.name) / file_name
+        if self.auto_patch:
+            path = Path(self.rv_dir) / "monitors" / self.name / file_name
+        self.__write_file(path, content)
+
+    def print_files(self):
+        main_c = self.fill_main_c()
+
+        self.__create_directory()
+
+        path = f"{self.name}.c"
+        self._create_file(path, main_c)
+
+        model_h = self.fill_model_h()
+        path = f"{self.name}.h"
+        self._create_file(path, model_h)
+
+        kconfig = self.fill_kconfig()
+        self._create_file("Kconfig", kconfig)
+
+
+class Monitor(RVGenerator):
+    monitor_types = {"global": 1, "per_cpu": 2, "per_task": 3, "per_obj": 4}
+
+    def __init__(self, extra_params={}):
+        super().__init__(extra_params)
+        self.trace_h = self._read_template_file("trace.h")
+
+    def fill_trace_h(self):
+        trace_h = self.trace_h
+        monitor_class = self.fill_monitor_class()
+        monitor_class_type = self.fill_monitor_class_type()
+        tracepoint_args_skel_event = self.fill_tracepoint_args_skel("event")
+        tracepoint_args_skel_error = self.fill_tracepoint_args_skel("error")
+        tracepoint_args_skel_error_env = self.fill_tracepoint_args_skel("error_env")
+        trace_h = trace_h.replace("%%MODEL_NAME%%", self.name)
+        trace_h = trace_h.replace("%%MODEL_NAME_UP%%", self.name.upper())
+        trace_h = trace_h.replace("%%MONITOR_CLASS%%", monitor_class)
+        trace_h = trace_h.replace("%%MONITOR_CLASS_TYPE%%", monitor_class_type)
+        trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_EVENT%%", tracepoint_args_skel_event)
+        trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_ERROR%%", tracepoint_args_skel_error)
+        trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_ERROR_ENV%%", tracepoint_args_skel_error_env)
+        return trace_h
+
+    def print_files(self):
+        super().print_files()
+        trace_h = self.fill_trace_h()
+        path = f"{self.name}_trace.h"
+        self._create_file(path, trace_h)
diff --git a/tools/verification/rvgen/rvgen/kunit.py b/tools/verification/rvgen/rvgen/kunit.py
new file mode 100644
index 000000000..85973f918
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/kunit.py
@@ -0,0 +1,194 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# Copyright (C) 2026-2029 Red Hat, Inc. Gabriele Monaco <gmonaco@redhat.com>
+#
+# Generator for runtime verification kunit files
+
+import re
+from pathlib import Path
+from . import generator
+
+
+class KUnitError(Exception):
+    """Exception raised for errors in KUnit generation and file handling."""
+
+
+class KUnit(generator.RVGenerator):
+    template_dir = ""
+
+    def __init__(self, extra_params={}):
+        super().__init__(extra_params)
+        self.local = extra_params.get("local", False)
+        self.kunit_c = self._read_template_file("kunit.c")
+        if not self.local:
+            self._fill_rv_kernel_dir()
+        try:
+            self.monitor_path = self.__find_monitor_c_file()
+            with open(self.monitor_path, 'r') as f:
+                self.content = f.read()
+        except OSError as e:
+            raise KUnitError(e) from e
+        self.monitor_class = self.__detect_monitor_class()
+
+    def _read_template_file(self, file):
+        if file in ("main.c", "Kconfig"):
+            return ""
+        return super()._read_template_file(file)
+
+    def __find_monitor_c_file(self) -> str:
+        """Look for the monitor file in the kernel tree or in the current folder."""
+        if not self.local:
+            path = Path(self.rv_dir) / "monitors" / self.name / f"{self.name}.c"
+            if path.exists():
+                return str(path)
+
+        path = Path(self.name) / f"{self.name}.c"
+        if path.exists():
+            return str(path)
+
+        raise FileNotFoundError(f"Could not find monitor C file for '{self.name}'")
+
+    def __extract_function_args(self, handler_name: str) -> str:
+        pattern = re.compile(
+            r'^\s*(.*?)\b' + re.escape(handler_name) + r'\(([^)]*)\)',
+            re.MULTILINE | re.DOTALL
+        )
+        match = pattern.search(self.content)
+        if not match:
+            return "/* XXX: fill handlers argument. */"
+
+        return match.group(2).strip()
+
+    def __parse_attach_handlers(self) -> list[str]:
+        """Find handlers by parsing when they are attached to tracepoints."""
+        probe_pattern = re.compile(
+            r'rv_attach_trace_probe\(.*, ([a-zA-Z0-9_]+)\)'
+        )
+        handlers = []
+        for match in probe_pattern.finditer(self.content):
+            handler = match.group(1)
+            if handler not in handlers:
+                handlers.append(handler)
+        return handlers
+
+    def __detect_monitor_class(self) -> str:
+        for c in ("da", "ha", "ltl"):
+            if f"{c}_monitor.h" in self.content:
+                return c
+        return "da"
+
+    def __fill_kunit_c(self, struct_name: str) -> str:
+        kunit_c = self.kunit_c
+        kunit_c = kunit_c.replace("%%MODEL_NAME%%", self.name)
+        kunit_c = kunit_c.replace("%%MODEL_NAME_UP%%", self.name.upper())
+        kunit_c = kunit_c.replace("%%MONITOR_CLASS%%", self.monitor_class)
+        kunit_c = kunit_c.replace("%%STRUCT_NAME%%", struct_name)
+        return kunit_c
+
+    def __fill_kunit_h(self, struct_name, prototypes) -> str:
+        return f"""/* SPDX-License-Identifier: GPL-2.0-only */
+/*
+ * Automatically generated by rvgen kunit.
+ * May need manual intervention for function prototypes that couldn't be
+ * found (e.g. are in another file) or variables to be exported.
+ */
+
+#ifndef __{self.name.upper()}_KUNIT_H
+#define __{self.name.upper()}_KUNIT_H
+
+#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
+
+#include <linux/rv.h>
+#include <rv/kunit.h>
+
+extern const struct {struct_name} {{
+\tstruct rv_kunit_mon mon;
+\t{"\n\t".join(prototypes)}
+}} {struct_name};
+#endif
+
+#endif /* __{self.name.upper()}_KUNIT_H */
+"""
+
+    def __fill_monitor_handlers(self, struct_name, assignments):
+        struct_definition = f"""#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
+#include <kunit/visibility.h>
+#include "{self.name}_kunit.h"
+
+const struct {struct_name} {struct_name} = {{
+\t.mon = RV_MON_OPS_INIT(),
+\t{"\n\t".join(assignments)}
+}};
+EXPORT_SYMBOL_IF_KUNIT({struct_name});
+#endif"""
+
+        if self.auto_patch:
+            try:
+                with open(self.monitor_path, 'w') as f:
+                    f.write(f"{self.content}\n{struct_definition}\n")
+            except OSError as e:
+                raise KUnitError(f"Error patching monitor file {self.monitor_path}: {e}") from e
+        else:
+            print(f"Append the following to {self.name}.c:\n")
+            print(struct_definition)
+        print("Now complete the test and add it to rv_monitors_test.c")
+
+    def print_files(self):
+
+        handlers = self.__parse_attach_handlers()
+
+        if not handlers:
+            raise KUnitError(f"No handlers found in {self.monitor_path}")
+
+        prototypes = []
+        assignments = []
+        for handler in handlers:
+            arguments = self.__extract_function_args(handler)
+
+            prototypes.append(f"void (*{handler})({arguments});")
+            assignments.append(f".{handler} = {handler},")
+
+        struct_name = f"rv_{self.name}_ops"
+
+        self.__fill_monitor_handlers(struct_name, assignments)
+
+        dir_path = Path(self.monitor_path).parent
+
+        header_file_path = dir_path / f"{self.name}_kunit.h"
+        kunit_c_file_path = dir_path / f"{self.name}_kunit.c"
+
+        use_backup = True
+        if header_file_path.exists() or kunit_c_file_path.exists():
+            try:
+                response = input("KUnit file(s) already exist. Backup? [Y/n] ")
+                if response.strip().lower() in ("n", "no"):
+                    use_backup = False
+            except EOFError:
+                print("Non-interactive session detected, backing up existing files.")
+        else:
+            use_backup = False
+
+        if use_backup:
+            for path in (header_file_path, kunit_c_file_path):
+                if path.exists():
+                    try:
+                        path.rename(path.with_suffix(path.suffix + ".old"))
+                    except OSError as e:
+                        raise KUnitError(f"Error backing up file {path}: {e}") from e
+
+        header_content = self.__fill_kunit_h(struct_name, prototypes)
+        try:
+            with open(header_file_path, 'w') as f:
+                f.write(header_content)
+            print(f"Successfully created KUnit header file: {header_file_path}")
+        except OSError as e:
+            raise KUnitError(f"Error writing to file {header_file_path}: {e}") from e
+
+        kunit_c_content = self.__fill_kunit_c(struct_name)
+        try:
+            with open(kunit_c_file_path, 'w') as f:
+                f.write(kunit_c_content)
+            print(f"Successfully created KUnit C file: {kunit_c_file_path}")
+        except OSError as e:
+            raise KUnitError(f"Error writing to file {kunit_c_file_path}: {e}") from e
diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py
new file mode 100644
index 000000000..7cebda61b
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/ltl2ba.py
@@ -0,0 +1,524 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# Implementation based on
+# Gerth, R., Peled, D., Vardi, M.Y., Wolper, P. (1996).
+# Simple On-the-fly Automatic Verification of Linear Temporal Logic.
+# https://doi.org/10.1007/978-0-387-34892-6_1
+# With extra optimizations
+
+import lark
+
+# Grammar:
+# 	ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
+#
+# Operands (opd):
+# 	true, false, user-defined names
+#
+# Unary Operators (unop):
+#       always
+#       eventually
+#       next
+#       not
+#
+# Binary Operators (binop):
+#       until
+#       and
+#       or
+#       imply
+#       equivalent
+
+GRAMMAR = r'''
+start: assign+
+
+assign: VARIABLE "=" _ltl
+
+_ltl: _opd | binop | unop
+
+_opd : VARIABLE
+     | LITERAL
+     | "(" _ltl ")"
+
+unop: UNOP _ltl
+UNOP: "always"
+     | "eventually"
+     | "next"
+     | "not"
+
+binop: _opd BINOP _ltl
+BINOP: "until"
+      | "and"
+      | "or"
+      | "imply"
+
+VARIABLE: /[A-Z_][A-Z0-9_]*/
+LITERAL: "true" | "false"
+
+COMMENT: "#" /.*/ "\n"
+%ignore COMMENT
+
+%import common.WS
+%ignore WS
+'''
+
+class LTLError(Exception):
+    "Exception raised for malformed linear temporal logic"
+
+class GraphNode:
+    uid = 0
+
+    def __init__(self, incoming: set['GraphNode'], new, old, _next):
+        self.init = False
+        self.outgoing = set()
+        self.labels = set()
+        self.incoming = incoming.copy()
+        self.new = new.copy()
+        self.old = old.copy()
+        self.next = _next.copy()
+        self.id = GraphNode.uid
+        GraphNode.uid += 1
+
+    def expand(self, node_set):
+        if not self.new:
+            for nd in node_set:
+                if nd.old == self.old and nd.next == self.next:
+                    nd.incoming |= self.incoming
+                    return node_set
+
+            new_current_node = GraphNode({self}, self.next, set(), set())
+            return new_current_node.expand({self} | node_set)
+        n = self.new.pop()
+        return n.expand(self, node_set)
+
+    def __lt__(self, other):
+        return self.id < other.id
+
+class ASTNode:
+    uid = 0
+
+    def __init__(self, op):
+        self.op = op
+        self.id = ASTNode.uid
+        ASTNode.uid += 1
+
+    def __hash__(self):
+        return hash(self.op)
+
+    def __eq__(self, other):
+        return self is other
+
+    def __iter__(self):
+        yield self
+        yield from self.op
+
+    def negate(self):
+        self.op = self.op.negate()
+        return self
+
+    def expand(self, node, node_set):
+        return self.op.expand(self, node, node_set)
+
+    def __str__(self):
+        if isinstance(self.op, (Literal, Variable)):
+            return str(self.op)
+        return "val" + str(self.id)
+
+    def normalize(self):
+        # Get rid of:
+        #   - ALWAYS
+        #   - EVENTUALLY
+        #   - IMPLY
+        # And move all the NOT to be inside
+        self.op = self.op.normalize()
+        return self
+
+class BinaryOp:
+    op_str = "not_supported"
+
+    def __init__(self, left: ASTNode, right: ASTNode):
+        self.left = left
+        self.right = right
+
+    def __hash__(self):
+        return hash((self.left, self.right))
+
+    def __iter__(self):
+        yield from self.left
+        yield from self.right
+
+    def normalize(self):
+        raise NotImplementedError
+
+    def negate(self):
+        raise NotImplementedError
+
+    def _is_temporal(self):
+        raise NotImplementedError
+
+    def is_temporal(self):
+        if self.left.op.is_temporal():
+            return True
+        if self.right.op.is_temporal():
+            return True
+        return self._is_temporal()
+
+    @staticmethod
+    def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+        raise NotImplementedError
+
+class AndOp(BinaryOp):
+    op_str = '&&'
+
+    def normalize(self):
+        return self
+
+    def negate(self):
+        return OrOp(self.left.negate(), self.right.negate())
+
+    def _is_temporal(self):
+        return False
+
+    @staticmethod
+    def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+        if not n.op.is_temporal():
+            node.old.add(n)
+            return node.expand(node_set)
+
+        tmp = GraphNode(node.incoming,
+                        node.new | ({n.op.left, n.op.right} - node.old),
+                        node.old | {n},
+                        node.next)
+        return tmp.expand(node_set)
+
+class OrOp(BinaryOp):
+    op_str = '||'
+
+    def normalize(self):
+        return self
+
+    def negate(self):
+        return AndOp(self.left.negate(), self.right.negate())
+
+    def _is_temporal(self):
+        return False
+
+    @staticmethod
+    def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+        if not n.op.is_temporal():
+            node.old |= {n}
+            return node.expand(node_set)
+
+        node1 = GraphNode(node.incoming,
+                          node.new | ({n.op.left} - node.old),
+                          node.old | {n},
+                          node.next)
+        node2 = GraphNode(node.incoming,
+                          node.new | ({n.op.right} - node.old),
+                          node.old | {n},
+                          node.next)
+        return node2.expand(node1.expand(node_set))
+
+class UntilOp(BinaryOp):
+    def normalize(self):
+        return self
+
+    def negate(self):
+        return VOp(self.left.negate(), self.right.negate())
+
+    def _is_temporal(self):
+        return True
+
+    @staticmethod
+    def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+        node1 = GraphNode(node.incoming,
+                          node.new | ({n.op.left} - node.old),
+                          node.old | {n},
+                          node.next | {n})
+        node2 = GraphNode(node.incoming,
+                          node.new | ({n.op.right} - node.old),
+                          node.old | {n},
+                          node.next)
+        return node2.expand(node1.expand(node_set))
+
+class VOp(BinaryOp):
+    def normalize(self):
+        return self
+
+    def negate(self):
+        return UntilOp(self.left.negate(), self.right.negate())
+
+    def _is_temporal(self):
+        return True
+
+    @staticmethod
+    def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+        node1 = GraphNode(node.incoming,
+                          node.new | ({n.op.right} - node.old),
+                          node.old | {n},
+                          node.next | {n})
+        node2 = GraphNode(node.incoming,
+                          node.new | ({n.op.left, n.op.right} - node.old),
+                          node.old | {n},
+                          node.next)
+        return node2.expand(node1.expand(node_set))
+
+class ImplyOp(BinaryOp):
+    def normalize(self):
+        # P -> Q === !P | Q
+        return OrOp(self.left.negate(), self.right)
+
+    def _is_temporal(self):
+        return False
+
+    def negate(self):
+        # !(P -> Q) === !(!P | Q) === P & !Q
+        return AndOp(self.left, self.right.negate())
+
+class UnaryOp:
+    def __init__(self, child: ASTNode):
+        self.child = child
+
+    def __iter__(self):
+        yield from self.child
+
+    def __hash__(self):
+        return hash(self.child)
+
+    def normalize(self):
+        raise NotImplementedError
+
+    def _is_temporal(self):
+        raise NotImplementedError
+
+    def is_temporal(self):
+        if self.child.op.is_temporal():
+            return True
+        return self._is_temporal()
+
+    def negate(self):
+        raise NotImplementedError
+
+class EventuallyOp(UnaryOp):
+    def __str__(self):
+        return "eventually " + str(self.child)
+
+    def normalize(self):
+        # <>F == true U F
+        return UntilOp(ASTNode(Literal(True)), self.child)
+
+    def _is_temporal(self):
+        return True
+
+    def negate(self):
+        # !<>F == [](!F)
+        return AlwaysOp(self.child.negate()).normalize()
+
+class AlwaysOp(UnaryOp):
+    def normalize(self):
+        # []F === !(true U !F) == false V F
+        new = ASTNode(Literal(False))
+        return VOp(new, self.child)
+
+    def _is_temporal(self):
+        return True
+
+    def negate(self):
+        # ![]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)
+
+    def normalize(self):
+        return self.child.op.negate()
+
+    def negate(self):
+        return self.child.op
+
+    def _is_temporal(self):
+        return False
+
+    @staticmethod
+    def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+        for f in node.old:
+            if n.op.child is f:
+                return node_set
+        node.old |= {n}
+        return node.expand(node_set)
+
+class Variable:
+    def __init__(self, name: str):
+        self.name = name
+
+    def __hash__(self):
+        return hash(self.name)
+
+    def __iter__(self):
+        yield from ()
+
+    def __str__(self):
+        return self.name.lower()
+
+    def negate(self):
+        new = ASTNode(self)
+        return NotOp(new)
+
+    def normalize(self):
+        return self
+
+    def is_temporal(self):
+        return False
+
+    @staticmethod
+    def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+        for f in node.old:
+            if isinstance(f.op, NotOp) and f.op.child is n:
+                return node_set
+        node.old |= {n}
+        return node.expand(node_set)
+
+class Literal:
+    def __init__(self, value: bool):
+        self.value = value
+
+    def __iter__(self):
+        yield from ()
+
+    def __hash__(self):
+        return hash(self.value)
+
+    def __str__(self):
+        if self.value:
+            return "true"
+        return "false"
+
+    def negate(self):
+        self.value = not self.value
+        return self
+
+    def normalize(self):
+        return self
+
+    def is_temporal(self):
+        return False
+
+    @staticmethod
+    def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+        if not n.op.value:
+            return node_set
+        node.old |= {n}
+        return node.expand(node_set)
+
+class Transform(lark.visitors.Transformer):
+    def unop(self, node):
+        if node[0] == "always":
+            return ASTNode(AlwaysOp(node[1]))
+        if node[0] == "eventually":
+            return ASTNode(EventuallyOp(node[1]))
+        if node[0] == "next":
+            return ASTNode(NextOp(node[1]))
+        if node[0] == "not":
+            return ASTNode(NotOp(node[1]))
+        raise ValueError("Unknown operator %s" % node[0])
+
+    def binop(self, node):
+        if node[1] == "until":
+            return ASTNode(UntilOp(node[0], node[2]))
+        if node[1] == "and":
+            return ASTNode(AndOp(node[0], node[2]))
+        if node[1] == "or":
+            return ASTNode(OrOp(node[0], node[2]))
+        if node[1] == "imply":
+            return ASTNode(ImplyOp(node[0], node[2]))
+        raise ValueError("Unknown operator %s" % node[1])
+
+    def VARIABLE(self, args):
+        return ASTNode(Variable(args))
+
+    def LITERAL(self, args):
+        return ASTNode(Literal(args == "true"))
+
+    def start(self, node):
+        return node
+
+    def assign(self, node):
+        return node[0].op.name, node[1]
+
+parser = lark.Lark(GRAMMAR)
+
+def parse_ltl(s: str) -> ASTNode:
+    try:
+        spec = parser.parse(s)
+    except lark.exceptions.UnexpectedInput as e:
+        raise LTLError(str(e))
+    spec = Transform().transform(spec)
+
+    rule = None
+    subexpr = {}
+
+    for assign in spec:
+        if assign[0] == "RULE":
+            rule = assign[1]
+        else:
+            subexpr[assign[0]] = assign[1]
+
+    if rule is None:
+        raise LTLError("Please define your specification in the \"RULE = <LTL spec>\" format")
+
+    for node in rule:
+        if not isinstance(node.op, Variable):
+            continue
+        replace = subexpr.get(node.op.name)
+        if replace is not None:
+            node.op = replace.op
+
+    return rule
+
+def create_graph(s: str):
+    atoms = set()
+
+    ltl = parse_ltl(s)
+    for c in ltl:
+        c.normalize()
+        if isinstance(c.op, Variable):
+            atoms.add(c.op.name)
+
+    init = GraphNode(set(), set(), set(), set())
+    head = GraphNode({init}, {ltl}, set(), set())
+    graph = sorted(head.expand(set()))
+
+    for i, node in enumerate(graph):
+        # The id assignment during graph generation has gaps. Reassign them
+        node.id = i
+
+        for incoming in node.incoming:
+            if incoming is init:
+                node.init = True
+            else:
+                incoming.outgoing.add(node)
+        for o in node.old:
+            if not o.op.is_temporal():
+                node.labels.add(str(o))
+
+    return sorted(atoms), graph, ltl
diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/rvgen/rvgen/ltl2k.py
new file mode 100644
index 000000000..f3781a3e0
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/ltl2k.py
@@ -0,0 +1,277 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+
+from pathlib import Path
+from . import generator
+from . import ltl2ba
+from .automata import AutomataError
+
+COLUMN_LIMIT = 100
+
+def line_len(line: str) -> int:
+    tabs = line.count('\t')
+    return tabs * 7 + len(line)
+
+def break_long_line(line: str, indent='') -> list[str]:
+    result = []
+    while line_len(line) > COLUMN_LIMIT:
+        i = line[:COLUMN_LIMIT - line_len(line)].rfind(' ')
+        result.append(line[:i])
+        line = indent + line[i + 1:]
+    if line:
+        result.append(line)
+    return result
+
+def build_condition_string(node: ltl2ba.GraphNode):
+    if not node.labels:
+        return "(true)"
+
+    result = "("
+
+    first = True
+    for label in sorted(node.labels):
+        if not first:
+            result += " && "
+        result += label
+        first = False
+
+    result += ")"
+
+    return result
+
+def abbreviate_atoms(atoms: list[str]) -> list[str]:
+    def shorten(s: str) -> str:
+        skip = ["is", "by", "or", "and"]
+        return '_'.join([x[:2] for x in s.lower().split('_') if x not in skip])
+
+    def find_share_length(atom: str) -> int:
+        for i in range(len(atom), -1, -1):
+            if sum(a.startswith(atom[:i]) for a in atoms) > 1:
+                return i
+        return 0
+
+    abbrs = []
+    for atom in atoms:
+        share_len = find_share_length(atom)
+        share = atom[:share_len]
+        unique = atom[share_len:]
+        abbrs.append((shorten(share) + shorten(unique)))
+    return abbrs
+
+class ltl2k(generator.Monitor):
+    template_dir = "ltl2k"
+
+    def __init__(self, file_path, MonitorType, extra_params={}):
+        if MonitorType != "per_task":
+            raise NotImplementedError("Only per_task monitor is supported for LTL")
+        super().__init__(extra_params)
+        try:
+            with open(file_path) as f:
+                self.atoms, self.ba, self.ltl = ltl2ba.create_graph(f.read())
+        except OSError as exc:
+            raise AutomataError(exc.strerror) from exc
+        self.atoms_abbr = abbreviate_atoms(self.atoms)
+        self.name = extra_params.get("model_name")
+        if not self.name:
+            self.name = Path(file_path).stem
+
+    def _fill_states(self) -> list[str]:
+        buf = [
+            "enum ltl_buchi_state {",
+        ]
+
+        for node in self.ba:
+            buf.append(f"\tS{node.id},")
+        buf.append("\tRV_NUM_BA_STATES")
+        buf.append("};")
+        buf.append("static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);")
+        return buf
+
+    def _fill_atoms(self):
+        buf = ["enum ltl_atom {"]
+        for a in sorted(self.atoms):
+            buf.append(f"\tLTL_{a},")
+        buf.append("\tLTL_NUM_ATOM")
+        buf.append("};")
+        buf.append("static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM);")
+        return buf
+
+    def _fill_atoms_to_string(self):
+        buf = [
+            "static const char *ltl_atom_str(enum ltl_atom atom)",
+            "{",
+            "\tstatic const char *const names[] = {"
+        ]
+
+        for name in self.atoms_abbr:
+            buf.append(f"\t\t\"{name}\",")
+
+        buf.extend([
+            "\t};",
+            "",
+            "\treturn names[atom];",
+            "}"
+        ])
+        return buf
+
+    def _fill_atom_values(self, required_values):
+        buf = []
+        for node in self.ltl:
+            if str(node) not in required_values:
+                continue
+
+            if isinstance(node.op, ltl2ba.AndOp):
+                buf.append(f"\tbool {node} = {node.op.left} && {node.op.right};")
+                required_values |= {str(node.op.left), str(node.op.right)}
+            elif isinstance(node.op, ltl2ba.OrOp):
+                buf.append(f"\tbool {node} = {node.op.left} || {node.op.right};")
+                required_values |= {str(node.op.left), str(node.op.right)}
+            elif isinstance(node.op, ltl2ba.NotOp):
+                buf.append(f"\tbool {node} = !{node.op.child};")
+                required_values.add(str(node.op.child))
+
+        for atom in self.atoms:
+            if atom.lower() not in required_values:
+                continue
+            buf.append(f"\tbool {atom.lower()} = test_bit(LTL_{atom}, mon->atoms);")
+
+        buf.reverse()
+
+        buf2 = []
+        for line in buf:
+            buf2.extend(break_long_line(line, "\t     "))
+        return buf2
+
+    def _fill_transitions(self):
+        buf = [
+            "static void",
+            "ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)",
+            "{"
+        ]
+
+        required_values = set()
+        for node in self.ba:
+            for o in sorted(node.outgoing):
+                required_values |= o.labels
+
+        buf.extend(self._fill_atom_values(required_values))
+        buf.extend([
+            "",
+            "\tswitch (state) {"
+        ])
+
+        for node in self.ba:
+            buf.append(f"\tcase S{node.id}:")
+
+            for o in sorted(node.outgoing):
+                line   = "\t\tif "
+                indent = "\t\t   "
+
+                line += build_condition_string(o)
+                lines = break_long_line(line, indent)
+                buf.extend(lines)
+
+                buf.append(f"\t\t\t__set_bit(S{o.id}, next);")
+            buf.append("\t\tbreak;")
+        buf.extend([
+            "\t}",
+            "}"
+        ])
+
+        return buf
+
+    def _fill_start(self):
+        buf = [
+            "static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)",
+            "{"
+        ]
+
+        required_values = set()
+        for node in self.ba:
+            if node.init:
+                required_values |= node.labels
+
+        buf.extend(self._fill_atom_values(required_values))
+        buf.append("")
+
+        for node in self.ba:
+            if not node.init:
+                continue
+
+            line   = "\tif "
+            indent = "\t   "
+
+            line += build_condition_string(node)
+            lines = break_long_line(line, indent)
+            buf.extend(lines)
+
+            buf.append(f"\t\t__set_bit(S{node.id}, mon->states);")
+        buf.append("}")
+        return buf
+
+    def fill_tracepoint_handlers_skel(self):
+        buff = []
+        buff.append("static void handle_example_event(void *data, /* XXX: fill header */)")
+        buff.append("{")
+        buff.append(f"\tltl_atom_update(task, LTL_{self.atoms[0]}, true/false);")
+        buff.append("}")
+        buff.append("")
+        return '\n'.join(buff)
+
+    def fill_tracepoint_attach_probe(self):
+        return f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_example_event);"
+
+    def fill_tracepoint_detach_helper(self):
+        return f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_example_event);"
+
+    def fill_atoms_init(self):
+        buff = []
+        for a in self.atoms:
+            buff.append(f"\tltl_atom_set(mon, LTL_{a}, true/false);")
+        return '\n'.join(buff)
+
+    def fill_model_h(self):
+        buf = [
+            "/* SPDX-License-Identifier: GPL-2.0 */",
+            "",
+            "/*",
+            " * C implementation of Buchi automaton, automatically generated by",
+            " * tools/verification/rvgen from the linear temporal logic specification.",
+            " * For further information, see kernel documentation:",
+            " *   Documentation/trace/rv/linear_temporal_logic.rst",
+            " */",
+            "",
+            "#include <linux/rv.h>",
+            "",
+            "#define MONITOR_NAME " + self.name,
+            ""
+        ]
+
+        buf.extend(self._fill_atoms())
+        buf.append('')
+
+        buf.extend(self._fill_atoms_to_string())
+        buf.append('')
+
+        buf.extend(self._fill_states())
+        buf.append('')
+
+        buf.extend(self._fill_start())
+        buf.append('')
+
+        buf.extend(self._fill_transitions())
+        buf.append('')
+
+        return '\n'.join(buf)
+
+    def fill_monitor_class_type(self):
+        return "LTL_MON_EVENTS_ID"
+
+    def fill_monitor_class(self):
+        return "ltl_monitor_id"
+
+    def fill_main_c(self):
+        main_c = super().fill_main_c()
+        main_c = main_c.replace("%%ATOMS_INIT%%", self.fill_atoms_init())
+
+        return main_c
diff --git a/tools/verification/rvgen/rvgen/templates/Kconfig b/tools/verification/rvgen/rvgen/templates/Kconfig
new file mode 100644
index 000000000..291b29ea2
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/templates/Kconfig
@@ -0,0 +1,9 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_%%MODEL_NAME_UP%%
+	depends on RV
+%%MONITOR_DEPS%%
+	select %%MONITOR_CLASS_TYPE%%
+	bool "%%MODEL_NAME%% monitor"
+	help
+	  %%DESCRIPTION%%
diff --git a/tools/verification/rvgen/rvgen/templates/container/Kconfig b/tools/verification/rvgen/rvgen/templates/container/Kconfig
new file mode 100644
index 000000000..a60611194
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/templates/container/Kconfig
@@ -0,0 +1,5 @@
+config RV_MON_%%MODEL_NAME_UP%%
+	depends on RV
+	bool "%%MODEL_NAME%% monitor"
+	help
+	  %%DESCRIPTION%%
diff --git a/tools/verification/rvgen/rvgen/templates/container/main.c b/tools/verification/rvgen/rvgen/templates/container/main.c
new file mode 100644
index 000000000..e6a20d748
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/templates/container/main.c
@@ -0,0 +1,35 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+
+#define MODULE_NAME "%%MODEL_NAME%%"
+
+#include "%%MODEL_NAME%%.h"
+
+struct rv_monitor rv_%%MODEL_NAME%% = {
+	.name = "%%MODEL_NAME%%",
+	.description = "%%DESCRIPTION%%",
+	.enable = NULL,
+	.disable = NULL,
+	.reset = NULL,
+	.enabled = 0,
+};
+
+static int __init register_%%MODEL_NAME%%(void)
+{
+	return rv_register_monitor(&rv_%%MODEL_NAME%%, NULL);
+}
+
+static void __exit unregister_%%MODEL_NAME%%(void)
+{
+	rv_unregister_monitor(&rv_%%MODEL_NAME%%);
+}
+
+module_init(register_%%MODEL_NAME%%);
+module_exit(unregister_%%MODEL_NAME%%);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("rvgen: auto-generated");
+MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%");
diff --git a/tools/verification/rvgen/rvgen/templates/container/main.h b/tools/verification/rvgen/rvgen/templates/container/main.h
new file mode 100644
index 000000000..0f6883ab4
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/templates/container/main.h
@@ -0,0 +1,3 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+extern struct rv_monitor rv_%%MODEL_NAME%%;
diff --git a/tools/verification/rvgen/rvgen/templates/dot2k/main.c b/tools/verification/rvgen/rvgen/templates/dot2k/main.c
new file mode 100644
index 000000000..bd3e0aab9
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/templates/dot2k/main.c
@@ -0,0 +1,83 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "%%MODEL_NAME%%"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <trace/events/sched.h>
+ */
+#include <rv_trace.h>
+%%INCLUDE_PARENT%%
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#define RV_MON_TYPE RV_MON_%%MONITOR_TYPE%%
+#include "%%MODEL_NAME%%.h"
+#include <rv/%%MONITOR_CLASS%%_monitor.h>
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ *
+ */
+%%TRACEPOINT_HANDLERS_SKEL%%
+static int enable_%%MODEL_NAME%%(void)
+{
+	int retval;
+
+	retval = %%MONITOR_CLASS%%_monitor_init();
+	if (retval)
+		return retval;
+
+%%TRACEPOINT_ATTACH%%
+
+	return 0;
+}
+
+static void disable_%%MODEL_NAME%%(void)
+{
+	rv_this.enabled = 0;
+
+%%TRACEPOINT_DETACH%%
+
+	%%MONITOR_CLASS%%_monitor_destroy();
+}
+
+/*
+ * This is the monitor register section.
+ */
+static struct rv_monitor rv_this = {
+	.name = "%%MODEL_NAME%%",
+	.description = "%%DESCRIPTION%%",
+	.enable = enable_%%MODEL_NAME%%,
+	.disable = disable_%%MODEL_NAME%%,
+	.reset = da_monitor_reset_all,
+	.enabled = 0,
+};
+
+static int __init register_%%MODEL_NAME%%(void)
+{
+	return rv_register_monitor(&rv_this, %%PARENT%%);
+}
+
+static void __exit unregister_%%MODEL_NAME%%(void)
+{
+	rv_unregister_monitor(&rv_this);
+}
+
+module_init(register_%%MODEL_NAME%%);
+module_exit(unregister_%%MODEL_NAME%%);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("rvgen: auto-generated");
+MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%");
diff --git a/tools/verification/rvgen/rvgen/templates/dot2k/trace.h b/tools/verification/rvgen/rvgen/templates/dot2k/trace.h
new file mode 100644
index 000000000..87d3a1308
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/templates/dot2k/trace.h
@@ -0,0 +1,13 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_%%MODEL_NAME_UP%%
+DEFINE_EVENT(event_%%MONITOR_CLASS%%, event_%%MODEL_NAME%%,
+%%TRACEPOINT_ARGS_SKEL_EVENT%%);
+
+DEFINE_EVENT(error_%%MONITOR_CLASS%%, error_%%MODEL_NAME%%,
+%%TRACEPOINT_ARGS_SKEL_ERROR%%);
+#endif /* CONFIG_RV_MON_%%MODEL_NAME_UP%% */
diff --git a/tools/verification/rvgen/rvgen/templates/dot2k/trace_hybrid.h b/tools/verification/rvgen/rvgen/templates/dot2k/trace_hybrid.h
new file mode 100644
index 000000000..c8290e9ba
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/templates/dot2k/trace_hybrid.h
@@ -0,0 +1,16 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_%%MODEL_NAME_UP%%
+DEFINE_EVENT(event_%%MONITOR_CLASS%%, event_%%MODEL_NAME%%,
+%%TRACEPOINT_ARGS_SKEL_EVENT%%);
+
+DEFINE_EVENT(error_%%MONITOR_CLASS%%, error_%%MODEL_NAME%%,
+%%TRACEPOINT_ARGS_SKEL_ERROR%%);
+
+DEFINE_EVENT(error_env_%%MONITOR_CLASS%%, error_env_%%MODEL_NAME%%,
+%%TRACEPOINT_ARGS_SKEL_ERROR_ENV%%);
+#endif /* CONFIG_RV_MON_%%MODEL_NAME_UP%% */
diff --git a/tools/verification/rvgen/rvgen/templates/kunit.c b/tools/verification/rvgen/rvgen/templates/kunit.c
new file mode 100644
index 000000000..62092b5cc
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/templates/kunit.c
@@ -0,0 +1,33 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/kernel.h>
+#include <linux/rv.h>
+#include <rv/kunit.h>
+/*
+ * XXX: include required headers, e.g.,
+ * #include <linux/sched.h>
+ */
+#include "%%MODEL_NAME%%_kunit.h"
+
+#if IS_REACHABLE(CONFIG_RV_MON_%%MODEL_NAME_UP%%)
+
+static void rv_test_%%MODEL_NAME%%(struct kunit *test)
+{
+	struct rv_kunit_ctx *ctx = test->priv;
+	/*
+	 * If you need to create task_structs with rv_kunit_alloc_mock_task()
+	 * do it BEFORE preparing the test.
+	 */
+
+	prepare_test(test, &%%STRUCT_NAME%%.mon);
+
+	/*
+	 * XXX: write the test here
+	 * e.g.
+	 * RV_KUNIT_EXPECT_REACTION_HERE(test, ctx)
+	 *	%%STRUCT_NAME%%.handle_event(args);
+	 */
+}
+
+#else
+#define rv_test_%%MODEL_NAME%% rv_test_stub
+#endif
diff --git a/tools/verification/rvgen/rvgen/templates/ltl2k/main.c b/tools/verification/rvgen/rvgen/templates/ltl2k/main.c
new file mode 100644
index 000000000..c33f21535
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/templates/ltl2k/main.c
@@ -0,0 +1,102 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "%%MODEL_NAME%%"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <trace/events/sched.h>
+ */
+#include <rv_trace.h>
+%%INCLUDE_PARENT%%
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#include "%%MODEL_NAME%%.h"
+#include <rv/ltl_monitor.h>
+
+static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon)
+{
+	/*
+	 * This is called everytime the Buchi automaton is triggered.
+	 *
+	 * This function could be used to fetch the atomic propositions which
+	 * are expensive to trace. It is possible only if the atomic proposition
+	 * does not need to be updated at precise time.
+	 *
+	 * It is recommended to use tracepoints and ltl_atom_update() instead.
+	 */
+}
+
+static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)
+{
+	/*
+	 * This should initialize as many atomic propositions as possible.
+	 *
+	 * @task_creation indicates whether the task is being created. This is
+	 * false if the task is already running before the monitor is enabled.
+	 */
+%%ATOMS_INIT%%
+}
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ */
+%%TRACEPOINT_HANDLERS_SKEL%%
+static int enable_%%MODEL_NAME%%(void)
+{
+	int retval;
+
+	retval = ltl_monitor_init();
+	if (retval)
+		return retval;
+
+%%TRACEPOINT_ATTACH%%
+
+	return 0;
+}
+
+static void disable_%%MODEL_NAME%%(void)
+{
+%%TRACEPOINT_DETACH%%
+
+	ltl_monitor_destroy();
+}
+
+/*
+ * This is the monitor register section.
+ */
+static struct rv_monitor rv_this = {
+	.name = "%%MODEL_NAME%%",
+	.description = "%%DESCRIPTION%%",
+	.enable = enable_%%MODEL_NAME%%,
+	.disable = disable_%%MODEL_NAME%%,
+};
+
+static int __init register_%%MODEL_NAME%%(void)
+{
+	return rv_register_monitor(&rv_this, %%PARENT%%);
+}
+
+static void __exit unregister_%%MODEL_NAME%%(void)
+{
+	rv_unregister_monitor(&rv_this);
+}
+
+module_init(register_%%MODEL_NAME%%);
+module_exit(unregister_%%MODEL_NAME%%);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("rvgen: auto-generated");
+MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%");
diff --git a/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h b/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h
new file mode 100644
index 000000000..49394c4b0
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h
@@ -0,0 +1,14 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_%%MODEL_NAME_UP%%
+DEFINE_EVENT(event_%%MONITOR_CLASS%%, event_%%MODEL_NAME%%,
+	     TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next),
+	     TP_ARGS(task, states, atoms, next));
+DEFINE_EVENT(error_%%MONITOR_CLASS%%, error_%%MODEL_NAME%%,
+	     TP_PROTO(struct task_struct *task),
+	     TP_ARGS(task));
+#endif /* CONFIG_RV_MON_%%MODEL_NAME_UP%% */
diff --git a/tools/verification/rvgen/tests/golden/da_global/Kconfig b/tools/verification/rvgen/tests/golden/da_global/Kconfig
new file mode 100644
index 000000000..799fbf11c
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/da_global/Kconfig
@@ -0,0 +1,9 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_DA_GLOBAL
+	depends on RV
+	# XXX: add dependencies if there
+	select DA_MON_EVENTS_IMPLICIT
+	bool "da_global monitor"
+	help
+	  auto-generated
diff --git a/tools/verification/rvgen/tests/golden/da_global/da_global.c b/tools/verification/rvgen/tests/golden/da_global/da_global.c
new file mode 100644
index 000000000..71b26ae2d
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/da_global/da_global.c
@@ -0,0 +1,95 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "da_global"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <trace/events/sched.h>
+ */
+#include <rv_trace.h>
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#define RV_MON_TYPE RV_MON_GLOBAL
+#include "da_global.h"
+#include <rv/da_monitor.h>
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ *
+ */
+static void handle_event_1(void *data, /* XXX: fill header */)
+{
+	da_handle_event(event_1_da_global);
+}
+
+static void handle_event_2(void *data, /* XXX: fill header */)
+{
+	/* XXX: validate that this event always leads to the initial state */
+	da_handle_start_event(event_2_da_global);
+}
+
+static int enable_da_global(void)
+{
+	int retval;
+
+	retval = da_monitor_init();
+	if (retval)
+		return retval;
+
+	rv_attach_trace_probe("da_global", /* XXX: tracepoint */, handle_event_1);
+	rv_attach_trace_probe("da_global", /* XXX: tracepoint */, handle_event_2);
+
+	return 0;
+}
+
+static void disable_da_global(void)
+{
+	rv_this.enabled = 0;
+
+	rv_detach_trace_probe("da_global", /* XXX: tracepoint */, handle_event_1);
+	rv_detach_trace_probe("da_global", /* XXX: tracepoint */, handle_event_2);
+
+	da_monitor_destroy();
+}
+
+/*
+ * This is the monitor register section.
+ */
+static struct rv_monitor rv_this = {
+	.name = "da_global",
+	.description = "auto-generated",
+	.enable = enable_da_global,
+	.disable = disable_da_global,
+	.reset = da_monitor_reset_all,
+	.enabled = 0,
+};
+
+static int __init register_da_global(void)
+{
+	return rv_register_monitor(&rv_this, NULL);
+}
+
+static void __exit unregister_da_global(void)
+{
+	rv_unregister_monitor(&rv_this);
+}
+
+module_init(register_da_global);
+module_exit(unregister_da_global);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("rvgen: auto-generated");
+MODULE_DESCRIPTION("da_global: auto-generated");
diff --git a/tools/verification/rvgen/tests/golden/da_global/da_global.h b/tools/verification/rvgen/tests/golden/da_global/da_global.h
new file mode 100644
index 000000000..40b1f1c0c
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/da_global/da_global.h
@@ -0,0 +1,47 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Automatically generated C representation of da_global automaton
+ * For further information about this format, see kernel documentation:
+ *   Documentation/trace/rv/deterministic_automata.rst
+ */
+
+#define MONITOR_NAME da_global
+
+enum states_da_global {
+	state_a_da_global,
+	state_b_da_global,
+	state_max_da_global,
+};
+
+#define INVALID_STATE state_max_da_global
+
+enum events_da_global {
+	event_1_da_global,
+	event_2_da_global,
+	event_max_da_global,
+};
+
+struct automaton_da_global {
+	char *state_names[state_max_da_global];
+	char *event_names[event_max_da_global];
+	unsigned char function[state_max_da_global][event_max_da_global];
+	unsigned char initial_state;
+	bool final_states[state_max_da_global];
+};
+
+static const struct automaton_da_global automaton_da_global = {
+	.state_names = {
+		"state_a",
+		"state_b",
+	},
+	.event_names = {
+		"event_1",
+		"event_2",
+	},
+	.function = {
+		{       state_b_da_global,       state_a_da_global },
+		{           INVALID_STATE,       state_a_da_global },
+	},
+	.initial_state = state_a_da_global,
+	.final_states = { 1, 0 },
+};
diff --git a/tools/verification/rvgen/tests/golden/da_global/da_global_trace.h b/tools/verification/rvgen/tests/golden/da_global/da_global_trace.h
new file mode 100644
index 000000000..4d2730b71
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/da_global/da_global_trace.h
@@ -0,0 +1,15 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_DA_GLOBAL
+DEFINE_EVENT(event_da_monitor, event_da_global,
+	     TP_PROTO(char *state, char *event, char *next_state, bool final_state),
+	     TP_ARGS(state, event, next_state, final_state));
+
+DEFINE_EVENT(error_da_monitor, error_da_global,
+	     TP_PROTO(char *state, char *event),
+	     TP_ARGS(state, event));
+#endif /* CONFIG_RV_MON_DA_GLOBAL */
diff --git a/tools/verification/rvgen/tests/golden/da_perobj_parent/Kconfig b/tools/verification/rvgen/tests/golden/da_perobj_parent/Kconfig
new file mode 100644
index 000000000..249ba3aee
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/da_perobj_parent/Kconfig
@@ -0,0 +1,11 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_DA_PEROBJ_PARENT
+	depends on RV
+	# XXX: add dependencies if there
+	depends on RV_MON_PARENT_MON
+	default y
+	select DA_MON_EVENTS_ID
+	bool "da_perobj_parent monitor"
+	help
+	  auto-generated
diff --git a/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent.c b/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent.c
new file mode 100644
index 000000000..5c5d300b4
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent.c
@@ -0,0 +1,119 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "da_perobj_parent"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <trace/events/sched.h>
+ */
+#include <rv_trace.h>
+#include <monitors/parent_mon/parent_mon.h>
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#define RV_MON_TYPE RV_MON_PER_OBJ
+typedef /* XXX: define the target type */ *monitor_target;
+#include "da_perobj_parent.h"
+#include <rv/da_monitor.h>
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ *
+ */
+static void handle_event_1(void *data, /* XXX: fill header */)
+{
+	/* XXX: validate that this event is only valid in the initial state */
+	int id = /* XXX: how do I get the id? */;
+	monitor_target t = /* XXX: how do I get t? */;
+	da_handle_start_run_event(id, t, event_1_da_perobj_parent);
+}
+
+static void handle_event_2(void *data, /* XXX: fill header */)
+{
+	int id = /* XXX: how do I get the id? */;
+	monitor_target t = /* XXX: how do I get t? */;
+	da_handle_event(id, t, event_2_da_perobj_parent);
+}
+
+static void handle_event_3(void *data, /* XXX: fill header */)
+{
+	int id = /* XXX: how do I get the id? */;
+	monitor_target t = /* XXX: how do I get t? */;
+	da_handle_event(id, t, event_3_da_perobj_parent);
+}
+
+/* XXX: obj is being destroyed, remove if not required (e.g. obj is static) */
+static void handle_obj_cleanup(void *data, /* XXX: fill header */)
+{
+	int id = /* XXX: how do I get the id? */;
+	da_destroy_storage(id);
+}
+
+static int enable_da_perobj_parent(void)
+{
+	int retval;
+
+	retval = da_monitor_init();
+	if (retval)
+		return retval;
+
+	rv_attach_trace_probe("da_perobj_parent", /* XXX: tracepoint */, handle_event_1);
+	rv_attach_trace_probe("da_perobj_parent", /* XXX: tracepoint */, handle_event_2);
+	rv_attach_trace_probe("da_perobj_parent", /* XXX: tracepoint */, handle_event_3);
+	rv_attach_trace_probe("da_perobj_parent", /* XXX: cleanup tracepoint */, handle_obj_cleanup);
+
+	return 0;
+}
+
+static void disable_da_perobj_parent(void)
+{
+	rv_this.enabled = 0;
+
+	rv_detach_trace_probe("da_perobj_parent", /* XXX: tracepoint */, handle_event_1);
+	rv_detach_trace_probe("da_perobj_parent", /* XXX: tracepoint */, handle_event_2);
+	rv_detach_trace_probe("da_perobj_parent", /* XXX: tracepoint */, handle_event_3);
+	rv_detach_trace_probe("da_perobj_parent", /* XXX: cleanup tracepoint */, handle_obj_cleanup);
+
+	da_monitor_destroy();
+}
+
+/*
+ * This is the monitor register section.
+ */
+static struct rv_monitor rv_this = {
+	.name = "da_perobj_parent",
+	.description = "auto-generated",
+	.enable = enable_da_perobj_parent,
+	.disable = disable_da_perobj_parent,
+	.reset = da_monitor_reset_all,
+	.enabled = 0,
+};
+
+static int __init register_da_perobj_parent(void)
+{
+	return rv_register_monitor(&rv_this, &rv_parent_mon);
+}
+
+static void __exit unregister_da_perobj_parent(void)
+{
+	rv_unregister_monitor(&rv_this);
+}
+
+module_init(register_da_perobj_parent);
+module_exit(unregister_da_perobj_parent);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("rvgen: auto-generated");
+MODULE_DESCRIPTION("da_perobj_parent: auto-generated");
diff --git a/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent.h b/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent.h
new file mode 100644
index 000000000..3c8dc3b22
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent.h
@@ -0,0 +1,64 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Automatically generated C representation of da_perobj_parent automaton
+ * For further information about this format, see kernel documentation:
+ *   Documentation/trace/rv/deterministic_automata.rst
+ */
+
+#define MONITOR_NAME da_perobj_parent
+
+enum states_da_perobj_parent {
+	state_a_da_perobj_parent,
+	state_b_da_perobj_parent,
+	state_c_da_perobj_parent,
+	state_max_da_perobj_parent,
+};
+
+#define INVALID_STATE state_max_da_perobj_parent
+
+enum events_da_perobj_parent {
+	event_1_da_perobj_parent,
+	event_2_da_perobj_parent,
+	event_3_da_perobj_parent,
+	event_max_da_perobj_parent,
+};
+
+struct automaton_da_perobj_parent {
+	char *state_names[state_max_da_perobj_parent];
+	char *event_names[event_max_da_perobj_parent];
+	unsigned char function[state_max_da_perobj_parent][event_max_da_perobj_parent];
+	unsigned char initial_state;
+	bool final_states[state_max_da_perobj_parent];
+};
+
+static const struct automaton_da_perobj_parent automaton_da_perobj_parent = {
+	.state_names = {
+		"state_a",
+		"state_b",
+		"state_c",
+	},
+	.event_names = {
+		"event_1",
+		"event_2",
+		"event_3",
+	},
+	.function = {
+		{
+			state_b_da_perobj_parent,
+			state_c_da_perobj_parent,
+			INVALID_STATE,
+		},
+		{
+			INVALID_STATE,
+			state_a_da_perobj_parent,
+			state_c_da_perobj_parent,
+		},
+		{
+			INVALID_STATE,
+			INVALID_STATE,
+			INVALID_STATE,
+		},
+	},
+	.initial_state = state_a_da_perobj_parent,
+	.final_states = { 1, 0, 0 },
+};
diff --git a/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent_trace.h b/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent_trace.h
new file mode 100644
index 000000000..59bfca8f7
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent_trace.h
@@ -0,0 +1,15 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_DA_PEROBJ_PARENT
+DEFINE_EVENT(event_da_monitor_id, event_da_perobj_parent,
+	     TP_PROTO(int id, char *state, char *event, char *next_state, bool final_state),
+	     TP_ARGS(id, state, event, next_state, final_state));
+
+DEFINE_EVENT(error_da_monitor_id, error_da_perobj_parent,
+	     TP_PROTO(int id, char *state, char *event),
+	     TP_ARGS(id, state, event));
+#endif /* CONFIG_RV_MON_DA_PEROBJ_PARENT */
diff --git a/tools/verification/rvgen/tests/golden/da_pertask_desc/Kconfig b/tools/verification/rvgen/tests/golden/da_pertask_desc/Kconfig
new file mode 100644
index 000000000..c6f350179
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/da_pertask_desc/Kconfig
@@ -0,0 +1,9 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_DA_PERTASK_DESC
+	depends on RV
+	# XXX: add dependencies if there
+	select DA_MON_EVENTS_ID
+	bool "da_pertask_desc monitor"
+	help
+	  Custom description for testing
diff --git a/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc.c b/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc.c
new file mode 100644
index 000000000..c1ae5078c
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc.c
@@ -0,0 +1,105 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "da_pertask_desc"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <trace/events/sched.h>
+ */
+#include <rv_trace.h>
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#define RV_MON_TYPE RV_MON_PER_TASK
+#include "da_pertask_desc.h"
+#include <rv/da_monitor.h>
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ *
+ */
+static void handle_event_1(void *data, /* XXX: fill header */)
+{
+	/* XXX: validate that this event is only valid in the initial state */
+	struct task_struct *p = /* XXX: how do I get p? */;
+	da_handle_start_run_event(p, event_1_da_pertask_desc);
+}
+
+static void handle_event_2(void *data, /* XXX: fill header */)
+{
+	struct task_struct *p = /* XXX: how do I get p? */;
+	da_handle_event(p, event_2_da_pertask_desc);
+}
+
+static void handle_event_3(void *data, /* XXX: fill header */)
+{
+	struct task_struct *p = /* XXX: how do I get p? */;
+	da_handle_event(p, event_3_da_pertask_desc);
+}
+
+static int enable_da_pertask_desc(void)
+{
+	int retval;
+
+	retval = da_monitor_init();
+	if (retval)
+		return retval;
+
+	rv_attach_trace_probe("da_pertask_desc", /* XXX: tracepoint */, handle_event_1);
+	rv_attach_trace_probe("da_pertask_desc", /* XXX: tracepoint */, handle_event_2);
+	rv_attach_trace_probe("da_pertask_desc", /* XXX: tracepoint */, handle_event_3);
+
+	return 0;
+}
+
+static void disable_da_pertask_desc(void)
+{
+	rv_this.enabled = 0;
+
+	rv_detach_trace_probe("da_pertask_desc", /* XXX: tracepoint */, handle_event_1);
+	rv_detach_trace_probe("da_pertask_desc", /* XXX: tracepoint */, handle_event_2);
+	rv_detach_trace_probe("da_pertask_desc", /* XXX: tracepoint */, handle_event_3);
+
+	da_monitor_destroy();
+}
+
+/*
+ * This is the monitor register section.
+ */
+static struct rv_monitor rv_this = {
+	.name = "da_pertask_desc",
+	.description = "Custom description for testing",
+	.enable = enable_da_pertask_desc,
+	.disable = disable_da_pertask_desc,
+	.reset = da_monitor_reset_all,
+	.enabled = 0,
+};
+
+static int __init register_da_pertask_desc(void)
+{
+	return rv_register_monitor(&rv_this, NULL);
+}
+
+static void __exit unregister_da_pertask_desc(void)
+{
+	rv_unregister_monitor(&rv_this);
+}
+
+module_init(register_da_pertask_desc);
+module_exit(unregister_da_pertask_desc);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("rvgen: auto-generated");
+MODULE_DESCRIPTION("da_pertask_desc: Custom description for testing");
diff --git a/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc.h b/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc.h
new file mode 100644
index 000000000..837b23875
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc.h
@@ -0,0 +1,64 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Automatically generated C representation of da_pertask_desc automaton
+ * For further information about this format, see kernel documentation:
+ *   Documentation/trace/rv/deterministic_automata.rst
+ */
+
+#define MONITOR_NAME da_pertask_desc
+
+enum states_da_pertask_desc {
+	state_a_da_pertask_desc,
+	state_b_da_pertask_desc,
+	state_c_da_pertask_desc,
+	state_max_da_pertask_desc,
+};
+
+#define INVALID_STATE state_max_da_pertask_desc
+
+enum events_da_pertask_desc {
+	event_1_da_pertask_desc,
+	event_2_da_pertask_desc,
+	event_3_da_pertask_desc,
+	event_max_da_pertask_desc,
+};
+
+struct automaton_da_pertask_desc {
+	char *state_names[state_max_da_pertask_desc];
+	char *event_names[event_max_da_pertask_desc];
+	unsigned char function[state_max_da_pertask_desc][event_max_da_pertask_desc];
+	unsigned char initial_state;
+	bool final_states[state_max_da_pertask_desc];
+};
+
+static const struct automaton_da_pertask_desc automaton_da_pertask_desc = {
+	.state_names = {
+		"state_a",
+		"state_b",
+		"state_c",
+	},
+	.event_names = {
+		"event_1",
+		"event_2",
+		"event_3",
+	},
+	.function = {
+		{
+			state_b_da_pertask_desc,
+			state_c_da_pertask_desc,
+			INVALID_STATE,
+		},
+		{
+			INVALID_STATE,
+			state_a_da_pertask_desc,
+			state_c_da_pertask_desc,
+		},
+		{
+			INVALID_STATE,
+			INVALID_STATE,
+			INVALID_STATE,
+		},
+	},
+	.initial_state = state_a_da_pertask_desc,
+	.final_states = { 1, 0, 0 },
+};
diff --git a/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc_trace.h b/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc_trace.h
new file mode 100644
index 000000000..4e6086c4d
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc_trace.h
@@ -0,0 +1,15 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_DA_PERTASK_DESC
+DEFINE_EVENT(event_da_monitor_id, event_da_pertask_desc,
+	     TP_PROTO(int id, char *state, char *event, char *next_state, bool final_state),
+	     TP_ARGS(id, state, event, next_state, final_state));
+
+DEFINE_EVENT(error_da_monitor_id, error_da_pertask_desc,
+	     TP_PROTO(int id, char *state, char *event),
+	     TP_ARGS(id, state, event));
+#endif /* CONFIG_RV_MON_DA_PERTASK_DESC */
diff --git a/tools/verification/rvgen/tests/golden/ha_percpu/Kconfig b/tools/verification/rvgen/tests/golden/ha_percpu/Kconfig
new file mode 100644
index 000000000..0cc185ccf
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/ha_percpu/Kconfig
@@ -0,0 +1,9 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_HA_PERCPU
+	depends on RV
+	# XXX: add dependencies if there
+	select HA_MON_EVENTS_IMPLICIT
+	bool "ha_percpu monitor"
+	help
+	  auto-generated
diff --git a/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu.c b/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu.c
new file mode 100644
index 000000000..3a72e8671
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu.c
@@ -0,0 +1,227 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "ha_percpu"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <trace/events/sched.h>
+ */
+#include <rv_trace.h>
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#define RV_MON_TYPE RV_MON_PER_CPU
+/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */
+#define HA_TIMER_TYPE HA_TIMER_HRTIMER
+#include "ha_percpu.h"
+#include <rv/ha_monitor.h>
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ *
+ */
+#define BAR_NS(ha_mon) /* XXX: what is BAR_NS(ha_mon)? */
+
+#define FOO_NS /* XXX: what is FOO_NS? */
+
+static inline u64 bar_ns(struct ha_monitor *ha_mon)
+{
+	return /* XXX: what is bar_ns(ha_mon)? */;
+}
+
+static u64 foo_ns = /* XXX: default value */;
+module_param(foo_ns, ullong, 0644);
+
+/*
+ * These functions define how to read and reset the environment variable.
+ *
+ * Common environment variables like ns-based and jiffy-based clocks have
+ * pre-define getters and resetters you can use. The parser can infer the type
+ * of the environment variable if you supply a measure unit in the constraint.
+ * If you define your own functions, make sure to add appropriate memory
+ * barriers if required.
+ * Some environment variables don't require a storage as they read a system
+ * state (e.g. preemption count). Those variables are never reset, so we don't
+ * define a reset function on monitors only relying on this type of variables.
+ */
+static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs_ha_percpu env, u64 time_ns)
+{
+	if (env == clk_ha_percpu)
+		return ha_get_clk_ns(ha_mon, env, time_ns);
+	else if (env == env1_ha_percpu)
+		return /* XXX: how do I read env1? */
+	else if (env == env2_ha_percpu)
+		return /* XXX: how do I read env2? */
+	return ENV_INVALID_VALUE;
+}
+
+static void ha_reset_env(struct ha_monitor *ha_mon, enum envs_ha_percpu env, u64 time_ns)
+{
+	if (env == clk_ha_percpu)
+		ha_reset_clk_ns(ha_mon, env, time_ns);
+}
+
+/*
+ * These functions are used to validate state transitions.
+ *
+ * They are generated by parsing the model, there is usually no need to change them.
+ * If the monitor requires a timer, there are functions responsible to arm it when
+ * the next state has a constraint, cancel it in any other case and to check
+ * that it didn't expire before the callback run. Transitions to the same state
+ * without a reset never affect timers.
+ */
+static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
+					enum states curr_state, enum events event,
+					enum states next_state, u64 time_ns)
+{
+	if (curr_state == S0_ha_percpu)
+		return ha_check_invariant_ns(ha_mon, clk_ha_percpu, time_ns, bar_ns(ha_mon));
+	else if (curr_state == S2_ha_percpu)
+		return ha_check_invariant_ns(ha_mon, clk_ha_percpu, time_ns, BAR_NS(ha_mon));
+	return true;
+}
+
+static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
+				    enum states curr_state, enum events event,
+				    enum states next_state, u64 time_ns)
+{
+	bool res = true;
+
+	if (curr_state == S0_ha_percpu && event == event0_ha_percpu)
+		ha_reset_env(ha_mon, clk_ha_percpu, time_ns);
+	else if (curr_state == S0_ha_percpu && event == event1_ha_percpu)
+		ha_reset_env(ha_mon, clk_ha_percpu, time_ns);
+	else if (curr_state == S1_ha_percpu && event == event0_ha_percpu)
+		ha_reset_env(ha_mon, clk_ha_percpu, time_ns);
+	else if (curr_state == S1_ha_percpu && event == event2_ha_percpu) {
+		res = ha_get_env(ha_mon, env1_ha_percpu, time_ns) == 0ull;
+		ha_reset_env(ha_mon, clk_ha_percpu, time_ns);
+	} else if (curr_state == S2_ha_percpu && event == event1_ha_percpu)
+		res = ha_monitor_env_invalid(ha_mon, clk_ha_percpu) ||
+		      ha_get_env(ha_mon, clk_ha_percpu, time_ns) < foo_ns;
+	else if (curr_state == S3_ha_percpu && event == event0_ha_percpu)
+		res = ha_monitor_env_invalid(ha_mon, clk_ha_percpu) ||
+		      (ha_get_env(ha_mon, clk_ha_percpu, time_ns) < FOO_NS &&
+		      ha_get_env(ha_mon, env2_ha_percpu, time_ns) == 0ull);
+	else if (curr_state == S3_ha_percpu && event == event1_ha_percpu) {
+		res = ha_monitor_env_invalid(ha_mon, clk_ha_percpu) ||
+		      (ha_get_env(ha_mon, clk_ha_percpu, time_ns) < 5000ull &&
+		      ha_get_env(ha_mon, env1_ha_percpu, time_ns) == 1ull);
+		ha_reset_env(ha_mon, clk_ha_percpu, time_ns);
+	}
+	return res;
+}
+
+static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
+				       enum states curr_state, enum events event,
+				       enum states next_state, u64 time_ns)
+{
+	if (next_state == curr_state && event != event0_ha_percpu)
+		return;
+	if (next_state == S0_ha_percpu)
+		ha_start_timer_ns(ha_mon, clk_ha_percpu, bar_ns(ha_mon), time_ns);
+	else if (next_state == S2_ha_percpu)
+		ha_start_timer_ns(ha_mon, clk_ha_percpu, BAR_NS(ha_mon), time_ns);
+	else if (curr_state == S0_ha_percpu)
+		ha_cancel_timer(ha_mon);
+	else if (curr_state == S2_ha_percpu)
+		ha_cancel_timer(ha_mon);
+}
+
+static bool ha_verify_constraint(struct ha_monitor *ha_mon,
+				 enum states curr_state, enum events event,
+				 enum states next_state, u64 time_ns)
+{
+	if (!ha_verify_invariants(ha_mon, curr_state, event, next_state, time_ns))
+		return false;
+
+	if (!ha_verify_guards(ha_mon, curr_state, event, next_state, time_ns))
+		return false;
+
+	ha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns);
+
+	return true;
+}
+
+static void handle_event0(void *data, /* XXX: fill header */)
+{
+	/* XXX: validate that this event always leads to the initial state */
+	da_handle_start_event(event0_ha_percpu);
+}
+
+static void handle_event1(void *data, /* XXX: fill header */)
+{
+	da_handle_event(event1_ha_percpu);
+}
+
+static void handle_event2(void *data, /* XXX: fill header */)
+{
+	da_handle_event(event2_ha_percpu);
+}
+
+static int enable_ha_percpu(void)
+{
+	int retval;
+
+	retval = ha_monitor_init();
+	if (retval)
+		return retval;
+
+	rv_attach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event0);
+	rv_attach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event1);
+	rv_attach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event2);
+
+	return 0;
+}
+
+static void disable_ha_percpu(void)
+{
+	rv_this.enabled = 0;
+
+	rv_detach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event0);
+	rv_detach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event1);
+	rv_detach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event2);
+
+	ha_monitor_destroy();
+}
+
+/*
+ * This is the monitor register section.
+ */
+static struct rv_monitor rv_this = {
+	.name = "ha_percpu",
+	.description = "auto-generated",
+	.enable = enable_ha_percpu,
+	.disable = disable_ha_percpu,
+	.reset = da_monitor_reset_all,
+	.enabled = 0,
+};
+
+static int __init register_ha_percpu(void)
+{
+	return rv_register_monitor(&rv_this, NULL);
+}
+
+static void __exit unregister_ha_percpu(void)
+{
+	rv_unregister_monitor(&rv_this);
+}
+
+module_init(register_ha_percpu);
+module_exit(unregister_ha_percpu);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("rvgen: auto-generated");
+MODULE_DESCRIPTION("ha_percpu: auto-generated");
diff --git a/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu.h b/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu.h
new file mode 100644
index 000000000..2538db4f6
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu.h
@@ -0,0 +1,72 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Automatically generated C representation of ha_percpu automaton
+ * For further information about this format, see kernel documentation:
+ *   Documentation/trace/rv/deterministic_automata.rst
+ */
+
+#define MONITOR_NAME ha_percpu
+
+enum states_ha_percpu {
+	S0_ha_percpu,
+	S1_ha_percpu,
+	S2_ha_percpu,
+	S3_ha_percpu,
+	state_max_ha_percpu,
+};
+
+#define INVALID_STATE state_max_ha_percpu
+
+enum events_ha_percpu {
+	event0_ha_percpu,
+	event1_ha_percpu,
+	event2_ha_percpu,
+	event_max_ha_percpu,
+};
+
+enum envs_ha_percpu {
+	clk_ha_percpu,
+	env1_ha_percpu,
+	env2_ha_percpu,
+	env_max_ha_percpu,
+	env_max_stored_ha_percpu = env1_ha_percpu,
+};
+
+_Static_assert(env_max_stored_ha_percpu <= MAX_HA_ENV_LEN, "Not enough slots");
+#define HA_CLK_NS
+
+struct automaton_ha_percpu {
+	char *state_names[state_max_ha_percpu];
+	char *event_names[event_max_ha_percpu];
+	char *env_names[env_max_ha_percpu];
+	unsigned char function[state_max_ha_percpu][event_max_ha_percpu];
+	unsigned char initial_state;
+	bool final_states[state_max_ha_percpu];
+};
+
+static const struct automaton_ha_percpu automaton_ha_percpu = {
+	.state_names = {
+		"S0",
+		"S1",
+		"S2",
+		"S3",
+	},
+	.event_names = {
+		"event0",
+		"event1",
+		"event2",
+	},
+	.env_names = {
+		"clk",
+		"env1",
+		"env2",
+	},
+	.function = {
+		{            S0_ha_percpu,            S1_ha_percpu,           INVALID_STATE },
+		{            S0_ha_percpu,           INVALID_STATE,            S2_ha_percpu },
+		{           INVALID_STATE,            S2_ha_percpu,            S3_ha_percpu },
+		{            S0_ha_percpu,            S1_ha_percpu,           INVALID_STATE },
+	},
+	.initial_state = S0_ha_percpu,
+	.final_states = { 1, 0, 0, 0 },
+};
diff --git a/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu_trace.h b/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu_trace.h
new file mode 100644
index 000000000..074ddff6a
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu_trace.h
@@ -0,0 +1,19 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_HA_PERCPU
+DEFINE_EVENT(event_da_monitor, event_ha_percpu,
+	     TP_PROTO(char *state, char *event, char *next_state, bool final_state),
+	     TP_ARGS(state, event, next_state, final_state));
+
+DEFINE_EVENT(error_da_monitor, error_ha_percpu,
+	     TP_PROTO(char *state, char *event),
+	     TP_ARGS(state, event));
+
+DEFINE_EVENT(error_env_da_monitor, error_env_ha_percpu,
+	     TP_PROTO(char *state, char *event, char *env),
+	     TP_ARGS(state, event, env));
+#endif /* CONFIG_RV_MON_HA_PERCPU */
diff --git a/tools/verification/rvgen/tests/golden/ltl_pertask/Kconfig b/tools/verification/rvgen/tests/golden/ltl_pertask/Kconfig
new file mode 100644
index 000000000..b37f46670
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/ltl_pertask/Kconfig
@@ -0,0 +1,9 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_LTL_PERTASK
+	depends on RV
+	# XXX: add dependencies if there
+	select LTL_MON_EVENTS_ID
+	bool "ltl_pertask monitor"
+	help
+	  auto-generated
diff --git a/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask.c b/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask.c
new file mode 100644
index 000000000..2c60b5c5b
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask.c
@@ -0,0 +1,107 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "ltl_pertask"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <trace/events/sched.h>
+ */
+#include <rv_trace.h>
+
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#include "ltl_pertask.h"
+#include <rv/ltl_monitor.h>
+
+static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon)
+{
+	/*
+	 * This is called everytime the Buchi automaton is triggered.
+	 *
+	 * This function could be used to fetch the atomic propositions which
+	 * are expensive to trace. It is possible only if the atomic proposition
+	 * does not need to be updated at precise time.
+	 *
+	 * It is recommended to use tracepoints and ltl_atom_update() instead.
+	 */
+}
+
+static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)
+{
+	/*
+	 * This should initialize as many atomic propositions as possible.
+	 *
+	 * @task_creation indicates whether the task is being created. This is
+	 * false if the task is already running before the monitor is enabled.
+	 */
+	ltl_atom_set(mon, LTL_EVENT_A, true/false);
+	ltl_atom_set(mon, LTL_EVENT_B, true/false);
+}
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ */
+static void handle_example_event(void *data, /* XXX: fill header */)
+{
+	ltl_atom_update(task, LTL_EVENT_A, true/false);
+}
+
+static int enable_ltl_pertask(void)
+{
+	int retval;
+
+	retval = ltl_monitor_init();
+	if (retval)
+		return retval;
+
+	rv_attach_trace_probe("ltl_pertask", /* XXX: tracepoint */, handle_example_event);
+
+	return 0;
+}
+
+static void disable_ltl_pertask(void)
+{
+	rv_detach_trace_probe("ltl_pertask", /* XXX: tracepoint */, handle_example_event);
+
+	ltl_monitor_destroy();
+}
+
+/*
+ * This is the monitor register section.
+ */
+static struct rv_monitor rv_this = {
+	.name = "ltl_pertask",
+	.description = "auto-generated",
+	.enable = enable_ltl_pertask,
+	.disable = disable_ltl_pertask,
+};
+
+static int __init register_ltl_pertask(void)
+{
+	return rv_register_monitor(&rv_this, NULL);
+}
+
+static void __exit unregister_ltl_pertask(void)
+{
+	rv_unregister_monitor(&rv_this);
+}
+
+module_init(register_ltl_pertask);
+module_exit(unregister_ltl_pertask);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("rvgen: auto-generated");
+MODULE_DESCRIPTION("ltl_pertask: auto-generated");
diff --git a/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask.h b/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask.h
new file mode 100644
index 000000000..7e5de351b
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask.h
@@ -0,0 +1,108 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * C implementation of Buchi automaton, automatically generated by
+ * tools/verification/rvgen from the linear temporal logic specification.
+ * For further information, see kernel documentation:
+ *   Documentation/trace/rv/linear_temporal_logic.rst
+ */
+
+#include <linux/rv.h>
+
+#define MONITOR_NAME ltl_pertask
+
+enum ltl_atom {
+	LTL_EVENT_A,
+	LTL_EVENT_B,
+	LTL_NUM_ATOM
+};
+static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM);
+
+static const char *ltl_atom_str(enum ltl_atom atom)
+{
+	static const char *const names[] = {
+		"ev_a",
+		"ev_b",
+	};
+
+	return names[atom];
+}
+
+enum ltl_buchi_state {
+	S0,
+	S1,
+	S2,
+	S3,
+	S4,
+	RV_NUM_BA_STATES
+};
+static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);
+
+static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)
+{
+	bool event_b = test_bit(LTL_EVENT_B, mon->atoms);
+	bool event_a = test_bit(LTL_EVENT_A, mon->atoms);
+	bool val1 = !event_a;
+
+	if (val1)
+		__set_bit(S0, mon->states);
+	if (true)
+		__set_bit(S1, mon->states);
+	if (event_b)
+		__set_bit(S4, mon->states);
+}
+
+static void
+ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)
+{
+	bool event_b = test_bit(LTL_EVENT_B, mon->atoms);
+	bool event_a = test_bit(LTL_EVENT_A, mon->atoms);
+	bool val1 = !event_a;
+
+	switch (state) {
+	case S0:
+		if (val1)
+			__set_bit(S0, next);
+		if (true)
+			__set_bit(S1, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	case S1:
+		if (true)
+			__set_bit(S1, next);
+		if (true && val1)
+			__set_bit(S2, next);
+		if (event_b && val1)
+			__set_bit(S3, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	case S2:
+		if (true)
+			__set_bit(S1, next);
+		if (true && val1)
+			__set_bit(S2, next);
+		if (event_b && val1)
+			__set_bit(S3, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	case S3:
+		if (val1)
+			__set_bit(S0, next);
+		if (true)
+			__set_bit(S1, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	case S4:
+		if (val1)
+			__set_bit(S0, next);
+		if (true)
+			__set_bit(S1, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	}
+}
diff --git a/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask_trace.h b/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask_trace.h
new file mode 100644
index 000000000..ebd53621a
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask_trace.h
@@ -0,0 +1,14 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_LTL_PERTASK
+DEFINE_EVENT(event_ltl_monitor_id, event_ltl_pertask,
+	     TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next),
+	     TP_ARGS(task, states, atoms, next));
+DEFINE_EVENT(error_ltl_monitor_id, error_ltl_pertask,
+	     TP_PROTO(struct task_struct *task),
+	     TP_ARGS(task));
+#endif /* CONFIG_RV_MON_LTL_PERTASK */
diff --git a/tools/verification/rvgen/tests/golden/test_bak_kunit/Kconfig b/tools/verification/rvgen/tests/golden/test_bak_kunit/Kconfig
new file mode 100644
index 000000000..175a416f8
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_bak_kunit/Kconfig
@@ -0,0 +1,9 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_TEST_BAK_KUNIT
+	depends on RV
+	# XXX: add dependencies if there
+	select LTL_MON_EVENTS_ID
+	bool "test_bak_kunit monitor"
+	help
+	  auto-generated
diff --git a/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit.c b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit.c
new file mode 100644
index 000000000..16579c1c6
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit.c
@@ -0,0 +1,107 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "test_bak_kunit"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <trace/events/sched.h>
+ */
+#include <rv_trace.h>
+
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#include "test_bak_kunit.h"
+#include <rv/ltl_monitor.h>
+
+static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon)
+{
+	/*
+	 * This is called everytime the Buchi automaton is triggered.
+	 *
+	 * This function could be used to fetch the atomic propositions which
+	 * are expensive to trace. It is possible only if the atomic proposition
+	 * does not need to be updated at precise time.
+	 *
+	 * It is recommended to use tracepoints and ltl_atom_update() instead.
+	 */
+}
+
+static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)
+{
+	/*
+	 * This should initialize as many atomic propositions as possible.
+	 *
+	 * @task_creation indicates whether the task is being created. This is
+	 * false if the task is already running before the monitor is enabled.
+	 */
+	ltl_atom_set(mon, LTL_EVENT_A, true/false);
+	ltl_atom_set(mon, LTL_EVENT_B, true/false);
+}
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ */
+static void handle_example_event(void *data, /* XXX: fill header */)
+{
+	ltl_atom_update(task, LTL_EVENT_A, true/false);
+}
+
+static int enable_test_bak_kunit(void)
+{
+	int retval;
+
+	retval = ltl_monitor_init();
+	if (retval)
+		return retval;
+
+	rv_attach_trace_probe("test_bak_kunit", /* XXX: tracepoint */, handle_example_event);
+
+	return 0;
+}
+
+static void disable_test_bak_kunit(void)
+{
+	rv_detach_trace_probe("test_bak_kunit", /* XXX: tracepoint */, handle_example_event);
+
+	ltl_monitor_destroy();
+}
+
+/*
+ * This is the monitor register section.
+ */
+static struct rv_monitor rv_this = {
+	.name = "test_bak_kunit",
+	.description = "auto-generated",
+	.enable = enable_test_bak_kunit,
+	.disable = disable_test_bak_kunit,
+};
+
+static int __init register_test_bak_kunit(void)
+{
+	return rv_register_monitor(&rv_this, NULL);
+}
+
+static void __exit unregister_test_bak_kunit(void)
+{
+	rv_unregister_monitor(&rv_this);
+}
+
+module_init(register_test_bak_kunit);
+module_exit(unregister_test_bak_kunit);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("rvgen: auto-generated");
+MODULE_DESCRIPTION("test_bak_kunit: auto-generated");
diff --git a/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit.h b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit.h
new file mode 100644
index 000000000..2bfe4e37c
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit.h
@@ -0,0 +1,108 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * C implementation of Buchi automaton, automatically generated by
+ * tools/verification/rvgen from the linear temporal logic specification.
+ * For further information, see kernel documentation:
+ *   Documentation/trace/rv/linear_temporal_logic.rst
+ */
+
+#include <linux/rv.h>
+
+#define MONITOR_NAME test_bak_kunit
+
+enum ltl_atom {
+	LTL_EVENT_A,
+	LTL_EVENT_B,
+	LTL_NUM_ATOM
+};
+static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM);
+
+static const char *ltl_atom_str(enum ltl_atom atom)
+{
+	static const char *const names[] = {
+		"ev_a",
+		"ev_b",
+	};
+
+	return names[atom];
+}
+
+enum ltl_buchi_state {
+	S0,
+	S1,
+	S2,
+	S3,
+	S4,
+	RV_NUM_BA_STATES
+};
+static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);
+
+static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)
+{
+	bool event_b = test_bit(LTL_EVENT_B, mon->atoms);
+	bool event_a = test_bit(LTL_EVENT_A, mon->atoms);
+	bool val1 = !event_a;
+
+	if (val1)
+		__set_bit(S0, mon->states);
+	if (true)
+		__set_bit(S1, mon->states);
+	if (event_b)
+		__set_bit(S4, mon->states);
+}
+
+static void
+ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)
+{
+	bool event_b = test_bit(LTL_EVENT_B, mon->atoms);
+	bool event_a = test_bit(LTL_EVENT_A, mon->atoms);
+	bool val1 = !event_a;
+
+	switch (state) {
+	case S0:
+		if (val1)
+			__set_bit(S0, next);
+		if (true)
+			__set_bit(S1, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	case S1:
+		if (true)
+			__set_bit(S1, next);
+		if (true && val1)
+			__set_bit(S2, next);
+		if (event_b && val1)
+			__set_bit(S3, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	case S2:
+		if (true)
+			__set_bit(S1, next);
+		if (true && val1)
+			__set_bit(S2, next);
+		if (event_b && val1)
+			__set_bit(S3, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	case S3:
+		if (val1)
+			__set_bit(S0, next);
+		if (true)
+			__set_bit(S1, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	case S4:
+		if (val1)
+			__set_bit(S0, next);
+		if (true)
+			__set_bit(S1, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	}
+}
diff --git a/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.c b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.c
new file mode 100644
index 000000000..e2b935403
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.c
@@ -0,0 +1,33 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/kernel.h>
+#include <linux/rv.h>
+#include <rv/kunit.h>
+/*
+ * XXX: include required headers, e.g.,
+ * #include <linux/sched.h>
+ */
+#include "test_bak_kunit_kunit.h"
+
+#if IS_REACHABLE(CONFIG_RV_MON_TEST_BAK_KUNIT)
+
+static void rv_test_test_bak_kunit(struct kunit *test)
+{
+	struct rv_kunit_ctx *ctx = test->priv;
+	/*
+	 * If you need to create task_structs with rv_kunit_alloc_mock_task()
+	 * do it BEFORE preparing the test.
+	 */
+
+	prepare_test(test, &rv_test_bak_kunit_ops.mon);
+
+	/*
+	 * XXX: write the test here
+	 * e.g.
+	 * RV_KUNIT_EXPECT_REACTION_HERE(test, ctx)
+	 *	rv_test_bak_kunit_ops.handle_event(args);
+	 */
+}
+
+#else
+#define rv_test_test_bak_kunit rv_test_stub
+#endif
diff --git a/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.c.old b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.c.old
new file mode 100644
index 000000000..f747925bf
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.c.old
@@ -0,0 +1 @@
+DUMMY
diff --git a/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.h b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.h
new file mode 100644
index 000000000..585c4803b
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.h
@@ -0,0 +1,22 @@
+/* SPDX-License-Identifier: GPL-2.0-only */
+/*
+ * Automatically generated by rvgen kunit.
+ * May need manual intervention for function prototypes that couldn't be
+ * found (e.g. are in another file) or variables to be exported.
+ */
+
+#ifndef __TEST_BAK_KUNIT_KUNIT_H
+#define __TEST_BAK_KUNIT_KUNIT_H
+
+#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
+
+#include <linux/rv.h>
+#include <rv/kunit.h>
+
+extern const struct rv_test_bak_kunit_ops {
+	struct rv_kunit_mon mon;
+	void (*handle_example_event)(void *data, /* XXX: fill header */);
+} rv_test_bak_kunit_ops;
+#endif
+
+#endif /* __TEST_BAK_KUNIT_KUNIT_H */
diff --git a/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_trace.h b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_trace.h
new file mode 100644
index 000000000..b98420883
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_trace.h
@@ -0,0 +1,14 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_TEST_BAK_KUNIT
+DEFINE_EVENT(event_ltl_monitor_id, event_test_bak_kunit,
+	     TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next),
+	     TP_ARGS(task, states, atoms, next));
+DEFINE_EVENT(error_ltl_monitor_id, error_test_bak_kunit,
+	     TP_PROTO(struct task_struct *task),
+	     TP_ARGS(task));
+#endif /* CONFIG_RV_MON_TEST_BAK_KUNIT */
diff --git a/tools/verification/rvgen/tests/golden/test_container/Kconfig b/tools/verification/rvgen/tests/golden/test_container/Kconfig
new file mode 100644
index 000000000..2becb65dd
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_container/Kconfig
@@ -0,0 +1,5 @@
+config RV_MON_TEST_CONTAINER
+	depends on RV
+	bool "test_container monitor"
+	help
+	  Test container for grouping monitors
diff --git a/tools/verification/rvgen/tests/golden/test_container/test_container.c b/tools/verification/rvgen/tests/golden/test_container/test_container.c
new file mode 100644
index 000000000..e7e34592c
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_container/test_container.c
@@ -0,0 +1,35 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+
+#define MODULE_NAME "test_container"
+
+#include "test_container.h"
+
+struct rv_monitor rv_test_container = {
+	.name = "test_container",
+	.description = "Test container for grouping monitors",
+	.enable = NULL,
+	.disable = NULL,
+	.reset = NULL,
+	.enabled = 0,
+};
+
+static int __init register_test_container(void)
+{
+	return rv_register_monitor(&rv_test_container, NULL);
+}
+
+static void __exit unregister_test_container(void)
+{
+	rv_unregister_monitor(&rv_test_container);
+}
+
+module_init(register_test_container);
+module_exit(unregister_test_container);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("rvgen: auto-generated");
+MODULE_DESCRIPTION("test_container: Test container for grouping monitors");
diff --git a/tools/verification/rvgen/tests/golden/test_container/test_container.h b/tools/verification/rvgen/tests/golden/test_container/test_container.h
new file mode 100644
index 000000000..83e434432
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_container/test_container.h
@@ -0,0 +1,3 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+extern struct rv_monitor rv_test_container;
diff --git a/tools/verification/rvgen/tests/golden/test_da/Kconfig b/tools/verification/rvgen/tests/golden/test_da/Kconfig
new file mode 100644
index 000000000..0143a148e
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_da/Kconfig
@@ -0,0 +1,9 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_TEST_DA
+	depends on RV
+	# XXX: add dependencies if there
+	select DA_MON_EVENTS_IMPLICIT
+	bool "test_da monitor"
+	help
+	  auto-generated
diff --git a/tools/verification/rvgen/tests/golden/test_da/test_da.c b/tools/verification/rvgen/tests/golden/test_da/test_da.c
new file mode 100644
index 000000000..59b8dfabb
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_da/test_da.c
@@ -0,0 +1,95 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "test_da"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <trace/events/sched.h>
+ */
+#include <rv_trace.h>
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#define RV_MON_TYPE RV_MON_PER_CPU
+#include "test_da.h"
+#include <rv/da_monitor.h>
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ *
+ */
+static void handle_event_1(void *data, /* XXX: fill header */)
+{
+	da_handle_event(event_1_test_da);
+}
+
+static void handle_event_2(void *data, /* XXX: fill header */)
+{
+	/* XXX: validate that this event always leads to the initial state */
+	da_handle_start_event(event_2_test_da);
+}
+
+static int enable_test_da(void)
+{
+	int retval;
+
+	retval = da_monitor_init();
+	if (retval)
+		return retval;
+
+	rv_attach_trace_probe("test_da", /* XXX: tracepoint */, handle_event_1);
+	rv_attach_trace_probe("test_da", /* XXX: tracepoint */, handle_event_2);
+
+	return 0;
+}
+
+static void disable_test_da(void)
+{
+	rv_this.enabled = 0;
+
+	rv_detach_trace_probe("test_da", /* XXX: tracepoint */, handle_event_1);
+	rv_detach_trace_probe("test_da", /* XXX: tracepoint */, handle_event_2);
+
+	da_monitor_destroy();
+}
+
+/*
+ * This is the monitor register section.
+ */
+static struct rv_monitor rv_this = {
+	.name = "test_da",
+	.description = "auto-generated",
+	.enable = enable_test_da,
+	.disable = disable_test_da,
+	.reset = da_monitor_reset_all,
+	.enabled = 0,
+};
+
+static int __init register_test_da(void)
+{
+	return rv_register_monitor(&rv_this, NULL);
+}
+
+static void __exit unregister_test_da(void)
+{
+	rv_unregister_monitor(&rv_this);
+}
+
+module_init(register_test_da);
+module_exit(unregister_test_da);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("rvgen: auto-generated");
+MODULE_DESCRIPTION("test_da: auto-generated");
diff --git a/tools/verification/rvgen/tests/golden/test_da/test_da.h b/tools/verification/rvgen/tests/golden/test_da/test_da.h
new file mode 100644
index 000000000..d55795efb
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_da/test_da.h
@@ -0,0 +1,47 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Automatically generated C representation of test_da automaton
+ * For further information about this format, see kernel documentation:
+ *   Documentation/trace/rv/deterministic_automata.rst
+ */
+
+#define MONITOR_NAME test_da
+
+enum states_test_da {
+	state_a_test_da,
+	state_b_test_da,
+	state_max_test_da,
+};
+
+#define INVALID_STATE state_max_test_da
+
+enum events_test_da {
+	event_1_test_da,
+	event_2_test_da,
+	event_max_test_da,
+};
+
+struct automaton_test_da {
+	char *state_names[state_max_test_da];
+	char *event_names[event_max_test_da];
+	unsigned char function[state_max_test_da][event_max_test_da];
+	unsigned char initial_state;
+	bool final_states[state_max_test_da];
+};
+
+static const struct automaton_test_da automaton_test_da = {
+	.state_names = {
+		"state_a",
+		"state_b",
+	},
+	.event_names = {
+		"event_1",
+		"event_2",
+	},
+	.function = {
+		{       state_b_test_da,       state_a_test_da },
+		{         INVALID_STATE,       state_a_test_da },
+	},
+	.initial_state = state_a_test_da,
+	.final_states = { 1, 0 },
+};
diff --git a/tools/verification/rvgen/tests/golden/test_da/test_da_trace.h b/tools/verification/rvgen/tests/golden/test_da/test_da_trace.h
new file mode 100644
index 000000000..8bd67115d
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_da/test_da_trace.h
@@ -0,0 +1,15 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_TEST_DA
+DEFINE_EVENT(event_da_monitor, event_test_da,
+	     TP_PROTO(char *state, char *event, char *next_state, bool final_state),
+	     TP_ARGS(state, event, next_state, final_state));
+
+DEFINE_EVENT(error_da_monitor, error_test_da,
+	     TP_PROTO(char *state, char *event),
+	     TP_ARGS(state, event));
+#endif /* CONFIG_RV_MON_TEST_DA */
diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/Kconfig b/tools/verification/rvgen/tests/golden/test_da_kunit/Kconfig
new file mode 100644
index 000000000..6d664ba56
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_da_kunit/Kconfig
@@ -0,0 +1,9 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_TEST_DA_KUNIT
+	depends on RV
+	# XXX: add dependencies if there
+	select DA_MON_EVENTS_IMPLICIT
+	bool "test_da_kunit monitor"
+	help
+	  auto-generated
diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.c b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.c
new file mode 100644
index 000000000..effd26548
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.c
@@ -0,0 +1,107 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "test_da_kunit"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <trace/events/sched.h>
+ */
+#include <rv_trace.h>
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#define RV_MON_TYPE RV_MON_PER_CPU
+#include "test_da_kunit.h"
+#include <rv/da_monitor.h>
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ *
+ */
+static void handle_event_1(void *data, /* XXX: fill header */)
+{
+	da_handle_event(event_1_test_da_kunit);
+}
+
+static void handle_event_2(void *data, /* XXX: fill header */)
+{
+	/* XXX: validate that this event always leads to the initial state */
+	da_handle_start_event(event_2_test_da_kunit);
+}
+
+static int enable_test_da_kunit(void)
+{
+	int retval;
+
+	retval = da_monitor_init();
+	if (retval)
+		return retval;
+
+	rv_attach_trace_probe("test_da_kunit", /* XXX: tracepoint */, handle_event_1);
+	rv_attach_trace_probe("test_da_kunit", /* XXX: tracepoint */, handle_event_2);
+
+	return 0;
+}
+
+static void disable_test_da_kunit(void)
+{
+	rv_this.enabled = 0;
+
+	rv_detach_trace_probe("test_da_kunit", /* XXX: tracepoint */, handle_event_1);
+	rv_detach_trace_probe("test_da_kunit", /* XXX: tracepoint */, handle_event_2);
+
+	da_monitor_destroy();
+}
+
+/*
+ * This is the monitor register section.
+ */
+static struct rv_monitor rv_this = {
+	.name = "test_da_kunit",
+	.description = "auto-generated",
+	.enable = enable_test_da_kunit,
+	.disable = disable_test_da_kunit,
+	.reset = da_monitor_reset_all,
+	.enabled = 0,
+};
+
+static int __init register_test_da_kunit(void)
+{
+	return rv_register_monitor(&rv_this, NULL);
+}
+
+static void __exit unregister_test_da_kunit(void)
+{
+	rv_unregister_monitor(&rv_this);
+}
+
+module_init(register_test_da_kunit);
+module_exit(unregister_test_da_kunit);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("rvgen: auto-generated");
+MODULE_DESCRIPTION("test_da_kunit: auto-generated");
+
+#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
+#include <kunit/visibility.h>
+#include "test_da_kunit_kunit.h"
+
+const struct rv_test_da_kunit_ops rv_test_da_kunit_ops = {
+	.mon = RV_MON_OPS_INIT(),
+	.handle_event_1 = handle_event_1,
+	.handle_event_2 = handle_event_2,
+};
+EXPORT_SYMBOL_IF_KUNIT(rv_test_da_kunit_ops);
+#endif
diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.h b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.h
new file mode 100644
index 000000000..290a9454c
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.h
@@ -0,0 +1,47 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Automatically generated C representation of test_da_kunit automaton
+ * For further information about this format, see kernel documentation:
+ *   Documentation/trace/rv/deterministic_automata.rst
+ */
+
+#define MONITOR_NAME test_da_kunit
+
+enum states_test_da_kunit {
+	state_a_test_da_kunit,
+	state_b_test_da_kunit,
+	state_max_test_da_kunit,
+};
+
+#define INVALID_STATE state_max_test_da_kunit
+
+enum events_test_da_kunit {
+	event_1_test_da_kunit,
+	event_2_test_da_kunit,
+	event_max_test_da_kunit,
+};
+
+struct automaton_test_da_kunit {
+	char *state_names[state_max_test_da_kunit];
+	char *event_names[event_max_test_da_kunit];
+	unsigned char function[state_max_test_da_kunit][event_max_test_da_kunit];
+	unsigned char initial_state;
+	bool final_states[state_max_test_da_kunit];
+};
+
+static const struct automaton_test_da_kunit automaton_test_da_kunit = {
+	.state_names = {
+		"state_a",
+		"state_b",
+	},
+	.event_names = {
+		"event_1",
+		"event_2",
+	},
+	.function = {
+		{       state_b_test_da_kunit,       state_a_test_da_kunit },
+		{               INVALID_STATE,       state_a_test_da_kunit },
+	},
+	.initial_state = state_a_test_da_kunit,
+	.final_states = { 1, 0 },
+};
diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.c b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.c
new file mode 100644
index 000000000..17826a5c4
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.c
@@ -0,0 +1,33 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/kernel.h>
+#include <linux/rv.h>
+#include <rv/kunit.h>
+/*
+ * XXX: include required headers, e.g.,
+ * #include <linux/sched.h>
+ */
+#include "test_da_kunit_kunit.h"
+
+#if IS_REACHABLE(CONFIG_RV_MON_TEST_DA_KUNIT)
+
+static void rv_test_test_da_kunit(struct kunit *test)
+{
+	struct rv_kunit_ctx *ctx = test->priv;
+	/*
+	 * If you need to create task_structs with rv_kunit_alloc_mock_task()
+	 * do it BEFORE preparing the test.
+	 */
+
+	prepare_test(test, &rv_test_da_kunit_ops.mon);
+
+	/*
+	 * XXX: write the test here
+	 * e.g.
+	 * RV_KUNIT_EXPECT_REACTION_HERE(test, ctx)
+	 *	rv_test_da_kunit_ops.handle_event(args);
+	 */
+}
+
+#else
+#define rv_test_test_da_kunit rv_test_stub
+#endif
diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.h b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.h
new file mode 100644
index 000000000..0094215ff
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.h
@@ -0,0 +1,23 @@
+/* SPDX-License-Identifier: GPL-2.0-only */
+/*
+ * Automatically generated by rvgen kunit.
+ * May need manual intervention for function prototypes that couldn't be
+ * found (e.g. are in another file) or variables to be exported.
+ */
+
+#ifndef __TEST_DA_KUNIT_KUNIT_H
+#define __TEST_DA_KUNIT_KUNIT_H
+
+#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
+
+#include <linux/rv.h>
+#include <rv/kunit.h>
+
+extern const struct rv_test_da_kunit_ops {
+	struct rv_kunit_mon mon;
+	void (*handle_event_1)(void *data, /* XXX: fill header */);
+	void (*handle_event_2)(void *data, /* XXX: fill header */);
+} rv_test_da_kunit_ops;
+#endif
+
+#endif /* __TEST_DA_KUNIT_KUNIT_H */
diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_trace.h b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_trace.h
new file mode 100644
index 000000000..16804a79e
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_trace.h
@@ -0,0 +1,15 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_TEST_DA_KUNIT
+DEFINE_EVENT(event_da_monitor, event_test_da_kunit,
+	     TP_PROTO(char *state, char *event, char *next_state, bool final_state),
+	     TP_ARGS(state, event, next_state, final_state));
+
+DEFINE_EVENT(error_da_monitor, error_test_da_kunit,
+	     TP_PROTO(char *state, char *event),
+	     TP_ARGS(state, event));
+#endif /* CONFIG_RV_MON_TEST_DA_KUNIT */
diff --git a/tools/verification/rvgen/tests/golden/test_ha/Kconfig b/tools/verification/rvgen/tests/golden/test_ha/Kconfig
new file mode 100644
index 000000000..f4048290c
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_ha/Kconfig
@@ -0,0 +1,9 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_TEST_HA
+	depends on RV
+	# XXX: add dependencies if there
+	select HA_MON_EVENTS_ID
+	bool "test_ha monitor"
+	help
+	  auto-generated
diff --git a/tools/verification/rvgen/tests/golden/test_ha/test_ha.c b/tools/verification/rvgen/tests/golden/test_ha/test_ha.c
new file mode 100644
index 000000000..9047ff725
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_ha/test_ha.c
@@ -0,0 +1,230 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "test_ha"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <trace/events/sched.h>
+ */
+#include <rv_trace.h>
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#define RV_MON_TYPE RV_MON_PER_TASK
+/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */
+#define HA_TIMER_TYPE HA_TIMER_HRTIMER
+#include "test_ha.h"
+#include <rv/ha_monitor.h>
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ *
+ */
+#define BAR_NS(ha_mon) /* XXX: what is BAR_NS(ha_mon)? */
+
+#define FOO_NS /* XXX: what is FOO_NS? */
+
+static inline u64 bar_ns(struct ha_monitor *ha_mon)
+{
+	return /* XXX: what is bar_ns(ha_mon)? */;
+}
+
+static u64 foo_ns = /* XXX: default value */;
+module_param(foo_ns, ullong, 0644);
+
+/*
+ * These functions define how to read and reset the environment variable.
+ *
+ * Common environment variables like ns-based and jiffy-based clocks have
+ * pre-define getters and resetters you can use. The parser can infer the type
+ * of the environment variable if you supply a measure unit in the constraint.
+ * If you define your own functions, make sure to add appropriate memory
+ * barriers if required.
+ * Some environment variables don't require a storage as they read a system
+ * state (e.g. preemption count). Those variables are never reset, so we don't
+ * define a reset function on monitors only relying on this type of variables.
+ */
+static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs_test_ha env, u64 time_ns)
+{
+	if (env == clk_test_ha)
+		return ha_get_clk_ns(ha_mon, env, time_ns);
+	else if (env == env1_test_ha)
+		return /* XXX: how do I read env1? */
+	else if (env == env2_test_ha)
+		return /* XXX: how do I read env2? */
+	return ENV_INVALID_VALUE;
+}
+
+static void ha_reset_env(struct ha_monitor *ha_mon, enum envs_test_ha env, u64 time_ns)
+{
+	if (env == clk_test_ha)
+		ha_reset_clk_ns(ha_mon, env, time_ns);
+}
+
+/*
+ * These functions are used to validate state transitions.
+ *
+ * They are generated by parsing the model, there is usually no need to change them.
+ * If the monitor requires a timer, there are functions responsible to arm it when
+ * the next state has a constraint, cancel it in any other case and to check
+ * that it didn't expire before the callback run. Transitions to the same state
+ * without a reset never affect timers.
+ */
+static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
+					enum states curr_state, enum events event,
+					enum states next_state, u64 time_ns)
+{
+	if (curr_state == S0_test_ha)
+		return ha_check_invariant_ns(ha_mon, clk_test_ha, time_ns, bar_ns(ha_mon));
+	else if (curr_state == S2_test_ha)
+		return ha_check_invariant_ns(ha_mon, clk_test_ha, time_ns, BAR_NS(ha_mon));
+	return true;
+}
+
+static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
+				    enum states curr_state, enum events event,
+				    enum states next_state, u64 time_ns)
+{
+	bool res = true;
+
+	if (curr_state == S0_test_ha && event == event0_test_ha)
+		ha_reset_env(ha_mon, clk_test_ha, time_ns);
+	else if (curr_state == S0_test_ha && event == event1_test_ha)
+		ha_reset_env(ha_mon, clk_test_ha, time_ns);
+	else if (curr_state == S1_test_ha && event == event0_test_ha)
+		ha_reset_env(ha_mon, clk_test_ha, time_ns);
+	else if (curr_state == S1_test_ha && event == event2_test_ha) {
+		res = ha_get_env(ha_mon, env1_test_ha, time_ns) == 0ull;
+		ha_reset_env(ha_mon, clk_test_ha, time_ns);
+	} else if (curr_state == S2_test_ha && event == event1_test_ha)
+		res = ha_monitor_env_invalid(ha_mon, clk_test_ha) ||
+		      ha_get_env(ha_mon, clk_test_ha, time_ns) < foo_ns;
+	else if (curr_state == S3_test_ha && event == event0_test_ha)
+		res = ha_monitor_env_invalid(ha_mon, clk_test_ha) ||
+		      (ha_get_env(ha_mon, clk_test_ha, time_ns) < FOO_NS &&
+		      ha_get_env(ha_mon, env2_test_ha, time_ns) == 0ull);
+	else if (curr_state == S3_test_ha && event == event1_test_ha) {
+		res = ha_monitor_env_invalid(ha_mon, clk_test_ha) ||
+		      (ha_get_env(ha_mon, clk_test_ha, time_ns) < 5000ull &&
+		      ha_get_env(ha_mon, env1_test_ha, time_ns) == 1ull);
+		ha_reset_env(ha_mon, clk_test_ha, time_ns);
+	}
+	return res;
+}
+
+static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
+				       enum states curr_state, enum events event,
+				       enum states next_state, u64 time_ns)
+{
+	if (next_state == curr_state && event != event0_test_ha)
+		return;
+	if (next_state == S0_test_ha)
+		ha_start_timer_ns(ha_mon, clk_test_ha, bar_ns(ha_mon), time_ns);
+	else if (next_state == S2_test_ha)
+		ha_start_timer_ns(ha_mon, clk_test_ha, BAR_NS(ha_mon), time_ns);
+	else if (curr_state == S0_test_ha)
+		ha_cancel_timer(ha_mon);
+	else if (curr_state == S2_test_ha)
+		ha_cancel_timer(ha_mon);
+}
+
+static bool ha_verify_constraint(struct ha_monitor *ha_mon,
+				 enum states curr_state, enum events event,
+				 enum states next_state, u64 time_ns)
+{
+	if (!ha_verify_invariants(ha_mon, curr_state, event, next_state, time_ns))
+		return false;
+
+	if (!ha_verify_guards(ha_mon, curr_state, event, next_state, time_ns))
+		return false;
+
+	ha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns);
+
+	return true;
+}
+
+static void handle_event0(void *data, /* XXX: fill header */)
+{
+	/* XXX: validate that this event always leads to the initial state */
+	struct task_struct *p = /* XXX: how do I get p? */;
+	da_handle_start_event(p, event0_test_ha);
+}
+
+static void handle_event1(void *data, /* XXX: fill header */)
+{
+	struct task_struct *p = /* XXX: how do I get p? */;
+	da_handle_event(p, event1_test_ha);
+}
+
+static void handle_event2(void *data, /* XXX: fill header */)
+{
+	struct task_struct *p = /* XXX: how do I get p? */;
+	da_handle_event(p, event2_test_ha);
+}
+
+static int enable_test_ha(void)
+{
+	int retval;
+
+	retval = ha_monitor_init();
+	if (retval)
+		return retval;
+
+	rv_attach_trace_probe("test_ha", /* XXX: tracepoint */, handle_event0);
+	rv_attach_trace_probe("test_ha", /* XXX: tracepoint */, handle_event1);
+	rv_attach_trace_probe("test_ha", /* XXX: tracepoint */, handle_event2);
+
+	return 0;
+}
+
+static void disable_test_ha(void)
+{
+	rv_this.enabled = 0;
+
+	rv_detach_trace_probe("test_ha", /* XXX: tracepoint */, handle_event0);
+	rv_detach_trace_probe("test_ha", /* XXX: tracepoint */, handle_event1);
+	rv_detach_trace_probe("test_ha", /* XXX: tracepoint */, handle_event2);
+
+	ha_monitor_destroy();
+}
+
+/*
+ * This is the monitor register section.
+ */
+static struct rv_monitor rv_this = {
+	.name = "test_ha",
+	.description = "auto-generated",
+	.enable = enable_test_ha,
+	.disable = disable_test_ha,
+	.reset = da_monitor_reset_all,
+	.enabled = 0,
+};
+
+static int __init register_test_ha(void)
+{
+	return rv_register_monitor(&rv_this, NULL);
+}
+
+static void __exit unregister_test_ha(void)
+{
+	rv_unregister_monitor(&rv_this);
+}
+
+module_init(register_test_ha);
+module_exit(unregister_test_ha);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("rvgen: auto-generated");
+MODULE_DESCRIPTION("test_ha: auto-generated");
diff --git a/tools/verification/rvgen/tests/golden/test_ha/test_ha.h b/tools/verification/rvgen/tests/golden/test_ha/test_ha.h
new file mode 100644
index 000000000..949fa4453
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_ha/test_ha.h
@@ -0,0 +1,72 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Automatically generated C representation of test_ha automaton
+ * For further information about this format, see kernel documentation:
+ *   Documentation/trace/rv/deterministic_automata.rst
+ */
+
+#define MONITOR_NAME test_ha
+
+enum states_test_ha {
+	S0_test_ha,
+	S1_test_ha,
+	S2_test_ha,
+	S3_test_ha,
+	state_max_test_ha,
+};
+
+#define INVALID_STATE state_max_test_ha
+
+enum events_test_ha {
+	event0_test_ha,
+	event1_test_ha,
+	event2_test_ha,
+	event_max_test_ha,
+};
+
+enum envs_test_ha {
+	clk_test_ha,
+	env1_test_ha,
+	env2_test_ha,
+	env_max_test_ha,
+	env_max_stored_test_ha = env1_test_ha,
+};
+
+_Static_assert(env_max_stored_test_ha <= MAX_HA_ENV_LEN, "Not enough slots");
+#define HA_CLK_NS
+
+struct automaton_test_ha {
+	char *state_names[state_max_test_ha];
+	char *event_names[event_max_test_ha];
+	char *env_names[env_max_test_ha];
+	unsigned char function[state_max_test_ha][event_max_test_ha];
+	unsigned char initial_state;
+	bool final_states[state_max_test_ha];
+};
+
+static const struct automaton_test_ha automaton_test_ha = {
+	.state_names = {
+		"S0",
+		"S1",
+		"S2",
+		"S3",
+	},
+	.event_names = {
+		"event0",
+		"event1",
+		"event2",
+	},
+	.env_names = {
+		"clk",
+		"env1",
+		"env2",
+	},
+	.function = {
+		{            S0_test_ha,            S1_test_ha,         INVALID_STATE },
+		{            S0_test_ha,         INVALID_STATE,            S2_test_ha },
+		{         INVALID_STATE,            S2_test_ha,            S3_test_ha },
+		{            S0_test_ha,            S1_test_ha,         INVALID_STATE },
+	},
+	.initial_state = S0_test_ha,
+	.final_states = { 1, 0, 0, 0 },
+};
diff --git a/tools/verification/rvgen/tests/golden/test_ha/test_ha_trace.h b/tools/verification/rvgen/tests/golden/test_ha/test_ha_trace.h
new file mode 100644
index 000000000..381bafcb3
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_ha/test_ha_trace.h
@@ -0,0 +1,19 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_TEST_HA
+DEFINE_EVENT(event_da_monitor_id, event_test_ha,
+	     TP_PROTO(int id, char *state, char *event, char *next_state, bool final_state),
+	     TP_ARGS(id, state, event, next_state, final_state));
+
+DEFINE_EVENT(error_da_monitor_id, error_test_ha,
+	     TP_PROTO(int id, char *state, char *event),
+	     TP_ARGS(id, state, event));
+
+DEFINE_EVENT(error_env_da_monitor_id, error_env_test_ha,
+	     TP_PROTO(int id, char *state, char *event, char *env),
+	     TP_ARGS(id, state, event, env));
+#endif /* CONFIG_RV_MON_TEST_HA */
diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/Kconfig b/tools/verification/rvgen/tests/golden/test_ha_kunit/Kconfig
new file mode 100644
index 000000000..6c48770ac
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/Kconfig
@@ -0,0 +1,9 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_TEST_HA_KUNIT
+	depends on RV
+	# XXX: add dependencies if there
+	select HA_MON_EVENTS_ID
+	bool "test_ha_kunit monitor"
+	help
+	  auto-generated
diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.c b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.c
new file mode 100644
index 000000000..239b0539d
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.c
@@ -0,0 +1,243 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "test_ha_kunit"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <trace/events/sched.h>
+ */
+#include <rv_trace.h>
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#define RV_MON_TYPE RV_MON_PER_TASK
+/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */
+#define HA_TIMER_TYPE HA_TIMER_HRTIMER
+#include "test_ha_kunit.h"
+#include <rv/ha_monitor.h>
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ *
+ */
+#define BAR_NS(ha_mon) /* XXX: what is BAR_NS(ha_mon)? */
+
+#define FOO_NS /* XXX: what is FOO_NS? */
+
+static inline u64 bar_ns(struct ha_monitor *ha_mon)
+{
+	return /* XXX: what is bar_ns(ha_mon)? */;
+}
+
+static u64 foo_ns = /* XXX: default value */;
+module_param(foo_ns, ullong, 0644);
+
+/*
+ * These functions define how to read and reset the environment variable.
+ *
+ * Common environment variables like ns-based and jiffy-based clocks have
+ * pre-define getters and resetters you can use. The parser can infer the type
+ * of the environment variable if you supply a measure unit in the constraint.
+ * If you define your own functions, make sure to add appropriate memory
+ * barriers if required.
+ * Some environment variables don't require a storage as they read a system
+ * state (e.g. preemption count). Those variables are never reset, so we don't
+ * define a reset function on monitors only relying on this type of variables.
+ */
+static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs_test_ha_kunit env, u64 time_ns)
+{
+	if (env == clk_test_ha_kunit)
+		return ha_get_clk_ns(ha_mon, env, time_ns);
+	else if (env == env1_test_ha_kunit)
+		return /* XXX: how do I read env1? */
+	else if (env == env2_test_ha_kunit)
+		return /* XXX: how do I read env2? */
+	return ENV_INVALID_VALUE;
+}
+
+static void ha_reset_env(struct ha_monitor *ha_mon, enum envs_test_ha_kunit env, u64 time_ns)
+{
+	if (env == clk_test_ha_kunit)
+		ha_reset_clk_ns(ha_mon, env, time_ns);
+}
+
+/*
+ * These functions are used to validate state transitions.
+ *
+ * They are generated by parsing the model, there is usually no need to change them.
+ * If the monitor requires a timer, there are functions responsible to arm it when
+ * the next state has a constraint, cancel it in any other case and to check
+ * that it didn't expire before the callback run. Transitions to the same state
+ * without a reset never affect timers.
+ */
+static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
+					enum states curr_state, enum events event,
+					enum states next_state, u64 time_ns)
+{
+	if (curr_state == S0_test_ha_kunit)
+		return ha_check_invariant_ns(ha_mon, clk_test_ha_kunit, time_ns, bar_ns(ha_mon));
+	else if (curr_state == S2_test_ha_kunit)
+		return ha_check_invariant_ns(ha_mon, clk_test_ha_kunit, time_ns, BAR_NS(ha_mon));
+	return true;
+}
+
+static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
+				    enum states curr_state, enum events event,
+				    enum states next_state, u64 time_ns)
+{
+	bool res = true;
+
+	if (curr_state == S0_test_ha_kunit && event == event0_test_ha_kunit)
+		ha_reset_env(ha_mon, clk_test_ha_kunit, time_ns);
+	else if (curr_state == S0_test_ha_kunit && event == event1_test_ha_kunit)
+		ha_reset_env(ha_mon, clk_test_ha_kunit, time_ns);
+	else if (curr_state == S1_test_ha_kunit && event == event0_test_ha_kunit)
+		ha_reset_env(ha_mon, clk_test_ha_kunit, time_ns);
+	else if (curr_state == S1_test_ha_kunit && event == event2_test_ha_kunit) {
+		res = ha_get_env(ha_mon, env1_test_ha_kunit, time_ns) == 0ull;
+		ha_reset_env(ha_mon, clk_test_ha_kunit, time_ns);
+	} else if (curr_state == S2_test_ha_kunit && event == event1_test_ha_kunit)
+		res = ha_monitor_env_invalid(ha_mon, clk_test_ha_kunit) ||
+		      ha_get_env(ha_mon, clk_test_ha_kunit, time_ns) < foo_ns;
+	else if (curr_state == S3_test_ha_kunit && event == event0_test_ha_kunit)
+		res = ha_monitor_env_invalid(ha_mon, clk_test_ha_kunit) ||
+		      (ha_get_env(ha_mon, clk_test_ha_kunit, time_ns) < FOO_NS &&
+		      ha_get_env(ha_mon, env2_test_ha_kunit, time_ns) == 0ull);
+	else if (curr_state == S3_test_ha_kunit && event == event1_test_ha_kunit) {
+		res = ha_monitor_env_invalid(ha_mon, clk_test_ha_kunit) ||
+		      (ha_get_env(ha_mon, clk_test_ha_kunit, time_ns) < 5000ull &&
+		      ha_get_env(ha_mon, env1_test_ha_kunit, time_ns) == 1ull);
+		ha_reset_env(ha_mon, clk_test_ha_kunit, time_ns);
+	}
+	return res;
+}
+
+static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
+				       enum states curr_state, enum events event,
+				       enum states next_state, u64 time_ns)
+{
+	if (next_state == curr_state && event != event0_test_ha_kunit)
+		return;
+	if (next_state == S0_test_ha_kunit)
+		ha_start_timer_ns(ha_mon, clk_test_ha_kunit, bar_ns(ha_mon), time_ns);
+	else if (next_state == S2_test_ha_kunit)
+		ha_start_timer_ns(ha_mon, clk_test_ha_kunit, BAR_NS(ha_mon), time_ns);
+	else if (curr_state == S0_test_ha_kunit)
+		ha_cancel_timer(ha_mon);
+	else if (curr_state == S2_test_ha_kunit)
+		ha_cancel_timer(ha_mon);
+}
+
+static bool ha_verify_constraint(struct ha_monitor *ha_mon,
+				 enum states curr_state, enum events event,
+				 enum states next_state, u64 time_ns)
+{
+	if (!ha_verify_invariants(ha_mon, curr_state, event, next_state, time_ns))
+		return false;
+
+	if (!ha_verify_guards(ha_mon, curr_state, event, next_state, time_ns))
+		return false;
+
+	ha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns);
+
+	return true;
+}
+
+static void handle_event0(void *data, /* XXX: fill header */)
+{
+	/* XXX: validate that this event always leads to the initial state */
+	struct task_struct *p = /* XXX: how do I get p? */;
+	da_handle_start_event(p, event0_test_ha_kunit);
+}
+
+static void handle_event1(void *data, /* XXX: fill header */)
+{
+	struct task_struct *p = /* XXX: how do I get p? */;
+	da_handle_event(p, event1_test_ha_kunit);
+}
+
+static void handle_event2(void *data, /* XXX: fill header */)
+{
+	struct task_struct *p = /* XXX: how do I get p? */;
+	da_handle_event(p, event2_test_ha_kunit);
+}
+
+static int enable_test_ha_kunit(void)
+{
+	int retval;
+
+	retval = ha_monitor_init();
+	if (retval)
+		return retval;
+
+	rv_attach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event0);
+	rv_attach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event1);
+	rv_attach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event2);
+
+	return 0;
+}
+
+static void disable_test_ha_kunit(void)
+{
+	rv_this.enabled = 0;
+
+	rv_detach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event0);
+	rv_detach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event1);
+	rv_detach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event2);
+
+	ha_monitor_destroy();
+}
+
+/*
+ * This is the monitor register section.
+ */
+static struct rv_monitor rv_this = {
+	.name = "test_ha_kunit",
+	.description = "auto-generated",
+	.enable = enable_test_ha_kunit,
+	.disable = disable_test_ha_kunit,
+	.reset = da_monitor_reset_all,
+	.enabled = 0,
+};
+
+static int __init register_test_ha_kunit(void)
+{
+	return rv_register_monitor(&rv_this, NULL);
+}
+
+static void __exit unregister_test_ha_kunit(void)
+{
+	rv_unregister_monitor(&rv_this);
+}
+
+module_init(register_test_ha_kunit);
+module_exit(unregister_test_ha_kunit);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("rvgen: auto-generated");
+MODULE_DESCRIPTION("test_ha_kunit: auto-generated");
+
+#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
+#include <kunit/visibility.h>
+#include "test_ha_kunit_kunit.h"
+
+const struct rv_test_ha_kunit_ops rv_test_ha_kunit_ops = {
+	.mon = RV_MON_OPS_INIT(),
+	.handle_event0 = handle_event0,
+	.handle_event1 = handle_event1,
+	.handle_event2 = handle_event2,
+};
+EXPORT_SYMBOL_IF_KUNIT(rv_test_ha_kunit_ops);
+#endif
diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.h b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.h
new file mode 100644
index 000000000..5c428f818
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.h
@@ -0,0 +1,88 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Automatically generated C representation of test_ha_kunit automaton
+ * For further information about this format, see kernel documentation:
+ *   Documentation/trace/rv/deterministic_automata.rst
+ */
+
+#define MONITOR_NAME test_ha_kunit
+
+enum states_test_ha_kunit {
+	S0_test_ha_kunit,
+	S1_test_ha_kunit,
+	S2_test_ha_kunit,
+	S3_test_ha_kunit,
+	state_max_test_ha_kunit,
+};
+
+#define INVALID_STATE state_max_test_ha_kunit
+
+enum events_test_ha_kunit {
+	event0_test_ha_kunit,
+	event1_test_ha_kunit,
+	event2_test_ha_kunit,
+	event_max_test_ha_kunit,
+};
+
+enum envs_test_ha_kunit {
+	clk_test_ha_kunit,
+	env1_test_ha_kunit,
+	env2_test_ha_kunit,
+	env_max_test_ha_kunit,
+	env_max_stored_test_ha_kunit = env1_test_ha_kunit,
+};
+
+_Static_assert(env_max_stored_test_ha_kunit <= MAX_HA_ENV_LEN, "Not enough slots");
+#define HA_CLK_NS
+
+struct automaton_test_ha_kunit {
+	char *state_names[state_max_test_ha_kunit];
+	char *event_names[event_max_test_ha_kunit];
+	char *env_names[env_max_test_ha_kunit];
+	unsigned char function[state_max_test_ha_kunit][event_max_test_ha_kunit];
+	unsigned char initial_state;
+	bool final_states[state_max_test_ha_kunit];
+};
+
+static const struct automaton_test_ha_kunit automaton_test_ha_kunit = {
+	.state_names = {
+		"S0",
+		"S1",
+		"S2",
+		"S3",
+	},
+	.event_names = {
+		"event0",
+		"event1",
+		"event2",
+	},
+	.env_names = {
+		"clk",
+		"env1",
+		"env2",
+	},
+	.function = {
+		{
+			S0_test_ha_kunit,
+			S1_test_ha_kunit,
+			INVALID_STATE,
+		},
+		{
+			S0_test_ha_kunit,
+			INVALID_STATE,
+			S2_test_ha_kunit,
+		},
+		{
+			INVALID_STATE,
+			S2_test_ha_kunit,
+			S3_test_ha_kunit,
+		},
+		{
+			S0_test_ha_kunit,
+			S1_test_ha_kunit,
+			INVALID_STATE,
+		},
+	},
+	.initial_state = S0_test_ha_kunit,
+	.final_states = { 1, 0, 0, 0 },
+};
diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.c b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.c
new file mode 100644
index 000000000..6214a4aa6
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.c
@@ -0,0 +1,33 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/kernel.h>
+#include <linux/rv.h>
+#include <rv/kunit.h>
+/*
+ * XXX: include required headers, e.g.,
+ * #include <linux/sched.h>
+ */
+#include "test_ha_kunit_kunit.h"
+
+#if IS_REACHABLE(CONFIG_RV_MON_TEST_HA_KUNIT)
+
+static void rv_test_test_ha_kunit(struct kunit *test)
+{
+	struct rv_kunit_ctx *ctx = test->priv;
+	/*
+	 * If you need to create task_structs with rv_kunit_alloc_mock_task()
+	 * do it BEFORE preparing the test.
+	 */
+
+	prepare_test(test, &rv_test_ha_kunit_ops.mon);
+
+	/*
+	 * XXX: write the test here
+	 * e.g.
+	 * RV_KUNIT_EXPECT_REACTION_HERE(test, ctx)
+	 *	rv_test_ha_kunit_ops.handle_event(args);
+	 */
+}
+
+#else
+#define rv_test_test_ha_kunit rv_test_stub
+#endif
diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.h b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.h
new file mode 100644
index 000000000..0b2030cb6
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.h
@@ -0,0 +1,24 @@
+/* SPDX-License-Identifier: GPL-2.0-only */
+/*
+ * Automatically generated by rvgen kunit.
+ * May need manual intervention for function prototypes that couldn't be
+ * found (e.g. are in another file) or variables to be exported.
+ */
+
+#ifndef __TEST_HA_KUNIT_KUNIT_H
+#define __TEST_HA_KUNIT_KUNIT_H
+
+#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
+
+#include <linux/rv.h>
+#include <rv/kunit.h>
+
+extern const struct rv_test_ha_kunit_ops {
+	struct rv_kunit_mon mon;
+	void (*handle_event0)(void *data, /* XXX: fill header */);
+	void (*handle_event1)(void *data, /* XXX: fill header */);
+	void (*handle_event2)(void *data, /* XXX: fill header */);
+} rv_test_ha_kunit_ops;
+#endif
+
+#endif /* __TEST_HA_KUNIT_KUNIT_H */
diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_trace.h b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_trace.h
new file mode 100644
index 000000000..6c13ee006
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_trace.h
@@ -0,0 +1,19 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_TEST_HA_KUNIT
+DEFINE_EVENT(event_da_monitor_id, event_test_ha_kunit,
+	     TP_PROTO(int id, char *state, char *event, char *next_state, bool final_state),
+	     TP_ARGS(id, state, event, next_state, final_state));
+
+DEFINE_EVENT(error_da_monitor_id, error_test_ha_kunit,
+	     TP_PROTO(int id, char *state, char *event),
+	     TP_ARGS(id, state, event));
+
+DEFINE_EVENT(error_env_da_monitor_id, error_env_test_ha_kunit,
+	     TP_PROTO(int id, char *state, char *event, char *env),
+	     TP_ARGS(id, state, event, env));
+#endif /* CONFIG_RV_MON_TEST_HA_KUNIT */
diff --git a/tools/verification/rvgen/tests/golden/test_ltl/Kconfig b/tools/verification/rvgen/tests/golden/test_ltl/Kconfig
new file mode 100644
index 000000000..e2d0e721f
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_ltl/Kconfig
@@ -0,0 +1,11 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_TEST_LTL
+	depends on RV
+	# XXX: add dependencies if there
+	depends on RV_MON_LTL_PARENT
+	default y
+	select LTL_MON_EVENTS_ID
+	bool "test_ltl monitor"
+	help
+	  Simple description
diff --git a/tools/verification/rvgen/tests/golden/test_ltl/test_ltl.c b/tools/verification/rvgen/tests/golden/test_ltl/test_ltl.c
new file mode 100644
index 000000000..dd961c5dc
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_ltl/test_ltl.c
@@ -0,0 +1,108 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "test_ltl"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <trace/events/sched.h>
+ */
+#include <rv_trace.h>
+#include <monitors/ltl_parent/ltl_parent.h>
+
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#include "test_ltl.h"
+#include <rv/ltl_monitor.h>
+
+static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon)
+{
+	/*
+	 * This is called everytime the Buchi automaton is triggered.
+	 *
+	 * This function could be used to fetch the atomic propositions which
+	 * are expensive to trace. It is possible only if the atomic proposition
+	 * does not need to be updated at precise time.
+	 *
+	 * It is recommended to use tracepoints and ltl_atom_update() instead.
+	 */
+}
+
+static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)
+{
+	/*
+	 * This should initialize as many atomic propositions as possible.
+	 *
+	 * @task_creation indicates whether the task is being created. This is
+	 * false if the task is already running before the monitor is enabled.
+	 */
+	ltl_atom_set(mon, LTL_EVENT_A, true/false);
+	ltl_atom_set(mon, LTL_EVENT_B, true/false);
+}
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ */
+static void handle_example_event(void *data, /* XXX: fill header */)
+{
+	ltl_atom_update(task, LTL_EVENT_A, true/false);
+}
+
+static int enable_test_ltl(void)
+{
+	int retval;
+
+	retval = ltl_monitor_init();
+	if (retval)
+		return retval;
+
+	rv_attach_trace_probe("test_ltl", /* XXX: tracepoint */, handle_example_event);
+
+	return 0;
+}
+
+static void disable_test_ltl(void)
+{
+	rv_detach_trace_probe("test_ltl", /* XXX: tracepoint */, handle_example_event);
+
+	ltl_monitor_destroy();
+}
+
+/*
+ * This is the monitor register section.
+ */
+static struct rv_monitor rv_this = {
+	.name = "test_ltl",
+	.description = "Simple description",
+	.enable = enable_test_ltl,
+	.disable = disable_test_ltl,
+};
+
+static int __init register_test_ltl(void)
+{
+	return rv_register_monitor(&rv_this, &rv_ltl_parent);
+}
+
+static void __exit unregister_test_ltl(void)
+{
+	rv_unregister_monitor(&rv_this);
+}
+
+module_init(register_test_ltl);
+module_exit(unregister_test_ltl);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("rvgen: auto-generated");
+MODULE_DESCRIPTION("test_ltl: Simple description");
diff --git a/tools/verification/rvgen/tests/golden/test_ltl/test_ltl.h b/tools/verification/rvgen/tests/golden/test_ltl/test_ltl.h
new file mode 100644
index 000000000..7895f2e23
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_ltl/test_ltl.h
@@ -0,0 +1,108 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * C implementation of Buchi automaton, automatically generated by
+ * tools/verification/rvgen from the linear temporal logic specification.
+ * For further information, see kernel documentation:
+ *   Documentation/trace/rv/linear_temporal_logic.rst
+ */
+
+#include <linux/rv.h>
+
+#define MONITOR_NAME test_ltl
+
+enum ltl_atom {
+	LTL_EVENT_A,
+	LTL_EVENT_B,
+	LTL_NUM_ATOM
+};
+static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM);
+
+static const char *ltl_atom_str(enum ltl_atom atom)
+{
+	static const char *const names[] = {
+		"ev_a",
+		"ev_b",
+	};
+
+	return names[atom];
+}
+
+enum ltl_buchi_state {
+	S0,
+	S1,
+	S2,
+	S3,
+	S4,
+	RV_NUM_BA_STATES
+};
+static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);
+
+static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)
+{
+	bool event_b = test_bit(LTL_EVENT_B, mon->atoms);
+	bool event_a = test_bit(LTL_EVENT_A, mon->atoms);
+	bool val1 = !event_a;
+
+	if (val1)
+		__set_bit(S0, mon->states);
+	if (true)
+		__set_bit(S1, mon->states);
+	if (event_b)
+		__set_bit(S4, mon->states);
+}
+
+static void
+ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)
+{
+	bool event_b = test_bit(LTL_EVENT_B, mon->atoms);
+	bool event_a = test_bit(LTL_EVENT_A, mon->atoms);
+	bool val1 = !event_a;
+
+	switch (state) {
+	case S0:
+		if (val1)
+			__set_bit(S0, next);
+		if (true)
+			__set_bit(S1, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	case S1:
+		if (true)
+			__set_bit(S1, next);
+		if (true && val1)
+			__set_bit(S2, next);
+		if (event_b && val1)
+			__set_bit(S3, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	case S2:
+		if (true)
+			__set_bit(S1, next);
+		if (true && val1)
+			__set_bit(S2, next);
+		if (event_b && val1)
+			__set_bit(S3, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	case S3:
+		if (val1)
+			__set_bit(S0, next);
+		if (true)
+			__set_bit(S1, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	case S4:
+		if (val1)
+			__set_bit(S0, next);
+		if (true)
+			__set_bit(S1, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	}
+}
diff --git a/tools/verification/rvgen/tests/golden/test_ltl/test_ltl_trace.h b/tools/verification/rvgen/tests/golden/test_ltl/test_ltl_trace.h
new file mode 100644
index 000000000..3571b004c
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_ltl/test_ltl_trace.h
@@ -0,0 +1,14 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_TEST_LTL
+DEFINE_EVENT(event_ltl_monitor_id, event_test_ltl,
+	     TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next),
+	     TP_ARGS(task, states, atoms, next));
+DEFINE_EVENT(error_ltl_monitor_id, error_test_ltl,
+	     TP_PROTO(struct task_struct *task),
+	     TP_ARGS(task));
+#endif /* CONFIG_RV_MON_TEST_LTL */
diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/Kconfig b/tools/verification/rvgen/tests/golden/test_ltl_kunit/Kconfig
new file mode 100644
index 000000000..3e334c344
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_ltl_kunit/Kconfig
@@ -0,0 +1,9 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_TEST_LTL_KUNIT
+	depends on RV
+	# XXX: add dependencies if there
+	select LTL_MON_EVENTS_ID
+	bool "test_ltl_kunit monitor"
+	help
+	  auto-generated
diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.c b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.c
new file mode 100644
index 000000000..c1d58ce43
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.c
@@ -0,0 +1,107 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "test_ltl_kunit"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <trace/events/sched.h>
+ */
+#include <rv_trace.h>
+
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#include "test_ltl_kunit.h"
+#include <rv/ltl_monitor.h>
+
+static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon)
+{
+	/*
+	 * This is called everytime the Buchi automaton is triggered.
+	 *
+	 * This function could be used to fetch the atomic propositions which
+	 * are expensive to trace. It is possible only if the atomic proposition
+	 * does not need to be updated at precise time.
+	 *
+	 * It is recommended to use tracepoints and ltl_atom_update() instead.
+	 */
+}
+
+static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)
+{
+	/*
+	 * This should initialize as many atomic propositions as possible.
+	 *
+	 * @task_creation indicates whether the task is being created. This is
+	 * false if the task is already running before the monitor is enabled.
+	 */
+	ltl_atom_set(mon, LTL_EVENT_A, true/false);
+	ltl_atom_set(mon, LTL_EVENT_B, true/false);
+}
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ */
+static void handle_example_event(void *data, /* XXX: fill header */)
+{
+	ltl_atom_update(task, LTL_EVENT_A, true/false);
+}
+
+static int enable_test_ltl_kunit(void)
+{
+	int retval;
+
+	retval = ltl_monitor_init();
+	if (retval)
+		return retval;
+
+	rv_attach_trace_probe("test_ltl_kunit", /* XXX: tracepoint */, handle_example_event);
+
+	return 0;
+}
+
+static void disable_test_ltl_kunit(void)
+{
+	rv_detach_trace_probe("test_ltl_kunit", /* XXX: tracepoint */, handle_example_event);
+
+	ltl_monitor_destroy();
+}
+
+/*
+ * This is the monitor register section.
+ */
+static struct rv_monitor rv_this = {
+	.name = "test_ltl_kunit",
+	.description = "auto-generated",
+	.enable = enable_test_ltl_kunit,
+	.disable = disable_test_ltl_kunit,
+};
+
+static int __init register_test_ltl_kunit(void)
+{
+	return rv_register_monitor(&rv_this, NULL);
+}
+
+static void __exit unregister_test_ltl_kunit(void)
+{
+	rv_unregister_monitor(&rv_this);
+}
+
+module_init(register_test_ltl_kunit);
+module_exit(unregister_test_ltl_kunit);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("rvgen: auto-generated");
+MODULE_DESCRIPTION("test_ltl_kunit: auto-generated");
diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.h b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.h
new file mode 100644
index 000000000..acc503b56
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.h
@@ -0,0 +1,108 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * C implementation of Buchi automaton, automatically generated by
+ * tools/verification/rvgen from the linear temporal logic specification.
+ * For further information, see kernel documentation:
+ *   Documentation/trace/rv/linear_temporal_logic.rst
+ */
+
+#include <linux/rv.h>
+
+#define MONITOR_NAME test_ltl_kunit
+
+enum ltl_atom {
+	LTL_EVENT_A,
+	LTL_EVENT_B,
+	LTL_NUM_ATOM
+};
+static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM);
+
+static const char *ltl_atom_str(enum ltl_atom atom)
+{
+	static const char *const names[] = {
+		"ev_a",
+		"ev_b",
+	};
+
+	return names[atom];
+}
+
+enum ltl_buchi_state {
+	S0,
+	S1,
+	S2,
+	S3,
+	S4,
+	RV_NUM_BA_STATES
+};
+static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);
+
+static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)
+{
+	bool event_b = test_bit(LTL_EVENT_B, mon->atoms);
+	bool event_a = test_bit(LTL_EVENT_A, mon->atoms);
+	bool val1 = !event_a;
+
+	if (val1)
+		__set_bit(S0, mon->states);
+	if (true)
+		__set_bit(S1, mon->states);
+	if (event_b)
+		__set_bit(S4, mon->states);
+}
+
+static void
+ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)
+{
+	bool event_b = test_bit(LTL_EVENT_B, mon->atoms);
+	bool event_a = test_bit(LTL_EVENT_A, mon->atoms);
+	bool val1 = !event_a;
+
+	switch (state) {
+	case S0:
+		if (val1)
+			__set_bit(S0, next);
+		if (true)
+			__set_bit(S1, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	case S1:
+		if (true)
+			__set_bit(S1, next);
+		if (true && val1)
+			__set_bit(S2, next);
+		if (event_b && val1)
+			__set_bit(S3, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	case S2:
+		if (true)
+			__set_bit(S1, next);
+		if (true && val1)
+			__set_bit(S2, next);
+		if (event_b && val1)
+			__set_bit(S3, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	case S3:
+		if (val1)
+			__set_bit(S0, next);
+		if (true)
+			__set_bit(S1, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	case S4:
+		if (val1)
+			__set_bit(S0, next);
+		if (true)
+			__set_bit(S1, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	}
+}
diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.c b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.c
new file mode 100644
index 000000000..37dab5dfd
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.c
@@ -0,0 +1,33 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/kernel.h>
+#include <linux/rv.h>
+#include <rv/kunit.h>
+/*
+ * XXX: include required headers, e.g.,
+ * #include <linux/sched.h>
+ */
+#include "test_ltl_kunit_kunit.h"
+
+#if IS_REACHABLE(CONFIG_RV_MON_TEST_LTL_KUNIT)
+
+static void rv_test_test_ltl_kunit(struct kunit *test)
+{
+	struct rv_kunit_ctx *ctx = test->priv;
+	/*
+	 * If you need to create task_structs with rv_kunit_alloc_mock_task()
+	 * do it BEFORE preparing the test.
+	 */
+
+	prepare_test(test, &rv_test_ltl_kunit_ops.mon);
+
+	/*
+	 * XXX: write the test here
+	 * e.g.
+	 * RV_KUNIT_EXPECT_REACTION_HERE(test, ctx)
+	 *	rv_test_ltl_kunit_ops.handle_event(args);
+	 */
+}
+
+#else
+#define rv_test_test_ltl_kunit rv_test_stub
+#endif
diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.h b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.h
new file mode 100644
index 000000000..b2ca34be3
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.h
@@ -0,0 +1,22 @@
+/* SPDX-License-Identifier: GPL-2.0-only */
+/*
+ * Automatically generated by rvgen kunit.
+ * May need manual intervention for function prototypes that couldn't be
+ * found (e.g. are in another file) or variables to be exported.
+ */
+
+#ifndef __TEST_LTL_KUNIT_KUNIT_H
+#define __TEST_LTL_KUNIT_KUNIT_H
+
+#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
+
+#include <linux/rv.h>
+#include <rv/kunit.h>
+
+extern const struct rv_test_ltl_kunit_ops {
+	struct rv_kunit_mon mon;
+	void (*handle_example_event)(void *data, /* XXX: fill header */);
+} rv_test_ltl_kunit_ops;
+#endif
+
+#endif /* __TEST_LTL_KUNIT_KUNIT_H */
diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_trace.h b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_trace.h
new file mode 100644
index 000000000..a054d5b2c
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_trace.h
@@ -0,0 +1,14 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_TEST_LTL_KUNIT
+DEFINE_EVENT(event_ltl_monitor_id, event_test_ltl_kunit,
+	     TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next),
+	     TP_ARGS(task, states, atoms, next));
+DEFINE_EVENT(error_ltl_monitor_id, error_test_ltl_kunit,
+	     TP_PROTO(struct task_struct *task),
+	     TP_ARGS(task));
+#endif /* CONFIG_RV_MON_TEST_LTL_KUNIT */
diff --git a/tools/verification/rvgen/tests/rvgen_container.t b/tools/verification/rvgen/tests/rvgen_container.t
new file mode 100644
index 000000000..fa4fb3db8
--- /dev/null
+++ b/tools/verification/rvgen/tests/rvgen_container.t
@@ -0,0 +1,20 @@
+#!/bin/bash
+# SPDX-License-Identifier: GPL-2.0
+source ../tests/engine.sh
+test_begin
+
+set_timeout 30s
+
+# Help tests
+check "verify container subcommand help" \
+	"$RVGEN container -h" 0 "model_name" "class"
+
+check_and_compare_folder "container with description" \
+	"$RVGEN container -n test_container -D 'Test container for grouping monitors'" \
+	"test_container" "Writing the monitor into the directory test_container"
+
+# Error handling tests
+check "missing required model_name" \
+	"$RVGEN container" 2 "the following arguments are required: -n/--model_name"
+
+test_end
diff --git a/tools/verification/rvgen/tests/rvgen_kunit.t b/tools/verification/rvgen/tests/rvgen_kunit.t
new file mode 100644
index 000000000..d27d9175f
--- /dev/null
+++ b/tools/verification/rvgen/tests/rvgen_kunit.t
@@ -0,0 +1,41 @@
+#!/bin/bash
+# SPDX-License-Identifier: GPL-2.0
+source ../tests/engine.sh
+test_begin
+
+set_timeout 30s
+
+# Help tests
+check "verify kunit subcommand help" \
+	"$RVGEN kunit -h" 0 "model_name" "spec"
+
+check_and_compare_folder "KUnit generation with local lookup and test_da_kunit" \
+	"$RVGEN monitor -c da -s tests/specs/test_da.dot -t per_cpu -n test_da_kunit && $RVGEN kunit -a -l -n test_da_kunit" \
+	"test_da_kunit" "Now complete the test and add it to rv_monitors_test.c" "RV_MON_OPS_INIT"
+
+check_and_compare_folder "KUnit generation with local lookup and test_ha_kunit" \
+	"$RVGEN monitor -c ha -s tests/specs/test_ha.dot -t per_task -n test_ha_kunit && $RVGEN kunit -a -l -n test_ha_kunit" \
+	"test_ha_kunit" "Successfully created KUnit" "Append the following to"
+
+check_and_compare_folder "KUnit generation with local lookup and test_ltl_kunit" \
+	"$RVGEN monitor -c ltl -s tests/specs/test_ltl.ltl -t per_task -n test_ltl_kunit && $RVGEN kunit -l -n test_ltl_kunit" \
+	"test_ltl_kunit" "RV_MON_OPS_INIT"
+
+check_and_compare_folder "KUnit generation with backup file" \
+	"$RVGEN monitor -c ltl -s tests/specs/test_ltl.ltl -t per_task -n test_bak_kunit && echo DUMMY > test_bak_kunit/test_bak_kunit_kunit.c && $RVGEN kunit -l -n test_bak_kunit" \
+	"test_bak_kunit" "KUnit file(s) already exist.*backing up existing files"
+
+# Error handling tests
+check "missing required model_name" \
+	"$RVGEN kunit" 2 "the following arguments are required: -n/--model_name"
+
+check "non-existent model_name with auto_patch" \
+	"$RVGEN kunit -a -n nonexistent" 1 \
+	"Could not find monitor C file" "Traceback (most recent call last)"
+
+check "monitor without handlers" \
+	"mkdir -p nohandler ; echo DUMMY > nohandler/nohandler.c ; $RVGEN kunit -l -n nohandler" 1 \
+	"No handlers found" "Traceback (most recent call last)"
+rm -rf nohandler
+
+test_end
diff --git a/tools/verification/rvgen/tests/rvgen_monitor.t b/tools/verification/rvgen/tests/rvgen_monitor.t
new file mode 100644
index 000000000..5f2562600
--- /dev/null
+++ b/tools/verification/rvgen/tests/rvgen_monitor.t
@@ -0,0 +1,87 @@
+#!/bin/bash
+# SPDX-License-Identifier: GPL-2.0
+source ../tests/engine.sh
+test_begin
+
+set_timeout 30s
+
+# Help and basic tests
+check "verify help page" \
+	"$RVGEN --help" 0 "Generate kernel rv monitor"
+
+check "verify monitor subcommand help" \
+	"$RVGEN monitor --help" 0 "Monitor class"
+
+# DA monitor tests - test all monitor types
+check_and_compare_folder "DA per_cpu (default name)" \
+	"$RVGEN monitor -c da -s tests/specs/test_da.dot -t per_cpu" \
+	"test_da" "obj-\$(CONFIG_RV_MON_TEST_DA) += monitors/test_da/test_da.o"
+
+check_and_compare_folder "DA global type" \
+	"$RVGEN monitor -c da -s tests/specs/test_da.dot -t global -n da_global" \
+	"da_global" "DA_MON_EVENTS_IMPLICIT"
+
+check_and_compare_folder "DA per_task with description" \
+	"$RVGEN monitor -c da -s tests/specs/test_da2.dot -t per_task -n da_pertask_desc -D 'Custom description for testing'" \
+	"da_pertask_desc" "#include <monitors/da_pertask_desc/da_pertask_desc_trace.h>"
+
+check_and_compare_folder "DA per_obj with parent" \
+	"$RVGEN monitor -c da -s tests/specs/test_da2.dot -t per_obj -n da_perobj_parent -p parent_mon" \
+	"da_perobj_parent" "DA_MON_EVENTS_ID"
+
+# HA monitor tests
+check_and_compare_folder "HA per_task (default name)" \
+	"$RVGEN monitor -c ha -s tests/specs/test_ha.dot -t per_task" \
+	"test_ha" "HA_MON_EVENTS_ID"
+
+check_and_compare_folder "HA per_cpu type" \
+	"$RVGEN monitor -c ha -s tests/specs/test_ha.dot -t per_cpu -n ha_percpu" \
+	"ha_percpu" "HA_MON_EVENTS_IMPLICIT"
+
+# LTL monitor test
+check_and_compare_folder "LTL per_task" \
+	"$RVGEN monitor -c ltl -s tests/specs/test_ltl.ltl -t per_task -n ltl_pertask" \
+	"ltl_pertask" "source \"kernel/trace/rv/monitors/ltl_pertask/Kconfig\""
+
+check_and_compare_folder "LTL per_task with parent and description (default name)" \
+	"$RVGEN monitor -c ltl -s tests/specs/test_ltl.ltl -t per_task -p ltl_parent -D 'Simple description'" \
+	"test_ltl" "LTL_MON_EVENTS_ID"
+
+# Error handling tests
+check "missing required spec argument" \
+	"$RVGEN monitor -c da -t per_cpu" 2 \
+	"the following arguments are required: -s/--spec" "Traceback (most recent call last)"
+
+check "missing required monitor type" \
+	"$RVGEN monitor -c da -s tests/specs/test_da.dot" 2 \
+	"the following arguments are required: -t/--monitor_type" "Traceback (most recent call last)"
+
+check "missing required monitor class" \
+	"$RVGEN monitor -s tests/specs/test_da.dot -t per_cpu" 2 \
+	"the following arguments are required: -c/--class" "Traceback (most recent call last)"
+
+check "invalid monitor class" \
+	"$RVGEN monitor -c invalid -s tests/specs/test_da.dot -t per_cpu" 1 \
+	"Unknown monitor class" "Traceback (most recent call last)"
+
+check "missing dot file" \
+	"$RVGEN monitor -c da -s tests/specs/nonexistent.dot -t per_cpu" 1 \
+	"No such file or directory" "Traceback (most recent call last)"
+
+check "missing ltl file" \
+	"$RVGEN monitor -c ltl -s tests/specs/nonexistent.ltl -t per_task" 1 \
+	"No such file or directory" "Traceback (most recent call last)"
+
+check "invalid dot file syntax" \
+	"$RVGEN monitor -c da -s tests/specs/test_invalid.dot -t per_cpu" 1 \
+	"The automaton doesn't have an initial state" "Traceback (most recent call last)"
+
+check "invalid ha file syntax" \
+	"$RVGEN monitor -c ha -s tests/specs/test_invalid_ha.dot -t per_obj" 1 \
+	"Unrecognised event" "Traceback (most recent call last)"
+
+check "invalid ltl file syntax" \
+	"$RVGEN monitor -c ltl -s tests/specs/test_invalid.ltl -t per_task" 1 \
+	"No terminal matches 'i'" "Traceback (most recent call last)"
+
+test_end
diff --git a/tools/verification/rvgen/tests/specs/test_da.dot b/tools/verification/rvgen/tests/specs/test_da.dot
new file mode 100644
index 000000000..e555c239b
--- /dev/null
+++ b/tools/verification/rvgen/tests/specs/test_da.dot
@@ -0,0 +1,16 @@
+digraph state_automaton {
+	{node [shape = circle] "state_b"};
+	{node [shape = plaintext, style=invis, label=""] "__init_state_a"};
+	{node [shape = doublecircle] "state_a"};
+	{node [shape = circle] "state_a"};
+	"__init_state_a" -> "state_a";
+	"state_a" [label = "state_a"];
+	"state_a" -> "state_a" [ label = "event_2" ];
+	"state_a" -> "state_b" [ label = "event_1" ];
+	"state_b" [label = "state_b"];
+	"state_b" -> "state_a" [ label = "event_2" ];
+	{ rank = min ;
+		"__init_state_a";
+		"state_a";
+	}
+}
diff --git a/tools/verification/rvgen/tests/specs/test_da2.dot b/tools/verification/rvgen/tests/specs/test_da2.dot
new file mode 100644
index 000000000..cdd4192f5
--- /dev/null
+++ b/tools/verification/rvgen/tests/specs/test_da2.dot
@@ -0,0 +1,19 @@
+digraph state_automaton {
+	{node [shape = circle] "state_b"};
+	{node [shape = circle] "state_c"};
+	{node [shape = plaintext, style=invis, label=""] "__init_state_a"};
+	{node [shape = doublecircle] "state_a"};
+	{node [shape = circle] "state_a"};
+	"__init_state_a" -> "state_a";
+	"state_a" [label = "state_a"];
+	"state_a" -> "state_b" [ label = "event_1" ];
+	"state_a" -> "state_c" [ label = "event_2" ];
+	"state_b" [label = "state_b"];
+	"state_b" -> "state_a" [ label = "event_2" ];
+	"state_b" -> "state_c" [ label = "event_3" ];
+	"state_c" [label = "state_c"];
+	{ rank = min ;
+		"__init_state_a";
+		"state_a";
+	}
+}
diff --git a/tools/verification/rvgen/tests/specs/test_ha.dot b/tools/verification/rvgen/tests/specs/test_ha.dot
new file mode 100644
index 000000000..af18ad738
--- /dev/null
+++ b/tools/verification/rvgen/tests/specs/test_ha.dot
@@ -0,0 +1,27 @@
+digraph state_automaton {
+	center = true;
+	size = "7,11";
+	{node [shape = circle] "S1"};
+	{node [shape = plaintext, style=invis, label=""] "__init_S0"};
+	{node [shape = doublecircle] "S0"};
+	{node [shape = circle] "S0"};
+	{node [shape = circle] "S2"};
+	{node [shape = circle] "S3"};
+	"__init_S0" -> "S0";
+	"S0" [label = "S0\nclk < bar_ns()", color = green3];
+	"S1" [label = "S1"];
+	"S2" [label = "S2\nclk < BAR_NS()"];
+	"S3" [label = "S3"];
+	"S1" -> "S0" [ label = "event0;reset(clk)" ];
+	"S0" -> "S1" [ label = "event1;reset(clk)" ];
+	"S0" -> "S0" [ label = "event0;reset(clk)" ];
+	"S1" -> "S2" [ label = "event2;env1 == 0;reset(clk)" ];
+	"S2" -> "S3" [ label = "event2" ];
+	"S2" -> "S2" [ label = "event1;clk < foo_ns" ];
+	"S3" -> "S0" [ label = "event0;clk < FOO_NS && env2 == 0" ];
+	"S3" -> "S1" [ label = "event1;clk < 5us && env1 == 1;reset(clk)" ];
+	{ rank = min ;
+		"__init_S0";
+		"S0";
+	}
+}
diff --git a/tools/verification/rvgen/tests/specs/test_invalid.dot b/tools/verification/rvgen/tests/specs/test_invalid.dot
new file mode 100644
index 000000000..17c63fc57
--- /dev/null
+++ b/tools/verification/rvgen/tests/specs/test_invalid.dot
@@ -0,0 +1,8 @@
+digraph invalid {
+	{node [shape = circle] "init"};
+	{node [shape = circle] "state1"};
+	"init" [label = "init"];
+	"init" -> "state1" [ label = "event_a" ];
+	"state1" [label = "state1"];
+	"state1" -> "init" [ label = "event_b" ];
+}
diff --git a/tools/verification/rvgen/tests/specs/test_invalid.ltl b/tools/verification/rvgen/tests/specs/test_invalid.ltl
new file mode 100644
index 000000000..cf36307e0
--- /dev/null
+++ b/tools/verification/rvgen/tests/specs/test_invalid.ltl
@@ -0,0 +1 @@
+RULE = A invalid B
diff --git a/tools/verification/rvgen/tests/specs/test_invalid_ha.dot b/tools/verification/rvgen/tests/specs/test_invalid_ha.dot
new file mode 100644
index 000000000..06de6aa87
--- /dev/null
+++ b/tools/verification/rvgen/tests/specs/test_invalid_ha.dot
@@ -0,0 +1,16 @@
+digraph state_automaton {
+	{node [shape = circle] "state_b"};
+	{node [shape = plaintext, style=invis, label=""] "__init_state_a"};
+	{node [shape = doublecircle] "state_a"};
+	{node [shape = circle] "state_a"};
+	"__init_state_a" -> "state_a";
+	"state_a" [label = "state_a;clk < 1"];
+	"state_a" -> "state_a" [ label = "event_2;reset(clk)" ];
+	"state_a" -> "state_b" [ label = "event_1;wrong_constraint" ];
+	"state_b" [label = "state_b"];
+	"state_b" -> "state_a" [ label = "event_2" ];
+	{ rank = min ;
+		"__init_state_a";
+		"state_a";
+	}
+}
diff --git a/tools/verification/rvgen/tests/specs/test_ltl.ltl b/tools/verification/rvgen/tests/specs/test_ltl.ltl
new file mode 100644
index 000000000..5ed658abd
--- /dev/null
+++ b/tools/verification/rvgen/tests/specs/test_ltl.ltl
@@ -0,0 +1 @@
+RULE = always (EVENT_A imply eventually EVENT_B)