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

[Gabriele Monaco <gmonaco@redhat.com>]

On Mon, 2025-07-14 at 14:48 +0200, Nam Cao wrote:
> On Mon, Jul 14, 2025 at 02:42:10PM +0200, Nam Cao wrote:
> > On Mon, Jul 14, 2025 at 02:18:05PM +0200, Gabriele Monaco wrote:
> > > 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)
> > 
> > Be careful of operator precedence. This rule is also what I would
> > suggest,
> > but you need parentheses:
> > 
> >     RULE = always (((not SCHEDULING) and (next SCHEDULING)) imply
> > (next SWITCH))
> 
> Actually no, this also does not work. You need double 'next':
> 
>      RULE = always (((not SCHEDULING) and (next SCHEDULING)) imply
> (next next SWITCH))
> 

Thanks! This one seems to work.

> Not sure what you mean by .init field

I meant in ltl2k there's this condition for variable usage but not for
variable definition. I'm not sure exactly what it stands for.
  _fill_start():
	...
	if not node.init:
		continue

But I guess you got what I meant already.

> Btw, I think this "(not X) and (next X)" seems very useful. So we
> could
> define a helper for this, perhaps something like "rising_edge".

Yeah good idea! I see myself mixing up in the future otherwise..
I guess you'd need to define also a falling_edge for its counterpart.
Or perhaps making it more compact as just rising/falling (with good
documentation or references to somewhere defining it).

Also we need to make clear this operator takes 2 instances, so whatever
happens after (next) it needs a double next.

Maybe it gets complicated but in the future we might have also some
nextN (next2, next3, etc. with a sensible limit not to explode the
generated code) or something along the line.

> Thanks for the report, I will post some patches to address these
> problems
> with the scripts.

Great, thanks!
I'd say since those are unrelated and the next works as intended, feel
free to add

Tested-by: Gabriele Monaco <gmonaco@redhat.com>

Thanks again,
Gabriele