slang-tidy: NoOldAlwaysSyntax improvement and legit uses of always @

[VJSchneid]

Hi everyone and @Sustrak,
I was currently looking into slang-tidy (great tool btw.) and was wondering, whether the NoOldAlwaysSyntax check should always issue a warning whenever an always @ is encountered. I think there are at least in formal verification some places, where always @ should not be replaced by always_ff, always_comb, etc.. Therefore, always issuing an warning might not be the best way to go here.
E.g. this might be a legit use of an always @ statement.

One way of handling this might be to just look whether there are assignments used inside the always block, because if there are assignment inside the block (which are not only local to the always_ff block) they are probably better located inside an always_ff, always_latch or always_comb block.
I would like to get my feet wet in this project by changing this check, but I'm very unsure, whether I'm missing something 😄
What do you guys think would that be a appropriate way of dealing with this or do you have any opinion about that?

[Sustrak]

Hi @VJSchneid I wasn't aware of the use of the always construct in Formal. Now that I am, the current solution for the NoOldAlwaysSyntax is definitely not robust enough.

I think the change you propose makes sense and it shouldn't be much difficult to implement. If you want please give it a try 😄. Else I'll try to do it when I have some spare time.

Thanks for the feedback on the tool

[Sustrak]

Hi @VJSchneid #814 has a fix for the legit use of the old always syntax

[abradd]

In examples like this, assignments to variables in an always block can be necessary. For example, you may want to have a formal-specific counter.

Given that this is for formal verification, using always_* procedures may not be ideal as they are meant for synthesizable code.

sby defines the FORMAL macro. Perhaps the old always syntax could be valid when that macro is defined.

How does slang-tidy handle use of the old always syntax in simulation testbenches? Is the expectation that simulation testbench files will have this rule disabled?