Support system verilog labeled statements

[chuckbenz]

Section 10.8 of the system verilog LRM covers labeled statements, and I'd like to try yosys on a project that has code using them. Here's an example of a labeled statement:

module test_label_prob ;
  bbb:   begin  end
endmodule

It's not necessary that yosys do anything with the label for my purposes, as I'm not aware of any other code in the project that uses the label (I imagine that the most obvious use of the label could be a disable statement at a higher level of hierarchy, but I expect those are more relevant to simulation rather than synthesis and formal validation.

Currently, yosys will provide the following error message: ERROR: Parser error in line test_label_prob.v:2: syntax error, unexpected ':', expecting TOK_ID or '#'

I suspect that the change will be a mild change to frontends/verilog/verilog_parser.y, but I never learned bison (or yacc or lex), so I'm at a loss when I look at the code.

I'd really love to try out yosys formal checking on this project, and the label usage is in a module commonly used throughout the project (and I imagine that there are more labeled statements).

Chuck

[cliffordwolf]

I suspect that the change will be a mild change to frontends/verilog/verilog_parser.y, but I never learned bison (or yacc or lex), so I'm at a loss when I look at the code.

Unfortunately it's a massive change. Because of the way we currently parse cell instantiations we run into a myriad of shift-reduce and reduce-reduce conflicts when trying to add other module items that start with a TOK_ID. (This is because of bad design decisions in our parser, not because of an inherent property of Verilog syntax.)

There's a big hack in place to allow labels on assert/assume/cover. Maybe we can extend that hack to other items, but I'd need a more detailed list of the items you'd like to have supported.