Formal protocol checking for icache <-> core interface

This turns out to be quite complicated, because the icache has a lot
of different counters that all track addresses or fill buffer state.
For an inductive proof to go through, you need to make the relations
between them explicit, which takes lots of assertions.

All of the signals defined in the formal_tb are prefixed with 'f_'.
This isn't strictly necessary, but it makes it much easier to see what
came from the design (since we are "bound in", our ports don't have _o
or _i suffixes).

We add a couple of protocol assumptions:

ICache <-> Core:

  - Branch target addresses are half-word aligned
  - The branch_spec signal is driven if branch is

ICache <-> Memory:

  - The bus doesn't respond unless there is an outstanding request
  - The bus doesn't grant more than 4 billion outstanding requests(!)

There's also some protocol state tracking:

  - f_addr_valid tracks whether the ICache currently has an
    architectural address. It goes high with branch_i (which gives the
    cache an address) and goes low when the cache completes a
    transaction with err_o set (since the data is bad, there's no
    notion of a "next address").

  - f_reqs_on_bus tracks the number of requests currently outstanding
    on the bus. This is used for the ICache <-> Memory assumptions
    above. We have some internal assertions that check this equals the
    sum of the "ext" counters minus the sum of the "rvd" counters.

With these assumptions, we can prove:

  - Once asserted, valid_o stays high until a transaction is completed
    by ready_i or until branch_i is asserted (which cancels the
    transaction).

  - While the transaction is pending, addr_o remains stable.

  - While the transaction is pending, err_o remains stable and, if
    err_o is asserted, so does err_plus2_o.

  - While the transaction is pending, if err_o and err_plus2_o are
    high then bottom 16 bits of the returned instruction data imply an
    uncompressed instruction.

  - While the transaction is pending, if err_o is low then the bottom
    16 bits of the returned instruction remain stable.

  - While the transaction is pending, if err_o is low and the bottom
    16 bits of the returned instruction imply an uncompressed
    instruction then the top 16 bits of the returned instruction
    remain stable.