Better Support for Modular Typechecking

[dz333]

Currently, when typechecking dependent labels we rely on inspecting conditional checks to generate z3 constraints to prove data flows are safe.

However, sometimes these invariants are established in a different firrtl Module
For example, if Module B requires an invariant established by Module A, then we cannot modularly typecheck Module B. We need to elaborate the entire circuit which contains both of these modules and typecheck that.

This can lead to performance problems with the compiler since larger circuits generate more complicated z3 constraints; they also can lead to inefficient in memory representations of the circuit. By modularizing, we can improve performance by presenting simpler constraints to the solver and reducing the compiler's memory requirements.

One way to establish this would be to add preconditions and postconditions to modules which specify relationships about the modules inputs and outputs, respectively. Furthermore, we could add inference to the compiler which generates weakest preconditions and strongest postconditions for you.