Support for SVA Local Variables

[dh73]

Using local variables in properties causes a Verific error such as the following one:

• Current result: Verific is not able to elaborate the design.
  base: ERROR: Verific SVA primitive sva_match_item_trigger (i30) is currently unsupported in this context at <source_file>.<line>

• Expected result: The property should pass.
  The property "sva_local.ap_check_datapath" was proven in X s.

Local variables are powerful SVA constructs that helps reduce the need of helper logic (auxiliar FSMs and other supporting logic).
Consider the example property using local variables, attached in this issue for a simple PISO register:

   /* The local variables idx and data_i                                                                                                                                                                           
    * are used to store the data at the output, and reconstruct                                                                                                                                                    
    * the value in the data_i register, to check datapath value */
   property check_val;
      logic [$bits(data)-1:0] idx;
      logic [7:0] data_i;
      (load, idx = 0) |-> ##1 (!load, data_i[idx]=data_out, idx++)[*8] ##1 data_i == data;
   endproperty

Both idx and data_i local variables store certain values for late evaluation. In this specific case, the assertion assembles by itself the value to check after 8 clock cycles, instead of using explicit helper logic.

• Test case:
  sva_local_variables.gz

[mmicko]

At least some better error message is now displayed by YosysHQ/yosys@4470510
Implementing this feature would require some major rework to support.