Re: [PATCH 2/2] verification/rvgen: Support the 'next' operator

[Gabriele Monaco]

On Fri, 2025-07-11 at 15:17 +0200, Nam Cao wrote:
> The 'next' operator is a unary operator. It is defined as: "next
> time, the
> operand must be true".
> 
> Support this operator. For RV monitors, "next time" means the next
> invocation of ltl_validate().
> 
> Signed-off-by: Nam Cao <namcao@xxxxxxxxxxxxx>

Hi Nam,

thanks for the series, I did a very stupid test like this:

  RULE = always (SCHEDULING imply next SWITCH)

Despite the monitor working or not, the generator created code that
doesn't build, specifically:

1. It creates a variable named switch
  - sure I could change the name, but perhaps we could prepend
something to make sure local variables are not C keywords

2. It created unused variables in ltl_start
  - _fill_atom_values creates all variables but _fill_start uses only
those where the .init field is true (maybe the model is wrong though)

Now, this specific model reports errors without the sched_switch_vain
tracepoint which I'm introducing in another patch.

For it to work, I have to define it in such a way that scheduling
becomes true at schedule_entry and becomes false right after the
switch:

schedule_entry
	SCHEDULING=true

sched_switch
	SWITCH=true

schedule_exit
	SCHEDULING=false
	SWITCH=false

If I understood correctly that's intended behaviour since swapping the
assignments in schedule_exit (or doing a pulse in sched_switch) would
add another event when scheduling is true, which is against the next
requirement.

Now I can't think of a way to rewrite the model to allow a pulse in
sched_switch, that is /whenever scheduling turns to true, the next
event is a switch/ instead of /any time scheduling is true, the next
event is a switch/.

I tried something like:
  RULE = always ((not SCHEDULING and next SCHEDULING) imply next
SWITCH)
but the parser got the two SCHEDULING as two different atoms, so I
guess I did something I was not supposed to do..

Is the next operator only meaningful for atoms that are mutually
exclusive (e.g. RED next GREEN, if GREEN is true RED turns to false)
and/or when playing with ltl_atom_set without triggering validations?

What am I missing here?

Thanks,
Gabriele

> ---
>  .../trace/rv/linear_temporal_logic.rst        |  1 +
>  tools/verification/rvgen/rvgen/ltl2ba.py      | 26
> +++++++++++++++++++
>  2 files changed, 27 insertions(+)
> 
> diff --git a/Documentation/trace/rv/linear_temporal_logic.rst
> b/Documentation/trace/rv/linear_temporal_logic.rst
> index 57f107fcf6dd..9eee09d9cacf 100644
> --- a/Documentation/trace/rv/linear_temporal_logic.rst
> +++ b/Documentation/trace/rv/linear_temporal_logic.rst
> @@ -41,6 +41,7 @@ Operands (opd):
>  Unary Operators (unop):
>      always
>      eventually
> +    next
>      not
>  
>  Binary Operators (binop):
> diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py
> b/tools/verification/rvgen/rvgen/ltl2ba.py
> index d11840af7f5f..f14e6760ac3d 100644
> --- a/tools/verification/rvgen/rvgen/ltl2ba.py
> +++ b/tools/verification/rvgen/rvgen/ltl2ba.py
> @@ -19,6 +19,7 @@ from ply.yacc import yacc
>  # Unary Operators (unop):
>  #       always
>  #       eventually
> +#       next
>  #       not
>  #
>  # Binary Operators (binop):
> @@ -35,6 +36,7 @@ tokens = (
>     'UNTIL',
>     'ALWAYS',
>     'EVENTUALLY',
> +   'NEXT',
>     'VARIABLE',
>     'LITERAL',
>     'NOT',
> @@ -48,6 +50,7 @@ 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'
> @@ -327,6 +330,26 @@ class AlwaysOp(UnaryOp):
>          # ![]F == <>(!F)
>          return EventuallyOp(self.child.negate()).normalize()
>  
> +class NextOp(UnaryOp):
> +    def normalize(self):
> +        return self
> +
> +    def _is_temporal(self):
> +        return True
> +
> +    def negate(self):
> +        # not (next A) == next (not A)
> +        self.child = self.child.negate()
> +        return self
> +
> +    @staticmethod
> +    def expand(n: ASTNode, node: GraphNode, node_set) ->
> set[GraphNode]:
> +        tmp = GraphNode(node.incoming,
> +                        node.new,
> +                        node.old | {n},
> +                        node.next | {n.op.child})
> +        return tmp.expand(node_set)
> +
>  class NotOp(UnaryOp):
>      def __str__(self):
>          return "!" + str(self.child)
> @@ -452,12 +475,15 @@ 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: