[PATCH 08/13] verification/rvgen: Simplify the generation for clock variables

Nam Cao
2026-05-05T06:59:49Z

Hybrid automata monitors's clock variables have been changed to have
only a single representation. Now there is no need to generate code to
convert between the two representations.

Delete __fill_convert_inv_guard_func() and its associates. Update
__start_to_invariant_check() to how invariants now work.

Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/dot2k.py | 89 +------------------------
1 file changed, 1 insertion(+), 88 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index cf7e5ddc649c..c662c888f991 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -247,7 +247,7 @@ class ha2k(dot2k):
if inv.unit == "j":
clock_type = "jiffy"

- return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_{self.name}, time_ns)"
+ return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_{self.name}, time_ns, {inv.val})"

def __start_to_conv(self, constr: str) -> str:
"""
@@ -376,40 +376,6 @@ f"""static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
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:
- 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)};")
- _else = "else "
-
- buff.append("}\n")
- return buff
-
def __fill_verify_guards_func(self) -> list[str]:
buff = []

@@ -449,54 +415,6 @@ 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]:
if not self.has_invariant:
return []
@@ -555,8 +473,6 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
*/""")

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()

@@ -569,9 +485,6 @@ f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon,
if self.invariants:
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:
buff.append("\tif (!ha_verify_guards(ha_mon, curr_state, event, "
--
2.47.3