Merge tag 'trace-rv-v7.3' of git://git.kernel.org/pub/scm/linux/kernel/git/trace/linux-trace

Pull Real-time Verifier updates from Steven Rostedt:

 - Switch LTL and DOT parsers to Lark in code generation tool

   The rvgen code generation tool originally parsed DOT files and LTL
   specifications using custom string parsing and Ply, which is no
   longer maintained. The DOT parser was fragile and prone to failure on
   minor format variations. Both LTL and DOT parsers have been rewritten
   to use the Lark parsing library.

 - Simplify Hybrid Automata clock variables

   The clock variables in hybrid automata monitors now use a single
   representation of the elapsed time since the clock was reset, rather
   than converting between invariant and guard representations. This
   allows simpler code generation for the newly refactored parser.

 - Generate cleanup hook for per-obj monitor

   The code generation scripts now adds a cleanup function to per-obj
   monitors for the user to wire to the appropriate event (e.g.
   sched_process_exit for tasks).

 - Reduce read_lock scope during per-task cleanup

   Take the tasklist_lock only when necessary, that is when iterating
   over for_each_process_thread().

 - Simplify task monitor slot management

   Only rely on the slot array for per-task slot management to avoid
   inconsistency with the unused counter.

 - Improve rvgen code robustness and templates

   Use pathlib in rvgen and improve kernel path discovery. Also improve
   consistency across templates when generating code (e.g. author
   placeholder and monitor struct name).

 - Update rtapp sleep monitor

   Simplify the sleep monitor by excluding kernel threads and updating
   the nanosleep check to focus only on CLOCK_REALTIME. Also switch to
   use the sched_exit tracepoint to run in the context of the offending
   (wakee) task.

 - Add wakeup monitor

   Add the new rtapp/wakeup monitor to detect when lower-priority tasks
   wake up higher-priority ones, complementing the existing sleep
   monitor by running in the waker context and capturing its stack
   trace.

 - Fix tools/rv exit status on failure

   Ensure the rv tool returns a failure exit code when a monitor fails
   to start because it was already running.

 - Add automated selftests for tools/rv and rvgen

   Introduced automated bash selftests to validate rv monitor listing
   and execution under different configurations. Added tests for the
   rvgen code generator, validating generated files against expected
   output (golden). Tests are reachable via make check.

 - Add KUnit test coverage for verification monitors

   Added comprehensive KUnit tests to validate the functionality of
   deterministic, hybrid, and LTL monitors by emulating event sequences
   and timing in a mock environment without affecting the running kernel
   while expecting mock reactions to fire. Ensure real RV monitors
   cannot run during KUnit tests to avoid state corruption.

 - Mock current in rv monitors

   Mock the call to current in rv monitors when the KUnit tests are
   built to allow them to run the test on dummy tasks. No overhead is
   expected when KUnit tests aren't running.

 - Introduce rvgen kunit subcommand

   Added a new 'kunit' subcommand to rvgen to automatically patch an
   already generated monitor with KUnit integration templates by parsing
   its event handlers and creating the required mock structures and
   initializations.

 - Refine kernel verification selftests

   Added new selftests for the deadline and stall monitors and
   rearranged the existing wwnr_printk test to resolve flakiness.
   Additionally, fixed an issue in the selftests framework where
   negative assertion failures were not correctly propagated due to
   shell rules.

 - Fix 32-bit build of nomiss KUnit test

   A previous commit introduced a division between an u64 and a constant
   value and that doesn't build on 32-bit systems. Use div_u64()
   instead.

 - Document changes in sleep monitor

   The sleep monitor introduced some changes in the past like allowing
   epoll_wait() as a valid sleep and a task going to runnable before
   scheduling as a valid wakeup. Document both.

* tag 'trace-rv-v7.3' of git://git.kernel.org/pub/scm/linux/kernel/git/trace/linux-trace: (40 commits)
  Documentation/rv: Explain epoll and aborted sleeps
  rv: Fix 32-bit build of nomiss KUnit test
  selftests/verification: Add selftests for deadline and stall monitors
  selftests/verification: Rearrange the wwnr_printk test
  selftests/verification: Fix wrong errexit assumption
  rv: Add KUnit tests for some LTL monitors
  rv: Add KUnit mock for current
  rv: Add KUnit tests for some DA/HA monitors
  rv: Export task monitor slot and react symbols
  verification/rvgen: Add selftests for rvgen kunit
  verification/rvgen: Add the rvgen kunit subcommand
  verification/rvgen: Add selftests
  verification/rvgen: Add golden and spec folders for tests
  tools/rv: Add selftests
  verification/rvgen: Improve consistency in template files
  verification/rvgen: Use pathlib instead of os.path
  verification/rvgen: Improve rv_dir discovery in RVGenerator
  tools/rv: Fix exit status when monitor execution fails
  rv: Use generic rv_this for the rv_monitor variable in LTL
  rv/rtapp: Add wakeup monitor
  ...

95 files changed, 4688 insertions, 618 deletions

diff --git a/tools/testing/selftests/verification/test.d/rv_deadline.tc b/tools/testing/selftests/verification/test.d/rv_deadline.tc
new file mode 100644
index 000000000000..fc95267dbb82
--- /dev/null
+++ b/tools/testing/selftests/verification/test.d/rv_deadline.tc
@@ -0,0 +1,23 @@
+#!/bin/sh
+# SPDX-License-Identifier: GPL-2.0-or-later
+# description: Test deadline monitors trigger no reaction
+# requires: available_reactors deadline:monitor printk:reactor stress-ng:program
+
+load() { # returns true if there was a reaction
+	local lines_before
+	lines_before=$(dmesg | wc -l)
+	stress-ng --cpu 2 --sched deadline --sched-period 100000000 \
+		--sched-deadline 100000000 --sched-runtime 20000000 -t 5 &
+	stress-ng --cpu 2 --sched rr --sched-prio 50 --cyclic 1 \
+		--cyclic-policy rr --cyclic-prio 50 -t 5 &
+	wait
+	dmesg | tail -n +$((lines_before + 1)) | grep -q "rv: monitor [a-z]\+ does not allow event"
+}
+
+echo 1 > monitors/deadline/enable
+echo printk > monitors/deadline/reactors
+
+! load || false
+
+echo nop > monitors/deadline/reactors
+echo 0 > monitors/deadline/enable
diff --git a/tools/testing/selftests/verification/test.d/rv_monitor_enable_disable.tc b/tools/testing/selftests/verification/test.d/rv_monitor_enable_disable.tc
index f29236defb5a..61e2c8b54d9a 100644
--- a/tools/testing/selftests/verification/test.d/rv_monitor_enable_disable.tc
+++ b/tools/testing/selftests/verification/test.d/rv_monitor_enable_disable.tc
@@ -10,7 +10,7 @@ test_simple_monitor() {
     grep -q "$monitor$" enabled_monitors
 
     echo 0 > "monitors/$prefix$monitor/enable"
-    ! grep -q "$monitor$" enabled_monitors
+    ! grep -q "$monitor$" enabled_monitors || false
 
     echo "$monitor" >> enabled_monitors
     grep -q 1 "monitors/$prefix$monitor/enable"
@@ -34,12 +34,12 @@ test_container_monitor() {
 	test -n "$nested"
 
     echo 0 > "monitors/$monitor/enable"
-    ! grep -q "^$monitor$" enabled_monitors
+    ! grep -q "^$monitor$" enabled_monitors || false
 
     for nested_dir in "monitors/$monitor"/*; do
         [ -d "$nested_dir" ] || continue
         nested=$(basename "$nested_dir")
-        ! grep -q "^$monitor:$nested$" enabled_monitors
+        ! grep -q "^$monitor:$nested$" enabled_monitors || false
     done
 
     echo "$monitor" >> enabled_monitors
@@ -71,5 +71,5 @@ for monitor_dir in monitors/*; do
     fi
 done
 
-! echo non_existent_monitor > enabled_monitors
-! grep -q "^non_existent_monitor$" enabled_monitors
+! echo non_existent_monitor > enabled_monitors || false
+! grep -q "^non_existent_monitor$" enabled_monitors || false
diff --git a/tools/testing/selftests/verification/test.d/rv_monitor_reactor.tc b/tools/testing/selftests/verification/test.d/rv_monitor_reactor.tc
index 2958bf849338..516a20971390 100644
--- a/tools/testing/selftests/verification/test.d/rv_monitor_reactor.tc
+++ b/tools/testing/selftests/verification/test.d/rv_monitor_reactor.tc
@@ -64,5 +64,5 @@ done
 
 monitor=$(ls /sys/kernel/tracing/rv/monitors -1 | head -n 1)
 test -f "monitors/$monitor/reactors"
-! echo non_existent_reactor > "monitors/$monitor/reactors"
-! grep -q "\\[non_existent_reactor\\]" "monitors/$monitor/reactors"
+! echo non_existent_reactor > "monitors/$monitor/reactors" || false
+! grep -q "\\[non_existent_reactor\\]" "monitors/$monitor/reactors" || false
diff --git a/tools/testing/selftests/verification/test.d/rv_stall.tc b/tools/testing/selftests/verification/test.d/rv_stall.tc
new file mode 100644
index 000000000000..515a10263ca1
--- /dev/null
+++ b/tools/testing/selftests/verification/test.d/rv_stall.tc
@@ -0,0 +1,33 @@
+#!/bin/sh
+# SPDX-License-Identifier: GPL-2.0-or-later
+# description: Test stall monitor
+# requires: available_reactors stall:monitor printk:reactor stress-ng:program
+
+THRESHOLD=/sys/module/stall/parameters/threshold_jiffies
+ORIG_THRESHOLD=$(cat $THRESHOLD)
+trap 'echo $ORIG_THRESHOLD > $THRESHOLD' EXIT
+
+load() { # returns true if there was a reaction
+	local lines_before cpu
+	cpu=$(($(nproc) - 1))
+	lines_before=$(dmesg | wc -l)
+	stress-ng --cpu 1 --taskset "$cpu" --sched rr --sched-prio 1 -t 3 &
+	stress-ng --cpu 5 --taskset "$cpu" -t 3 &
+	wait
+	dmesg | tail -n +$((lines_before + 1)) | grep -q "rv: monitor stall does not allow event"
+}
+
+echo 5000 > $THRESHOLD
+echo 1 > monitors/stall/enable
+echo printk > monitors/stall/reactors
+
+! load || false
+
+echo 0 > monitors/stall/enable
+echo 70 > $THRESHOLD
+echo 1 > monitors/stall/enable
+
+load
+
+echo nop > monitors/stall/reactors
+echo 0 > monitors/stall/enable
diff --git a/tools/testing/selftests/verification/test.d/rv_wwnr_printk.tc b/tools/testing/selftests/verification/test.d/rv_wwnr_printk.tc
index 5a59432b1d93..17e1edfb3902 100644
--- a/tools/testing/selftests/verification/test.d/rv_wwnr_printk.tc
+++ b/tools/testing/selftests/verification/test.d/rv_wwnr_printk.tc
@@ -4,11 +4,29 @@
 # requires: available_reactors wwnr:monitor printk:reactor stress-ng:program
 
 load() { # returns true if there was a reaction
-	local lines_before num
+	local lines_before num load_pid ret
 	num=$((($(nproc) + 1) / 2))
 	lines_before=$(dmesg | wc -l)
-	stress-ng --cpu-sched "$num" --timer "$num" -t 5 -q
-	dmesg | tail -n $((lines_before + 1)) | grep -q "rv: monitor wwnr does not allow event"
+	stress-ng --cpu-sched "$num" --timer "$num" -t 5 -q &
+	load_pid=$!
+	timeout 5 dmesg -w | tail -n +$((lines_before + 1)) | \
+		grep -m 1 -q "rv: monitor wwnr does not allow event"
+	ret=$?
+	kill "$load_pid" || true
+	wait "$load_pid" || true
+	return $ret
+}
+
+# loads may flood the ringbuffer, wait for all pending printks (timeout at 2 minutes)
+wait_dmesg_flush() {
+	local last_before last_after
+	for _ in $(seq 400); do
+		last_before=$last_after
+		last_after=$(dmesg | grep "rv:" | tail -n 1 || true)
+		[ "$last_before" = "$last_after" ] && return 0
+		sleep .3
+	done
+	return 1
 }
 
 echo 1 > monitors/wwnr/enable
@@ -17,13 +35,17 @@ echo printk > monitors/wwnr/reactors
 load
 
 echo 0 > monitoring_on
-! load
+wait_dmesg_flush
+
+! load || false
 echo 1 > monitoring_on
 
 load
 
 echo 0 > reacting_on
-! load
+wait_dmesg_flush
+
+! load || false
 echo 1 > reacting_on
 
 echo nop > monitors/wwnr/reactors
diff --git a/tools/verification/models/rtapp/sleep.ltl b/tools/verification/models/rtapp/sleep.ltl
index 6f26c4810f78..4d78fdd204c0 100644
--- a/tools/verification/models/rtapp/sleep.ltl
+++ b/tools/verification/models/rtapp/sleep.ltl
@@ -1,7 +1,7 @@
-RULE = always ((RT and SLEEP) imply (RT_FRIENDLY_SLEEP or ALLOWLIST))
+RULE = always ((RT and SLEEP and USER_THREAD) imply (RT_FRIENDLY_SLEEP or ALLOWLIST))
 
-RT_FRIENDLY_SLEEP = (RT_VALID_SLEEP_REASON or KERNEL_THREAD)
-                and ((not WAKE) until RT_FRIENDLY_WAKE)
+RT_FRIENDLY_SLEEP = RT_VALID_SLEEP_REASON
+                and ((not SCHEDULE_IN) until RT_FRIENDLY_WAKE)
 
 RT_VALID_SLEEP_REASON = FUTEX_WAIT
                      or RT_FRIENDLY_NANOSLEEP
@@ -9,15 +9,12 @@ RT_VALID_SLEEP_REASON = FUTEX_WAIT
 
 RT_FRIENDLY_NANOSLEEP = CLOCK_NANOSLEEP
                     and NANOSLEEP_TIMER_ABSTIME
-                    and (NANOSLEEP_CLOCK_MONOTONIC or NANOSLEEP_CLOCK_TAI)
+                    and not NANOSLEEP_CLOCK_REALTIME
 
 RT_FRIENDLY_WAKE = WOKEN_BY_EQUAL_OR_HIGHER_PRIO
                 or WOKEN_BY_HARDIRQ
                 or WOKEN_BY_NMI
                 or ABORT_SLEEP
-                or KTHREAD_SHOULD_STOP
 
 ALLOWLIST = BLOCK_ON_RT_MUTEX
          or FUTEX_LOCK_PI
-         or TASK_IS_RCU
-         or TASK_IS_MIGRATION
diff --git a/tools/verification/models/rtapp/wakeup.ltl b/tools/verification/models/rtapp/wakeup.ltl
new file mode 100644
index 000000000000..a5d63ca0811a
--- /dev/null
+++ b/tools/verification/models/rtapp/wakeup.ltl
@@ -0,0 +1,5 @@
+RULE = always (((RT and USER_THREAD) imply
+		(not (WOKEN_BY_LOWER_PRIO or WOKEN_BY_SOFTIRQ)) or ALLOWLIST))
+
+ALLOWLIST = BLOCK_ON_RT_MUTEX
+         or FUTEX_LOCK_PI
diff --git a/tools/verification/rv/Makefile b/tools/verification/rv/Makefile
index 5b898360ba48..8ae5fc0d1d17 100644
--- a/tools/verification/rv/Makefile
+++ b/tools/verification/rv/Makefile
@@ -78,4 +78,7 @@ clean: doc_clean fixdep-clean
 	$(Q)rm -f rv rv-static fixdep FEATURE-DUMP rv-*
 	$(Q)rm -rf feature
 
-.PHONY: FORCE clean
+check: $(RV)
+	RV=$(RV) prove -o --directives -f tests/
+
+.PHONY: FORCE clean check
diff --git a/tools/verification/rv/src/rv.c b/tools/verification/rv/src/rv.c
index b8fe24a87d97..09e0d8598619 100644
--- a/tools/verification/rv/src/rv.c
+++ b/tools/verification/rv/src/rv.c
@@ -50,23 +50,23 @@ static void rv_list(int argc, char **argv)
 		"	[container]: list only monitors in this container",
 		NULL,
 	};
-	int i, print_help = 0, retval = 0;
+	int i, print_help = 0, retval = EXIT_SUCCESS;
 	char *container = NULL;
 
 	if (argc == 2) {
 		if (!strcmp(argv[1], "-h") || !strcmp(argv[1], "--help")) {
 			print_help = 1;
-			retval = 0;
+			retval = EXIT_SUCCESS;
 		} else if (argv[1][0] == '-') {
 			/* assume invalid option */
 			print_help = 1;
-			retval = 1;
+			retval = EXIT_FAILURE;
 		} else
 			container = argv[1];
 	} else if (argc > 2) {
 		/* more than 2 is always usage */
 		print_help = 1;
-		retval = 1;
+		retval = EXIT_FAILURE;
 	}
 	if (print_help) {
 		fprintf(stderr, "rv version %s\n", VERSION);
@@ -77,7 +77,7 @@ static void rv_list(int argc, char **argv)
 
 	ikm_list_monitors(container);
 
-	exit(0);
+	exit(EXIT_SUCCESS);
 }
 
 /*
@@ -108,14 +108,14 @@ static void rv_mon(int argc, char **argv)
 
 		for (i = 0; usage[i]; i++)
 			fprintf(stderr, "%s\n", usage[i]);
-		exit(1);
+		exit(EXIT_FAILURE);
 	} else if (!strcmp(argv[1], "-h") || !strcmp(argv[1], "--help")) {
 
 		fprintf(stderr, "rv version %s\n", VERSION);
 
 		for (i = 0; usage[i]; i++)
 			fprintf(stderr, "%s\n", usage[i]);
-		exit(0);
+		exit(EXIT_SUCCESS);
 	}
 
 	monitor_name = argv[1];
@@ -127,7 +127,7 @@ static void rv_mon(int argc, char **argv)
 
 	if (!run)
 		err_msg("rv: monitor %s does not exist\n", monitor_name);
-	exit(!run);
+	exit(run > 0 ? EXIT_SUCCESS : EXIT_FAILURE);
 }
 
 static void usage(int exit_val, const char *fmt, ...)
@@ -174,13 +174,13 @@ static void usage(int exit_val, const char *fmt, ...)
 int main(int argc, char **argv)
 {
 	if (geteuid())
-		usage(1, "%s needs root permission", argv[0]);
+		usage(EXIT_FAILURE, "%s needs root permission", argv[0]);
 
 	if (argc <= 1)
-		usage(1, "%s requires a command", argv[0]);
+		usage(EXIT_FAILURE, "%s requires a command", argv[0]);
 
 	if (!strcmp(argv[1], "-h") || !strcmp(argv[1], "--help"))
-		usage(0, "help");
+		usage(EXIT_SUCCESS, "help");
 
 	if (!strcmp(argv[1], "list"))
 		rv_list(--argc, &argv[1]);
@@ -197,5 +197,5 @@ int main(int argc, char **argv)
 	}
 
 	/* invalid sub-command */
-	usage(1, "%s does not know the %s command, old version?", argv[0], argv[1]);
+	usage(EXIT_FAILURE, "%s does not know the %s command, old version?", argv[0], argv[1]);
 }
diff --git a/tools/verification/rv/tests/rv_list.t b/tools/verification/rv/tests/rv_list.t
new file mode 100644
index 000000000000..201af33a52cc
--- /dev/null
+++ b/tools/verification/rv/tests/rv_list.t
@@ -0,0 +1,48 @@
+#!/bin/bash
+# SPDX-License-Identifier: GPL-2.0
+source ../tests/engine.sh
+test_begin
+
+set_timeout 30s
+
+RVDIR=/sys/kernel/tracing/rv/
+
+# Help and basic tests
+check "verify help page" \
+	"$RV --help" 0 "usage: rv command"
+
+check "verify list subcommand help" \
+	"$RV list --help" 0 "list all available monitors"
+
+all_nested=$(grep : $RVDIR/available_monitors | cut -d: -f2 | paste -s | sed 's/\t/\\|/g')
+all_non_nested=$(grep -v : $RVDIR/available_monitors | cut -d: -f2 | paste -s | sed 's/\t/\\|/g')
+sched_monitors=$(grep sched: $RVDIR/available_monitors | cut -d: -f2 | paste -s | sed 's/\t/\\|/g')
+description_state="[[:space:]]\+[[:print:]]\+\[\(OFF\|ON\)\]"
+line_nested=" - \($all_nested\)${description_state}"
+line_non_nested="\($all_non_nested\)${description_state}"
+
+# List monitors and containers
+check "list all monitors" \
+	"$RV list" 0 "" "" "^\($line_nested\|$line_non_nested\)$"
+
+check_if_exists "list container" \
+	"$RV list sched" "$RVDIR/monitors/sched" \
+	"" "-- No monitor found in container sched --" \
+	"^\($sched_monitors\)${description_state}$"
+
+check_if_exists "list non-container" \
+	"$RV list wwnr" "$RVDIR/monitors/wwnr" \
+	"-- No monitor found in container wwnr --" \
+	"^\( - \)\?[[:alnum:]]\+${description_state}$"
+
+check "list incomplete container name" \
+	"$RV list s" 0 "-- No monitor found in container s --"
+
+# Error handling tests
+check "no command" \
+	"$RV" 1 "rv requires a command"
+
+check "invalid command" \
+	"$RV invalid" 1 "rv does not know the invalid command"
+
+test_end
diff --git a/tools/verification/rv/tests/rv_mon.t b/tools/verification/rv/tests/rv_mon.t
new file mode 100644
index 000000000000..cbc346c74c71
--- /dev/null
+++ b/tools/verification/rv/tests/rv_mon.t
@@ -0,0 +1,95 @@
+#!/bin/bash
+# SPDX-License-Identifier: GPL-2.0
+source ../tests/engine.sh
+test_begin
+
+set_timeout 30s
+
+RVDIR=/sys/kernel/tracing/rv/
+
+# Help and basic tests
+check "verify mon subcommand help" \
+	"$RV mon --help" 0 "run a monitor"
+
+# Error handling tests
+check "mon without monitor name" \
+	"$RV mon" 1 "usage: rv mon"
+
+check "invalid monitor name" \
+	"$RV mon invalid" 1 "monitor invalid does not exist"
+
+if [ -d $RVDIR/monitors/wwnr ]; then
+
+check "invalid reactor name" \
+	"$RV mon wwnr -r invalid" 1 "failed to set invalid reactor, is it available?"
+
+check "monitor name is substring of another monitor" \
+	"$RV mon nr" 1 "monitor nr does not exist"
+
+check "already enabled monitor returns error" \
+	"echo 1 > $RVDIR/monitors/wwnr/enable; $RV mon wwnr" 1 \
+	"monitor wwnr (in-kernel) is already enabled"
+echo 0 > $RVDIR/monitors/wwnr/enable
+
+fi
+
+# rv mon runs until terminated
+set_expected_timeout 2s
+
+# Run monitors with different configurations
+check_if_exists "run the monitor without parameters" \
+	"$RV mon wwnr" "$RVDIR/monitors/wwnr" "" "."
+
+check_if_exists "run the monitor as verbose" \
+	"$RV mon wwnr -v" "$RVDIR/monitors/wwnr" \
+	"my pid is \$pid" "\(event\|error\)"
+
+check_if_exists "run the monitor with a reactor" \
+	"$RV mon wwnr -r printk & sleep .5 && cat $RVDIR/monitors/wwnr/reactors && wait" \
+	"$RVDIR/monitors/wwnr/reactors" "\[printk\]"
+
+check_if_exists "reactor is restored after exit" \
+	"cat $RVDIR/monitors/wwnr/reactors" \
+	"$RVDIR/monitors/wwnr/reactors" "\[nop\]"
+
+check_if_exists "run a nested monitor with a reactor" \
+	"$RV mon snroc -r printk & sleep .5 && cat $RVDIR/monitors/sched/snroc/reactors && wait" \
+	"$RVDIR/monitors/sched/snroc/reactors" "\[printk\]"
+
+check_if_exists "run an explicitly nested monitor with a reactor" \
+	"$RV mon sched:sssw -r printk & sleep .5 && cat $RVDIR/monitors/sched/sssw/reactors && wait" \
+	"$RVDIR/monitors/sched/sssw/reactors" "\[printk\]"
+
+check_if_exists "run container monitor" \
+	"$RV mon sched & sleep .5 && cat $RVDIR/monitors/sched/{sssw,sco}/enable && wait" \
+	"$RVDIR/monitors/sched" "1" "0" "^1$"
+
+# Regexes for the trace
+header="^[[:space:]]\+\(\([][A-Z_x<>-]\+\||\)[[:space:]]*\)\+$"
+type="\(event\|error\)[[:space:]]\+"
+genpid="[0-9]\+[[:space:]]\+"
+selfpid="\$pid[[:space:]]\+"
+cpu="\[[0-9]\{3\}\][[:space:]]\+"
+state="[a-z_]\+ "
+trace_task="${genpid}${cpu}${type}${genpid}${state}"
+trace_task_self="${genpid}${cpu}${type}${selfpid}${state}"
+trace_cpu="${genpid}${cpu}${type}${state}"
+trace_cpu_self="${selfpid}${cpu}${type}${state}"
+
+check_if_exists "run per-task monitor with tracing" \
+	"$RV mon sssw -t" "$RVDIR/monitors/sched/sssw" \
+	"$header" "$trace_task_self" "\($header\|$trace_task\)"
+
+check_if_exists "run per-task monitor tracing also self" \
+	"$RV mon sched:sssw -t -s" "$RVDIR/monitors/sched/sssw" \
+	"$trace_task_self" "" "\($header\|$trace_task\)"
+
+check_if_exists "run per-cpu monitor with tracing" \
+	"$RV mon sched:sco -t" "$RVDIR/monitors/sched/sco" \
+	"$header" "$trace_cpu_self" "\($header\|$trace_cpu\)"
+
+check_if_exists "run per-cpu monitor tracing also self" \
+	"$RV mon sco -t -s" "$RVDIR/monitors/sched/sco" \
+	"$trace_cpu_self" "" "\($header\|$trace_cpu\)"
+
+test_end
diff --git a/tools/verification/rvgen/Makefile b/tools/verification/rvgen/Makefile
index cfc4056c1e87..48d0376a5cc4 100644
--- a/tools/verification/rvgen/Makefile
+++ b/tools/verification/rvgen/Makefile
@@ -13,12 +13,17 @@ 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
diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py
index 5c923dc10d0f..246b43fa29f1 100644
--- a/tools/verification/rvgen/__main__.py
+++ b/tools/verification/rvgen/__main__.py
@@ -6,14 +6,16 @@
 # dot2k: transform dot files into a monitor for the Linux kernel.
 #
 # For further information, see:
-#   Documentation/trace/rv/da_monitor_synthesis.rst
+#   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
 
@@ -41,6 +43,11 @@ if __name__ == '__main__':
     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:
@@ -55,10 +62,17 @@ if __name__ == '__main__':
             else:
                 print("Unknown monitor class:", params.monitor_class)
                 sys.exit(1)
-        else:
+        elif params.subcmd == "container":
             monitor = Container(vars(params))
-    except AutomataError as e:
-        print(f"There was an error processing {params.spec}: {e}", file=sys.stderr)
+        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}")
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index b9f8149f7118..fd37ce304276 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -9,22 +9,349 @@
 #   Documentation/trace/rv/deterministic_automata.rst
 
 import ntpath
-import re
-from typing import Iterator
-from itertools import islice
 
-class _ConstraintKey:
-    """Base class for constraint keys."""
+import lark
 
-class _StateConstraintKey(_ConstraintKey, int):
-    """Key for a state constraint. Under the hood just state_id."""
-    def __new__(cls, state_id: int):
-        return super().__new__(cls, state_id)
+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 "}"
 
-class _EventConstraintKey(_ConstraintKey, tuple):
-    """Key for an event constraint. Under the hood just tuple(state_id,event_id)."""
-    def __new__(cls, state_id: int, event_id: int):
-        return super().__new__(cls, (state_id, event_id))
+    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.
@@ -44,35 +371,19 @@ class Automata:
 
     invalid_state_str = "INVALID_STATE"
     init_marker = "__init_"
-    node_marker = "{node"
-    # val can be numerical, uppercase (constant or macro), lowercase (parameter or function)
-    # only numerical values should have units
-    constraint_rule = re.compile(r"""
-        ^
-        (?P<env>[a-zA-Z_][a-zA-Z0-9_]+)  # C-like identifier for the env var
-        (?P<op>[!<=>]{1,2})              # operator
-        (?P<val>
-            [0-9]+ |                     # numerical value
-            [A-Z_]+\(\) |                # macro
-            [A-Z_]+ |                    # constant
-            [a-z_]+\(\) |                # function
-            [a-z_]+                      # parameter
-        )
-        (?P<unit>[a-z]{1,2})?            # optional unit for numerical values
-        """, re.VERBOSE)
-    constraint_reset = re.compile(r"^reset\((?P<env>[a-zA-Z_][a-zA-Z0-9_]+)\)")
 
     def __init__(self, file_path, model_name=None):
         self.__dot_path = file_path
         self.name = model_name or self.__get_model_name()
-        self.__dot_lines = self.__open_dot()
-        self.states, self.initial_state, self.final_states = self.__get_state_variables()
+        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.constraints = self.__create_matrix()
+        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)
@@ -90,194 +401,94 @@ class Automata:
 
         return model_name
 
-    def __open_dot(self) -> list[str]:
-        dot_lines = []
-        try:
-            with open(self.__dot_path) as dot_file:
-                dot_lines = dot_file.readlines()
-        except OSError as exc:
-            raise AutomataError(exc.strerror) from exc
+    def __parse_transitions(self):
+        transitions = []
 
-        if not dot_lines:
-            raise AutomataError(f"{self.__dot_path} is empty")
+        for edge in self.__parse_tree.edges:
+            attr = self.__parse_tree.edge_attrs.get(edge)
+            if not attr:
+                continue
 
-        # checking the first line:
-        line = dot_lines[0].split()
+            label = attr.get("label")
 
-        if len(line) < 2 or line[0] != "digraph" or line[1] != "state_automaton":
-            raise AutomataError(f"Not a valid .dot format: {self.__dot_path}")
+            src, dst = edge
 
-        return dot_lines
+            parser = EventLabelParser(label)
+            for event, reset, rule in parser.events:
+                transitions.append(Transition(src, dst, event, reset, rule))
 
-    def __get_cursor_begin_states(self) -> int:
-        for cursor, line in enumerate(self.__dot_lines):
-            split_line = line.split()
+        transitions.sort(key=lambda t : (t.src, t.event))
+        return transitions
 
-            if len(split_line) and split_line[0] == self.node_marker:
-                return cursor
+    def __parse_states(self):
+        initial_state = ""
+        states = []
+        final_states = []
 
-        raise AutomataError("Could not find a beginning state")
+        for node in self.__parse_tree.nodes:
+            attr = self.__parse_tree.node_attrs[node]
+            label = attr.get("label")
 
-    def __get_cursor_begin_events(self) -> int:
-        state = 0
-        cursor = 0 # make pyright happy
+            if node.startswith(Automata.init_marker):
+                initial_state = node[len(Automata.init_marker):]
 
-        for cursor, line in enumerate(self.__dot_lines):
-            line = line.split()
-            if not line:
+            if not label:
                 continue
 
-            if state == 0:
-                if line[0] == self.node_marker:
-                    state = 1
-            elif line[0] != self.node_marker:
-                break
-        else:
-            raise AutomataError("Could not find beginning event")
+            parser = StateLabelParser(label)
+            state = State(parser.state, parser.constraint)
 
-        cursor += 1 # skip initial state transition
-        if cursor == len(self.__dot_lines):
-            raise AutomataError("Dot file ended after event beginning")
+            states.append(state)
 
-        return cursor
+            shape = attr.get("shape")
+            if shape in ("doublecircle", "ellipse"):
+                final_states.append(state)
 
-    def __get_state_variables(self) -> tuple[list[str], str, list[str]]:
-        # wait for node declaration
-        states = []
-        final_states = []
-        initial_state = ""
-
-        has_final_states = False
-        cursor = self.__get_cursor_begin_states()
-
-        # process nodes
-        for line in islice(self.__dot_lines, cursor, None):
-            split_line = line.split()
-            if not split_line or split_line[0] != self.node_marker:
-                break
-
-            raw_state = split_line[-1]
-
-            #  "enabled_fired"}; -> enabled_fired
-            state = raw_state.replace('"', '').replace('};', '').replace(',', '_')
-            if state.startswith(self.init_marker):
-                initial_state = state[len(self.init_marker):]
-            else:
-                states.append(state)
-                if "doublecircle" in line:
-                    final_states.append(state)
-                    has_final_states = True
-
-                if "ellipse" in line:
-                    final_states.append(state)
-                    has_final_states = True
 
+        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")
 
-        states = sorted(set(states))
-        states.remove(initial_state)
-
-        # Insert the initial state at the beginning of the states
-        states.insert(0, initial_state)
-
-        if not has_final_states:
+        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] = []
-        # here we are at the begin of transitions, take a note, we will return later.
-        cursor = self.__get_cursor_begin_events()
-
-        for line in map(str.lstrip, islice(self.__dot_lines, cursor, None)):
-            if not line.startswith('"'):
-                break
 
-            # transitions have the format:
-            # "all_fired" -> "both_fired" [ label = "disable_irq" ];
-            #  ------------ event is here ------------^^^^^
-            split_line = line.split()
-            if len(split_line) > 1 and split_line[1] == "->":
-                event = "".join(split_line[split_line.index("label") + 2:-1]).replace('"', '')
+        for transition in self.transitions:
+            events.append(transition.event)
 
-                # when a transition has more than one label, they are like this
-                # "local_irq_enable\nhw_local_irq_enable_n"
-                # so split them.
+            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 i in event.split("\\n"):
-                    # if the event contains a constraint (hybrid automata),
-                    # it will be separated by a ";":
-                    # "sched_switch;x<1000;reset(x)"
-                    ev, *constr = i.split(";")
-                    if constr:
-                        if len(constr) > 2:
-                            raise AutomataError("Only 1 constraint and 1 reset are supported")
-                        envs += self.__extract_env_var(constr)
-                    events.append(ev)
-            else:
-                # state labels have the format:
-                # "enable_fired" [label = "enable_fired\ncondition"];
-                #  ----- label is here -----^^^^^
-                # label and node name must be the same, condition is optional
-                state = line.split("label")[1].split('"')[1]
-                _, *constr = state.split("\\n")
-                if constr:
-                    if len(constr) > 1:
-                        raise AutomataError("Only 1 constraint is supported in the state")
-                    envs += self.__extract_env_var([constr[0].replace(" ", "")])
+        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 _split_constraint_expr(self, constr: list[str]) -> Iterator[tuple[str,
-                                                                          str | None]]:
-        """
-        Get a list of strings of the type constr1 && constr2 and returns a list of
-        constraints and separators: [[constr1,"&&"],[constr2,None]]
-        """
-        exprs = []
-        seps = []
-        for c in constr:
-            while "&&" in c or "||" in c:
-                a = c.find("&&")
-                o = c.find("||")
-                pos = a if o < 0 or 0 < a < o else o
-                exprs.append(c[:pos].replace(" ", ""))
-                seps.append(c[pos:pos + 2].replace(" ", ""))
-                c = c[pos + 2:].replace(" ", "")
-            exprs.append(c)
-            seps.append(None)
-        return zip(exprs, seps)
+    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 __extract_env_var(self, constraint: list[str]) -> list[str]:
-        env = []
-        for c, _ in self._split_constraint_expr(constraint):
-            rule = self.constraint_rule.search(c)
-            reset = self.constraint_reset.search(c)
-            if rule:
-                env.append(rule["env"])
-                if rule.groupdict().get("unit"):
-                    self.env_types[rule["env"]] = rule["unit"]
-                if rule["val"][0].isalpha():
-                    self.constraint_vars.add(rule["val"])
-                # try to infer unit from constants or parameters
-                val_for_unit = rule["val"].lower().replace("()", "")
-                if val_for_unit.endswith("_ns"):
-                    self.env_types[rule["env"]] = "ns"
-                if val_for_unit.endswith("_jiffies"):
-                    self.env_types[rule["env"]] = "j"
-            if reset:
-                env.append(reset["env"])
-                # environment variables that are reset need a storage
-                self.env_stored.add(reset["env"])
-        return env
-
-    def __create_matrix(self) -> tuple[list[list[str]], dict[_ConstraintKey, list[str]]]:
+    def __create_matrix(self) -> list[list[str]]:
         # transform the array into a dictionary
         events = self.events
-        states = self.states
+        states = [s.name for s in self.states]
         events_dict = {}
         states_dict = {}
         nr_event = 0
@@ -292,39 +503,16 @@ class Automata:
 
         # declare the matrix....
         matrix = [[self.invalid_state_str for _ in range(nr_event)] for _ in range(nr_state)]
-        constraints: dict[_ConstraintKey, list[str]] = {}
-
-        # and we are back! Let's fill the matrix
-        cursor = self.__get_cursor_begin_events()
 
-        for line in map(str.lstrip,
-                        islice(self.__dot_lines, cursor, None)):
+        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
 
-            if not line or line[0] != '"':
-                break
-
-            split_line = line.split()
-
-            if len(split_line) > 2 and split_line[1] == "->":
-                origin_state = split_line[0].replace('"', '').replace(',', '_')
-                dest_state = split_line[2].replace('"', '').replace(',', '_')
-                possible_events = "".join(split_line[split_line.index("label") + 2:-1]).replace('"', '')
-                for event in possible_events.split("\\n"):
-                    event, *constr = event.split(";")
-                    if constr:
-                        key = _EventConstraintKey(states_dict[origin_state], events_dict[event])
-                        constraints[key] = constr
-                        # those events reset also on self loops
-                        if origin_state == dest_state and "reset" in "".join(constr):
-                            self.self_loop_reset_events.add(event)
-                    matrix[states_dict[origin_state]][events_dict[event]] = dest_state
-            else:
-                state = line.split("label")[1].split('"')[1]
-                state, *constr = state.replace(" ", "").split("\\n")
-                if constr:
-                    constraints[_StateConstraintKey(states_dict[state])] = constr
-
-        return matrix, constraints
+        return matrix
 
     def __store_init_events(self) -> tuple[list[bool], list[bool]]:
         events_start = [False] * len(self.events)
@@ -336,7 +524,7 @@ class Automata:
             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:
+                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
@@ -359,10 +547,3 @@ class Automata:
 
     def is_hybrid_automata(self) -> bool:
         return bool(self.envs)
-
-    def is_event_constraint(self, key: _ConstraintKey) -> bool:
-        """
-        Given the key in self.constraints return true if it is an event
-        constraint, false if it is a state constraint
-        """
-        return isinstance(key, _EventConstraintKey)
diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py
index fc85ba1f649e..22938ce1bf6c 100644
--- a/tools/verification/rvgen/rvgen/dot2c.py
+++ b/tools/verification/rvgen/rvgen/dot2c.py
@@ -29,10 +29,10 @@ class Dot2c(Automata):
 
     def __get_enum_states_content(self) -> list[str]:
         buff = []
-        buff.append(f"\t{self.initial_state}{self.enum_suffix},")
+        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}{self.enum_suffix},")
+                buff.append(f"\t{state.name}{self.enum_suffix},")
         buff.append(f"\tstate_max{self.enum_suffix},")
 
         return buff
@@ -142,7 +142,7 @@ class Dot2c(Automata):
     def format_aut_init_states_string(self) -> list[str]:
         buff = []
         buff.append("\t.state_names = {")
-        buff.append(self.__get_string_vector_per_line_content(self.states))
+        buff.append(self.__get_string_vector_per_line_content([s.name for s in self.states]))
         buff.append("\t},")
 
         return buff
@@ -159,7 +159,7 @@ class Dot2c(Automata):
         return buff
 
     def __get_max_strlen_of_states(self) -> int:
-        max_state_name = len(max(self.states, key=len))
+        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:
@@ -199,7 +199,7 @@ class Dot2c(Automata):
         return buff
 
     def get_aut_init_initial_state(self) -> str:
-        return self.initial_state
+        return self.initial_state.name
 
     def format_aut_init_initial_state(self) -> list[str]:
         buff = []
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index 110cfd69e53a..fd3254ea5b4d 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -6,17 +6,18 @@
 # dot2k: transform dot files into a monitor for the Linux kernel.
 #
 # For further information, see:
-#   Documentation/trace/rv/da_monitor_synthesis.rst
+#   Documentation/trace/rv/monitor_synthesis.rst
 
-from collections import deque
 from .dot2c import Dot2c
 from .generator import Monitor
-from .automata import _EventConstraintKey, _StateConstraintKey, AutomataError
-
+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)
@@ -56,18 +57,30 @@ class dot2k(Monitor, Dot2c):
                 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]:
@@ -176,7 +189,14 @@ class ha2k(dot2k):
         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.__parse_constraints()
+        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():
@@ -209,38 +229,52 @@ class ha2k(dot2k):
                 value *= 10**9
         return str(value) + "ull"
 
-    def __parse_single_constraint(self, rule: dict, value: str) -> str:
-        return f"ha_get_env(ha_mon, {rule["env"]}{self.enum_suffix}, time_ns) {rule["op"]} {value}"
+    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)
 
-    def __get_constraint_env(self, constr: str) -> str:
-        """Extract the second argument from an ha_ function"""
-        env = constr.split("(")[1].split()[1].rstrip(")").rstrip(",")
-        assert env.removesuffix(f"_{self.name}") in self.envs
-        return env
+            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, constr: str) -> str:
+    def __start_to_invariant_check(self, inv: ConstraintCondition) -> str:
         # by default assume the timer has ns expiration
-        env = self.__get_constraint_env(constr)
         clock_type = "ns"
-        if self.env_types.get(env.removesuffix(f"_{self.name}")) == "j":
+        if inv.unit == "j":
             clock_type = "jiffy"
 
-        return f"return ha_check_invariant_{clock_type}(ha_mon, {env}, time_ns)"
+        value = self.__adjust_value(inv.val, inv.unit)
 
-    def __start_to_conv(self, constr: str) -> str:
-        """
-        Undo the storage conversion done by ha_start_timer_
-        """
-        return "ha_inv_to_guard" + constr[constr.find("("):]
+        return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_{self.name}, time_ns, {value})"
 
-    def __parse_timer_constraint(self, rule: dict, value: str) -> str:
+    def __parse_invariant(self, inv):
         # by default assume the timer has ns expiration
         clock_type = "ns"
-        if self.env_types.get(rule["env"]) == "j":
+        if inv.unit == "j":
             clock_type = "jiffy"
 
-        return (f"ha_start_timer_{clock_type}(ha_mon, {rule["env"]}{self.enum_suffix},"
-                f" {value}, time_ns)")
+        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]:
         """
@@ -259,124 +293,35 @@ class ha2k(dot2k):
         rules = invalid_checks + rules
 
         separator = "\n\t\t      " if sum(len(r) for r in rules) > 80 else " "
-        return ["res = " + separator.join(rules)]
-
-    def __validate_constraint(self, key: tuple[int, int] | int, constr: str,
-                              rule, reset) -> None:
-        # event constrains are tuples and allow both rules and reset
-        # state constraints are only used for expirations (e.g. clk<N)
-        if self.is_event_constraint(key):
-            if not rule and not reset:
-                raise AutomataError("Unrecognised event constraint "
-                                    f"({self.states[key[0]]}/{self.events[key[1]]}: {constr})")
-            if rule and (rule["env"] in self.env_types and
-                         rule["env"] not in self.env_stored):
-                raise AutomataError("Clocks in hybrid automata always require a storage"
-                                    f" ({rule["env"]})")
-        else:
-            if not rule:
-                raise AutomataError("Unrecognised state constraint "
-                                    f"({self.states[key]}: {constr})")
-            if rule["env"] not in self.env_stored:
-                raise AutomataError("State constraints always require a storage "
-                                    f"({rule["env"]})")
-            if rule["op"] not in ["<", "<="]:
-                raise AutomataError("State constraints must be clock expirations like"
-                                    f" clk<N ({rule.string})")
-
-    def __parse_constraints(self) -> None:
-        self.guards: dict[_EventConstraintKey, str] = {}
-        self.invariants: dict[_StateConstraintKey, str] = {}
-        for key, constraint in self.constraints.items():
-            rules = []
-            resets = []
-            for c, sep in self._split_constraint_expr(constraint):
-                rule = self.constraint_rule.search(c)
-                reset = self.constraint_reset.search(c)
-                self.__validate_constraint(key, c, rule, reset)
-                if rule:
-                    value = rule["val"]
-                    value_len = len(rule["val"])
-                    unit = None
-                    if rule.groupdict().get("unit"):
-                        value_len += len(rule["unit"])
-                        unit = rule["unit"]
-                    c = c[:-(value_len)]
-                    value = self.__adjust_value(value, unit)
-                    if self.is_event_constraint(key):
-                        c = self.__parse_single_constraint(rule, value)
-                        if sep:
-                            c += f" {sep}"
-                    else:
-                        c = self.__parse_timer_constraint(rule, value)
-                    rules.append(c)
-                if reset:
-                    c = f"ha_reset_env(ha_mon, {reset["env"]}{self.enum_suffix}, time_ns)"
-                    resets.append(c)
-            if self.is_event_constraint(key):
-                res = self.__format_guard_rules(rules) + resets
-                self.guards[key] = ";".join(res)
-            else:
-                self.invariants[key] = rules[0]
+        return ["res = " + separator.join(rules) + ";"]
 
     def __fill_verify_invariants_func(self) -> list[str]:
-        buff = []
-        if not self.invariants:
+        if not self.has_invariant:
             return []
 
-        buff.append(
+        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, constr in sorted(self.invariants.items()):
-            check_str = self.__start_to_invariant_check(constr)
-            buff.append(f"\t{_else}if (curr_state == {self.states[state]}{self.enum_suffix})")
-            buff.append(f"\t\t{check_str};")
-            _else = "else "
-
-        buff.append("\treturn true;\n}\n")
-        return buff
-
-    def __fill_convert_inv_guard_func(self) -> list[str]:
-        buff = []
-        if not self.invariants:
-            return []
-
-        conflict_guards, conflict_invs = self.__find_inv_conflicts()
-        if not conflict_guards and not conflict_invs:
-            return []
-
-        buff.append(
-f"""static inline void ha_convert_inv_guard(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)
-{{""")
-        buff.append("\tif (curr_state == next_state)\n\t\treturn;")
+{{"""]
 
         _else = ""
-        for state, constr in sorted(self.invariants.items()):
-            # a state with invariant can reach us without reset
-            # multiple conflicts must have the same invariant, otherwise we cannot
-            # know how to reset the value
-            conf_i = [start for start, end in conflict_invs if end == state]
-            # we can reach a guard without reset
-            conf_g = [e for s, e in conflict_guards if s == state]
-            if not conf_i and not conf_g:
+        for state in self.states:
+            if not state.inv:
                 continue
-            buff.append(f"\t{_else}if (curr_state == {self.states[state]}{self.enum_suffix})")
 
-            buff.append(f"\t\t{self.__start_to_conv(constr)};")
+            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("}\n")
+        buff.append("\treturn true;\n}\n")
         return buff
 
     def __fill_verify_guards_func(self) -> list[str]:
         buff = []
-        if not self.guards:
+
+        if not self.has_guard:
             return []
 
         buff.append(
@@ -388,14 +333,22 @@ f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
 """)
 
         _else = ""
-        for edge, constr in sorted(self.guards.items()):
+        for transition in self.transitions:
+            if not transition.rule and not transition.reset:
+                continue
+
             buff.append(f"\t{_else}if (curr_state == "
-                        f"{self.states[edge[0]]}{self.enum_suffix} && "
-                        f"event == {self.events[edge[1]]}{self.enum_suffix})")
-            if constr.count(";") > 0:
+                        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] += " {"
-            buff += [f"\t\t{c};" for c in constr.split(";")]
-            if constr.count(";") > 0:
+            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 "
@@ -404,64 +357,15 @@ f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
         buff.append("\treturn res;\n}\n")
         return buff
 
-    def __find_inv_conflicts(self) -> tuple[set[tuple[int, _EventConstraintKey]],
-                                            set[tuple[int, _StateConstraintKey]]]:
-        """
-        Run a breadth first search from all states with an invariant.
-        Find any conflicting constraints reachable from there, this can be
-        another state with an invariant or an edge with a non-reset guard.
-        Stop when we find a reset.
-
-        Return the set of conflicting guards and invariants as tuples of
-        conflicting state and constraint key.
-        """
-        conflict_guards: set[tuple[int, _EventConstraintKey]] = set()
-        conflict_invs: set[tuple[int, _StateConstraintKey]] = set()
-        for start_idx in self.invariants:
-            queue = deque([(start_idx, 0)])  # (state_idx, distance)
-            env = self.__get_constraint_env(self.invariants[start_idx])
-
-            while queue:
-                curr_idx, distance = queue.popleft()
-
-                # Check state condition
-                if curr_idx != start_idx and curr_idx in self.invariants:
-                    conflict_invs.add((start_idx, _StateConstraintKey(curr_idx)))
-                    continue
-
-                # Check if we should stop
-                if distance > len(self.states):
-                    break
-                if curr_idx != start_idx and distance > 1:
-                    continue
-
-                for event_idx, next_state_name in enumerate(self.function[curr_idx]):
-                    if next_state_name == self.invalid_state_str:
-                        continue
-                    curr_guard = self.guards.get((curr_idx, event_idx), "")
-                    if "reset" in curr_guard and env in curr_guard:
-                        continue
-
-                    if env in curr_guard:
-                        conflict_guards.add((start_idx,
-                                             _EventConstraintKey(curr_idx, event_idx)))
-                        continue
-
-                    next_idx = self.states.index(next_state_name)
-                    queue.append((next_idx, distance + 1))
-
-        return conflict_guards, conflict_invs
-
     def __fill_setup_invariants_func(self) -> list[str]:
-        buff = []
-        if not self.invariants:
+        if not self.has_invariant:
             return []
 
-        buff.append(
+        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}"
@@ -470,13 +374,20 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
         buff.append(f"\tif ({condition_str})\n\t\treturn;")
 
         _else = ""
-        for state, constr in sorted(self.invariants.items()):
-            buff.append(f"\t{_else}if (next_state == {self.states[state]}{self.enum_suffix})")
-            buff.append(f"\t\t{constr};")
+        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.invariants:
-            buff.append(f"\telse if (curr_state == {self.states[state]}{self.enum_suffix})")
+        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")
@@ -484,7 +395,7 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
 
     def __fill_constr_func(self) -> list[str]:
         buff = []
-        if not self.constraints:
+        if not self.has_invariant and not self.has_guard:
             return []
 
         buff.append(
@@ -496,16 +407,9 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
  * 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.
- * Due to the different representations between invariants and guards, there is
- * a function to convert it in case invariants or guards are reachable from
- * another invariant without reset. Those are not present if not required in
- * the model. This is all automatic but is worth checking because it may show
- * errors in the model (e.g. missing resets).
  */""")
 
         buff += self.__fill_verify_invariants_func()
-        inv_conflicts = self.__fill_convert_inv_guard_func()
-        buff += inv_conflicts
         buff += self.__fill_verify_guards_func()
         buff += self.__fill_setup_invariants_func()
 
@@ -515,18 +419,15 @@ f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon,
 \t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns)
 {{""")
 
-        if self.invariants:
+        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 inv_conflicts:
-            buff.append("\tha_convert_inv_guard(ha_mon, curr_state, event, "
-                        "next_state, time_ns);\n")
 
-        if self.guards:
+        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.invariants:
+        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")
@@ -603,7 +504,7 @@ f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon,
         return self.__fill_hybrid_get_reset_functions() + self.__fill_constr_func()
 
     def _fill_timer_type(self) -> list:
-        if self.invariants:
+        if self.has_invariant:
             return [
                     "/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */",
                     "#define HA_TIMER_TYPE HA_TIMER_HRTIMER"
diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py
index 56f3bd8db850..45e2bab26cb5 100644
--- a/tools/verification/rvgen/rvgen/generator.py
+++ b/tools/verification/rvgen/rvgen/generator.py
@@ -6,7 +6,7 @@
 # Abstract class for generating kernel runtime verification monitors from specification file
 
 import platform
-import os
+from pathlib import Path
 
 
 class RVGenerator:
@@ -16,36 +16,38 @@ class RVGenerator:
         self.name = extra_params.get("model_name")
         self.parent = extra_params.get("parent")
         self.abs_template_dir = \
-            os.path.join(os.path.dirname(__file__), "templates", self.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()
+            self._fill_rv_kernel_dir()
 
-    def __fill_rv_kernel_dir(self):
+    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
 
-        # first try if we are running in the kernel tree root
-        if os.path.exists(self.rv_dir):
-            return
-
-        # offset if we are running inside the kernel tree from verification/dot2
-        kernel_path = os.path.join("../..", self.rv_dir)
+            if kernel_path.exists():
+                self.rv_dir = str(kernel_path)
+                return
 
-        if os.path.exists(kernel_path):
-            self.rv_dir = kernel_path
+        # 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 = os.path.join(f"/lib/modules/{platform.release()}/build", self.rv_dir)
+        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 os.path.exists(os.path.join(kernel_path, "rv_trace.h")):
-            self.rv_dir = kernel_path
+        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?")
@@ -57,12 +59,12 @@ class RVGenerator:
 
     def _read_template_file(self, file):
         try:
-            path = os.path.join(self.abs_template_dir, file)
+            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 = os.path.join(self.abs_template_dir, "..", file)
+            path = self.abs_template_dir.parent / file
             return self._read_file(path)
 
     def fill_parent(self):
@@ -133,7 +135,7 @@ class RVGenerator:
 
     def _patch_file(self, file, marker, line):
         assert self.auto_patch
-        file_to_patch = os.path.join(self.rv_dir, file)
+        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)
@@ -187,22 +189,19 @@ obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o
         return f"  - Move {self.name}/ to the kernel's monitor directory ({self.rv_dir}/monitors)"
 
     def __create_directory(self):
-        path = self.name
+        path = Path(self.name)
         if self.auto_patch:
-            path = os.path.join(self.rv_dir, "monitors", path)
-        try:
-            os.mkdir(path)
-        except FileExistsError:
-            return
+            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 = f"{self.name}/{file_name}"
+        path = Path(self.name) / file_name
         if self.auto_patch:
-            path = os.path.join(self.rv_dir, "monitors", path)
+            path = Path(self.rv_dir) / "monitors" / self.name / file_name
         self.__write_file(path, content)
 
     def print_files(self):
diff --git a/tools/verification/rvgen/rvgen/kunit.py b/tools/verification/rvgen/rvgen/kunit.py
new file mode 100644
index 000000000000..ed2082d7d3bc
--- /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 + ".bak"))
+                    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
index 016e7cf93bbb..7cebda61bce8 100644
--- a/tools/verification/rvgen/rvgen/ltl2ba.py
+++ b/tools/verification/rvgen/rvgen/ltl2ba.py
@@ -7,9 +7,7 @@
 # https://doi.org/10.1007/978-0-387-34892-6_1
 # With extra optimizations
 
-from ply.lex import lex
-from ply.yacc import yacc
-from .automata import AutomataError
+import lark
 
 # Grammar:
 # 	ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
@@ -30,42 +28,41 @@ from .automata import AutomataError
 #       imply
 #       equivalent
 
-tokens = (
-   'AND',
-   'OR',
-   'IMPLY',
-   'UNTIL',
-   'ALWAYS',
-   'EVENTUALLY',
-   'NEXT',
-   'VARIABLE',
-   'LITERAL',
-   'NOT',
-   'LPAREN',
-   'RPAREN',
-   'ASSIGN',
-)
+GRAMMAR = r'''
+start: assign+
 
-t_AND = r'and'
-t_OR = r'or'
-t_IMPLY = r'imply'
-t_UNTIL = r'until'
-t_ALWAYS = r'always'
-t_NEXT = r'next'
-t_EVENTUALLY = r'eventually'
-t_VARIABLE = r'[A-Z_0-9]+'
-t_LITERAL = r'true|false'
-t_NOT = r'not'
-t_LPAREN = r'\('
-t_RPAREN = r'\)'
-t_ASSIGN = r'='
-t_ignore_COMMENT = r'\#.*'
-t_ignore = ' \t\n'
+assign: VARIABLE "=" _ltl
 
-def t_error(t):
-    raise AutomataError(f"Illegal character '{t.value[0]}'")
+_ltl: _opd | binop | unop
 
-lexer = lex()
+_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
@@ -97,7 +94,7 @@ class GraphNode:
         return self.id < other.id
 
 class ASTNode:
-    uid = 1
+    uid = 0
 
     def __init__(self, op):
         self.op = op
@@ -433,90 +430,49 @@ class Literal:
         node.old |= {n}
         return node.expand(node_set)
 
-def p_spec(p):
-    '''
-    spec : assign
-         | assign spec
-    '''
-    if len(p) == 3:
-        p[2].append(p[1])
-        p[0] = p[2]
-    else:
-        p[0] = [p[1]]
-
-def p_assign(p):
-    '''
-    assign : VARIABLE ASSIGN ltl
-    '''
-    p[0] = (p[1], p[3])
-
-def p_ltl(p):
-    '''
-    ltl : opd
-        | binop
-        | unop
-    '''
-    p[0] = p[1]
+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 p_opd(p):
-    '''
-    opd : VARIABLE
-        | LITERAL
-        | LPAREN ltl RPAREN
-    '''
-    if p[1] == "true":
-        p[0] = ASTNode(Literal(True))
-    elif p[1] == "false":
-        p[0] = ASTNode(Literal(False))
-    elif p[1] == '(':
-        p[0] = p[2]
-    else:
-        p[0] = ASTNode(Variable(p[1]))
+    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 p_unop(p):
-    '''
-    unop : ALWAYS ltl
-         | EVENTUALLY ltl
-         | NEXT ltl
-         | NOT ltl
-    '''
-    if p[1] == "always":
-        op = AlwaysOp(p[2])
-    elif p[1] == "eventually":
-        op = EventuallyOp(p[2])
-    elif p[1] == "next":
-        op = NextOp(p[2])
-    elif p[1] == "not":
-        op = NotOp(p[2])
-    else:
-        raise AutomataError(f"Invalid unary operator {p[1]}")
+    def VARIABLE(self, args):
+        return ASTNode(Variable(args))
 
-    p[0] = ASTNode(op)
+    def LITERAL(self, args):
+        return ASTNode(Literal(args == "true"))
 
-def p_binop(p):
-    '''
-    binop : opd UNTIL ltl
-          | opd AND ltl
-          | opd OR ltl
-          | opd IMPLY ltl
-    '''
-    if p[2] == "and":
-        op = AndOp(p[1], p[3])
-    elif p[2] == "until":
-        op = UntilOp(p[1], p[3])
-    elif p[2] == "or":
-        op = OrOp(p[1], p[3])
-    elif p[2] == "imply":
-        op = ImplyOp(p[1], p[3])
-    else:
-        raise AutomataError(f"Invalid binary operator {p[2]}")
+    def start(self, node):
+        return node
 
-    p[0] = ASTNode(op)
+    def assign(self, node):
+        return node[0].op.name, node[1]
 
-parser = yacc()
+parser = lark.Lark(GRAMMAR)
 
 def parse_ltl(s: str) -> ASTNode:
-    spec = parser.parse(s)
+    try:
+        spec = parser.parse(s)
+    except lark.exceptions.UnexpectedInput as e:
+        raise LTLError(str(e))
+    spec = Transform().transform(spec)
 
     rule = None
     subexpr = {}
@@ -528,7 +484,7 @@ def parse_ltl(s: str) -> ASTNode:
             subexpr[assign[0]] = assign[1]
 
     if rule is None:
-        raise AutomataError("Please define your specification in the \"RULE = <LTL spec>\" format")
+        raise LTLError("Please define your specification in the \"RULE = <LTL spec>\" format")
 
     for node in rule:
         if not isinstance(node.op, Variable):
diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/rvgen/rvgen/ltl2k.py
index 81fd1f5ea5ea..f3781a3e0856 100644
--- a/tools/verification/rvgen/rvgen/ltl2k.py
+++ b/tools/verification/rvgen/rvgen/ltl2k.py
@@ -222,7 +222,7 @@ class ltl2k(generator.Monitor):
         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_sample_event);"
+        return f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_example_event);"
 
     def fill_atoms_init(self):
         buff = []
diff --git a/tools/verification/rvgen/rvgen/templates/container/main.c b/tools/verification/rvgen/rvgen/templates/container/main.c
index 5fc89b46f279..e6a20d74886c 100644
--- a/tools/verification/rvgen/rvgen/templates/container/main.c
+++ b/tools/verification/rvgen/rvgen/templates/container/main.c
@@ -31,5 +31,5 @@ module_init(register_%%MODEL_NAME%%);
 module_exit(unregister_%%MODEL_NAME%%);
 
 MODULE_LICENSE("GPL");
-MODULE_AUTHOR("dot2k: auto-generated");
+MODULE_AUTHOR("rvgen: auto-generated");
 MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%");
diff --git a/tools/verification/rvgen/rvgen/templates/dot2k/main.c b/tools/verification/rvgen/rvgen/templates/dot2k/main.c
index 889446760e3c..bd3e0aab9cc5 100644
--- a/tools/verification/rvgen/rvgen/templates/dot2k/main.c
+++ b/tools/verification/rvgen/rvgen/templates/dot2k/main.c
@@ -79,5 +79,5 @@ module_init(register_%%MODEL_NAME%%);
 module_exit(unregister_%%MODEL_NAME%%);
 
 MODULE_LICENSE("GPL");
-MODULE_AUTHOR("dot2k: auto-generated");
+MODULE_AUTHOR("rvgen: auto-generated");
 MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%");
diff --git a/tools/verification/rvgen/rvgen/templates/kunit.c b/tools/verification/rvgen/rvgen/templates/kunit.c
new file mode 100644
index 000000000000..62092b5cc6d4
--- /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
index f85d076fbf78..c33f21535a7a 100644
--- a/tools/verification/rvgen/rvgen/templates/ltl2k/main.c
+++ b/tools/verification/rvgen/rvgen/templates/ltl2k/main.c
@@ -77,7 +77,7 @@ static void disable_%%MODEL_NAME%%(void)
 /*
  * This is the monitor register section.
  */
-static struct rv_monitor rv_%%MODEL_NAME%% = {
+static struct rv_monitor rv_this = {
 	.name = "%%MODEL_NAME%%",
 	.description = "%%DESCRIPTION%%",
 	.enable = enable_%%MODEL_NAME%%,
@@ -86,17 +86,17 @@ static struct rv_monitor rv_%%MODEL_NAME%% = {
 
 static int __init register_%%MODEL_NAME%%(void)
 {
-	return rv_register_monitor(&rv_%%MODEL_NAME%%, %%PARENT%%);
+	return rv_register_monitor(&rv_this, %%PARENT%%);
 }
 
 static void __exit unregister_%%MODEL_NAME%%(void)
 {
-	rv_unregister_monitor(&rv_%%MODEL_NAME%%);
+	rv_unregister_monitor(&rv_this);
 }
 
 module_init(register_%%MODEL_NAME%%);
 module_exit(unregister_%%MODEL_NAME%%);
 
 MODULE_LICENSE("GPL");
-MODULE_AUTHOR(/* TODO */);
+MODULE_AUTHOR("rvgen: auto-generated");
 MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%");
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 000000000000..799fbf11c3ac
--- /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 000000000000..71b26ae2d51c
--- /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 000000000000..40b1f1c0c681
--- /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 000000000000..4d2730b71dd0
--- /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 000000000000..249ba3aee8d7
--- /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 000000000000..5c5d300b4183
--- /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 000000000000..3c8dc3b22443
--- /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 000000000000..59bfca8f73d2
--- /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 000000000000..c6f350179098
--- /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 000000000000..c1ae5078c4f9
--- /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 000000000000..837b238754b0
--- /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 000000000000..4e6086c4d86e
--- /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 000000000000..0cc185ccfddf
--- /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 000000000000..3a72e867122c
--- /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 000000000000..2538db4f6a26
--- /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 000000000000..074ddff6a60d
--- /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 000000000000..b37f46670bfd
--- /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 000000000000..2c60b5c5b4e0
--- /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 000000000000..7e5de351b8fa
--- /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 000000000000..ebd53621a5b1
--- /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 000000000000..175a416f8b18
--- /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 000000000000..16579c1c6910
--- /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 000000000000..2bfe4e37cea7
--- /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 000000000000..e2b9354034cc
--- /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.bak b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.c.bak
new file mode 100644
index 000000000000..f747925bf542
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.c.bak
@@ -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 000000000000..585c4803be23
--- /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 000000000000..b984208838c4
--- /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 000000000000..2becb65dddad
--- /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 000000000000..e7e34592c6c5
--- /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 000000000000..83e434432650
--- /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 000000000000..0143a148ef34
--- /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 000000000000..59b8dfabbbf1
--- /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 000000000000..d55795efbb61
--- /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 000000000000..8bd67115d244
--- /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 000000000000..6d664ba5624d
--- /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 000000000000..effd26548b07
--- /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 000000000000..290a9454caa4
--- /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 000000000000..17826a5c47c8
--- /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 000000000000..0094215ff4fb
--- /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 000000000000..16804a79e834
--- /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 000000000000..f4048290c774
--- /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 000000000000..9047ff725546
--- /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 000000000000..949fa4453403
--- /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 000000000000..381bafcb3322
--- /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 000000000000..6c48770ace1a
--- /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 000000000000..239b0539df18
--- /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 000000000000..5c428f818bdf
--- /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 000000000000..6214a4aa6d25
--- /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 000000000000..0b2030cb644a
--- /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 000000000000..6c13ee0068d3
--- /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 000000000000..e2d0e721f180
--- /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 000000000000..dd961c5dc8ad
--- /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 000000000000..7895f2e233e8
--- /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 000000000000..3571b004c114
--- /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 000000000000..3e334c344261
--- /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 000000000000..c1d58ce435a8
--- /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 000000000000..acc503b56e87
--- /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 000000000000..37dab5dfdebc
--- /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 000000000000..b2ca34be327f
--- /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 000000000000..a054d5b2c0ea
--- /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 000000000000..fa4fb3db8288
--- /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 000000000000..d27d9175f562
--- /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 000000000000..5f2562600bad
--- /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 000000000000..e555c239b221
--- /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 000000000000..cdd4192f58ae
--- /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 000000000000..af18ad7389ec
--- /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 000000000000..17c63fc57f17
--- /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 000000000000..cf36307e003c
--- /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 000000000000..06de6aa8709f
--- /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 000000000000..5ed658abd69c
--- /dev/null
+++ b/tools/verification/rvgen/tests/specs/test_ltl.ltl
@@ -0,0 +1 @@
+RULE = always (EVENT_A imply eventually EVENT_B)
diff --git a/tools/verification/tests/engine.sh b/tools/verification/tests/engine.sh
new file mode 100644
index 000000000000..cfdf2180aad8
--- /dev/null
+++ b/tools/verification/tests/engine.sh
@@ -0,0 +1,175 @@
+#!/bin/bash
+# SPDX-License-Identifier: GPL-2.0
+test_begin() {
+	# Count tests to allow the test harness to double-check if all were
+	# included correctly.
+	ctr=0
+	[ -z "$RV" ] && RV="../rv/rv"
+	[ -z "$RVGEN" ] && RVGEN="python3 ../rvgen"
+	[ -z "$GOLDEN_DIR" ] && GOLDEN_DIR="tests/golden"
+	[ -n "$TEST_COUNT" ] && echo "1..$TEST_COUNT"
+}
+
+failure() {
+	fail=1
+	if [ $# -gt 0 ]; then
+		failbuf+="$1"
+		failbuf+=$'\n'
+	fi
+}
+
+report() {
+	local desc="$1"
+
+	if [ "$fail" -eq 0 ]; then
+		echo "ok $ctr - $desc"
+	else
+		# Add output and exit code as comments in case of failure
+		echo "not ok $ctr - $desc"
+		echo -n "$failbuf"
+		echo "$result" | col -b | while read -r line; do echo "# $line"; done
+		printf "#\n# exit code %s\n" "$exitcode"
+	fi
+}
+
+_check() {
+	local command=$2
+	local expected_exitcode=${3:-0}
+	local expected_output=$4
+	local unexpected_output=$5
+	local all_lines_pattern=$6
+	local patterns="$expected_output $unexpected_output $all_lines_pattern"
+	local bgpid pid
+
+	eval "$TIMEOUT" "$command" &> check_output.$$ &
+	bgpid=$!
+
+	if grep -q "\$pid" <<< "$patterns"; then
+		for _ in {1..30}; do
+			pid=$(pgrep -f "${command%%[|;&>]*}" | tail -n1)
+			[ -n "$pid" ] && break
+			sleep 0.1
+		done
+	fi
+
+	wait $bgpid
+	exitcode=$?
+	result=$(tr -d '\0' < check_output.$$)
+	rm -f check_output.$$
+
+	failbuf=''
+	fail=0
+
+	# Suppress any other error if a needed pid is empty
+	if [ -z "$pid" ] && grep -q "\$pid" <<< "$patterns"; then
+		result=''
+		failure "# Empty pid for $command"
+		return 1
+	fi
+
+	expected_output="${expected_output//\$pid/$pid}"
+	unexpected_output="${unexpected_output//\$pid/$pid}"
+	all_lines_pattern="${all_lines_pattern//\$pid/$pid}"
+
+	# Test if the results matches if requested
+	if [ -n "$expected_output" ] && ! grep -qe "$expected_output" <<< "$result"; then
+		failure "# Output match failed: \"$expected_output\""
+	fi
+
+	if [ -n "$unexpected_output" ] && grep -qe "$unexpected_output" <<< "$result"; then
+		failure "# Output non-match failed: \"$unexpected_output\""
+	fi
+
+	if [ -n "$all_lines_pattern" ] && grep -vqe "$all_lines_pattern" <<< "$result"; then
+		failure "# All-lines pattern failed: \"$all_lines_pattern\""
+	fi
+
+	if [ $exitcode -ne "$expected_exitcode" ]; then
+		failure "# Expected exit code $expected_exitcode"
+	fi
+}
+
+check() {
+	# Simple check: run the command with given arguments and test exit code.
+	# If TEST_COUNT is set, run the test. Otherwise, just count.
+	ctr=$((ctr + 1))
+	if [ -n "$TEST_COUNT" ]; then
+		_check "$@"
+		report "$1"
+	fi
+}
+
+check_if_exists() {
+	# Conditional check that skips if a file or folder doesn't exist
+	local desc=$1
+	local command=$2
+	local file=$3
+	local expected_output=$4
+	local unexpected_output=$5
+	local all_lines_pattern=$6
+
+	ctr=$((ctr + 1))
+	if [ -n "$TEST_COUNT" ]; then
+		if [ ! -e "$file" ]; then
+			echo "ok $ctr - $desc # SKIP file not found: $file"
+		else
+			_check "$desc" "$command" 0 "$expected_output" \
+				"$unexpected_output" "$all_lines_pattern"
+			report "$desc"
+		fi
+	fi
+}
+
+check_and_compare_folder() {
+	# Run command, compare generated folder to golden, and cleanup
+	local desc=$1
+	local command=$2
+	local generated_dir=$3
+	local expected_output=$4
+	local unexpected_output=$5
+	local golden_dir="$GOLDEN_DIR/$generated_dir"
+
+	ctr=$((ctr + 1))
+	if [ -n "$TEST_COUNT" ]; then
+		rm -rf "$generated_dir"
+		_check "$desc" "$command" 0 "$expected_output" "$unexpected_output"
+
+		if [ "$fail" -eq 0 ] && [ ! -d "$generated_dir" ]; then
+			failure "# Generated directory not found: $generated_dir"
+		fi
+
+		if [ "$fail" -ne 0 ]; then
+			:
+		elif ! diff -r "$generated_dir" "$golden_dir" &> /dev/null; then
+			failure "# Directories differ:"
+			failbuf+=$(diff -r "$generated_dir" "$golden_dir" 2>&1 | sed 's/^/#   /')
+			failbuf+=$'\n'
+		fi
+
+		report "$1"
+
+		rm -rf "$generated_dir"
+	fi
+}
+
+set_timeout() {
+	TIMEOUT="timeout -v -k 30s $1"
+}
+
+set_expected_timeout() {
+	TIMEOUT="timeout --preserve-status -k 30s $1"
+}
+
+unset_timeout() {
+	unset TIMEOUT
+}
+
+test_end() {
+	# If running without TEST_COUNT, tests are not actually run, just
+	# counted. In that case, re-run the test with the correct count.
+	[ -z "$TEST_COUNT" ] && TEST_COUNT=$ctr exec bash "$0" || true
+}
+
+# Avoid any environmental discrepancies
+export LC_ALL=C
+unset_timeout