Gabriele Monaco <[email protected]> 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:
