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

[Nam Cao <namcao@linutronix.de>]

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

Or if you want to allow some other things to happen inbetween, then:

     RULE = always (((not SCHEDULING) and (next SCHEDULING)) imply (SCHEDULING until SWITCH))

Best regards,
Nam