On Thu, 2026-05-28 at 10:27 +0200, Nam Cao wrote: > Prepare for self.invariants and __parse_constraints() to be removed. > convert __fill_setup_invariants_func() to use the new parsed states > from Lark. > > Signed-off-by: Nam Cao <[email protected]> > ---
Reviewed-by: Gabriele Monaco <[email protected]> > v2: add missing time conversion [Sashiko] > --- > tools/verification/rvgen/rvgen/dot2k.py | 44 ++++++++++++++++++++--- > -- > 1 file changed, 35 insertions(+), 9 deletions(-) > > diff --git a/tools/verification/rvgen/rvgen/dot2k.py > b/tools/verification/rvgen/rvgen/dot2k.py > index a344cbbcb346..d9f8e1c7737a 100644 > --- a/tools/verification/rvgen/rvgen/dot2k.py > +++ b/tools/verification/rvgen/rvgen/dot2k.py > @@ -250,6 +250,26 @@ class ha2k(dot2k): > return (f"ha_start_timer_{clock_type}(ha_mon, > {rule["env"]}{self.enum_suffix}," > f" {value}, time_ns)") > > + def __parse_invariant(self, inv): > + # by default assume the timer has ns expiration > + clock_type = "ns" > + if inv.unit == "j": > + clock_type = "jiffy" > + > + env = inv.env + self.enum_suffix > + val = inv.val.replace("()", "(ha_mon)") > + > + match inv.unit: > + case "us": > + val *= 10**3 > + case "ms": > + val *= 10**6 > + case "s": > + val *= 10**9 > + > + return (f"ha_start_timer_{clock_type}(ha_mon, {env}," > + f" {val}, time_ns)") > + > def __format_guard_rules(self, rules: list[str]) -> list[str]: > """ > Merge guard constraints as a single C return statement. > @@ -463,15 +483,14 @@ f"""static inline bool ha_verify_guards(struct > ha_monitor *ha_mon, > 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}" > @@ -480,13 +499,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")
