* By replacing the goto operator with non-literal parameter
by counting the read enabled with simple VHDL counters we
can now replicate the properties instead of writing them
all out.
* Decrease the data width to decrease run-time of unbounded proofs