Reincorporate no-sensitive-upgrade check

[dz333]

This requires the assignment analysis from #9 to be fully completed (but the outline of the code can be implemented without it)

The algorithm should be as follows:

For all assignments to sequential variables (i.e. registers), v <= e,:

• If v is definitely assigned in all paths, check L(e) join L(pc) flows to L(next v)
• Else, check the above AND check L(pc) flows to L(v)

[dz333]

This is a sub-issue of #8

[dz333]

The first half of this has been implemented on the erasure branch. the NSU check isn't applied very often since it only is necessary on recursively-typed variable assignments (this only works b/c of the well-formedness assumption that all variables in a dependent type flow to the type in any context -which a different issue #14 is tracking).

[dz333]

The NSU part of the check currently occurs not assuming anything about the context. This can lead to imprecision since we can't accurately know the PC label.

Consider the following:

L(h) = H;
L(r) = PAR(r); // PAR(0) = PAR(1) = L; PAR(2) = PAR(3) = H;
//r may not be assigned, but this is also safe since we never _upgrade_ r; it's already as high as the pc label
if (h== 0 && r == 2) begin
   r <= 3;
end

We would generate the following z3:

(assert (not (and (= h 0) (= r 2)))
(assert (not (leq (join H (LH r)) (LH r_next_))))

However, the second assertion will fail (i.e., get sat). Basically, this is because what we really want is:

Check assertion 1, if sat, then check assertion 2 in its normal context. This isn't really a feature of z3 (i.e., we can't say "if there's a model, do X else do Y") unless we actually use the integrated z3 libraries (which is tracked in #10 - once we finish that we should revisit this imprecision)