Re: [PATCH 03/13] verification/rvgen: Implement state and transition parser based on Lark

[Nam Cao]

Gabriele Monaco <gmonaco@xxxxxxxxxx> writes:
> Looks good, although I need to put more effort to understand the grammar.
> There's an issue parsing events though:
>
>> +class EventLabelParser:
>> +    grammar = r'''
>> +    events: event ("\\n" event)*
>> +
>> +    event: name (";" guard)*
>> +
>> +    guard: reset
>> +         | rule
>> +         | rule reset
>> +         | reset rule
>
> I'm not sure if it could be solved better changing the grammar, but this doesn't
> work in case we have both a reset and a rule, e.g.:
>
>   "event2;env1 == 0;reset(clk)"
>
> It apparently saves only one of them, the other would end up in args[2].

Thanks for pointing that out. The grammar is broken, it allows any
number of guards and does not require a ";" between reset and rule.

This grammar change fixes it:

diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index cc42b8127fc0..d8c5e9028364 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -275,12 +275,12 @@ class EventLabelParser:
     grammar = r'''
     events: event ("\\n" event)*
 
-    event: name (";" guard)*
+    event: name (";" guard)?
 
     guard: reset
          | rule
-         | rule reset
-         | reset rule
+         | rule ";" reset
+         | reset ";" rule
 
     name: CNAME
 
@@ -312,6 +312,7 @@ class EventLabelParser:
             return ConstraintCondition(*args)
 
         def event(self, args):
+            assert(len(args) <= 2)
             name = args[0]
             rule, reset = None, None
             if len(args) == 2: