As some proofs involving memories, it is necessary to add more ports to
the queue interface, to sync state. These changes are predicated on the
test environment, so normal use is not affected.
Since some speedup is achieved, use the saved time to test with a deeper
FIFO.
For now, only check that the basic properties work in bounded model check
mode, leave the induction proof for later.
Partially replace the previously existing proof.
Remove earlier assumptions and bounds that don't apply for this proof.
Use parameterized types instead of hard-coded types.
Cesar Strauss