Verilog: arrays of module instances

[kroening]

Summary

This adds support for arrays of module instances (IEEE 1800-2017 23.3.2), including multi-dimensional ones.

• Elaboration creates one module instance symbol per array element (e.g., s[3]...s[0] for sub s[3:0](...)), plus a symbol for the array itself, which is used to resolve hierarchical references into the elements.
• During parameterization, an instance array is expanded into one instance per element, each with its own parameterized module, so that synthesis needs no special handling. defparam onto individual elements works via the element identifiers.
• Port connections are split per 1800-2017 23.3.3:
  • a connection that matches the port connects to every element;
  • a wider vector connection whose width is the port width times the number of elements is split bit-wise, with the most significant bits going to the element with the leftmost index;
  • unpacked array connections whose outer dimensions match the instance array dimensions are split element-wise (23.3.3.5);
  • anything else yields a type-checking error.
• Hierarchical references into instance array elements (my_instance[1].i, c[1][2].o) are resolved by the type checker, including multi-dimensional selects.

Test plan

• regression/verilog/modules/instance_array1: multi-dimensional instance array with element-wise unpacked connections (was a rejection test, now CORE with properties)
• regression/verilog/modules/instance_array2: bit-wise splitting with [8:1] range and hierarchical references (was KNOWNBUG, now CORE)
• regression/verilog/modules/instance_array3 (new): named port connections, replication, and bit-wise splitting of a wide connection
• regression/verilog/modules/instance_array4 (new): error for connections that cannot be split
• All verilog, ebmc, smv and vlindex regression tests pass; unit tests pass