ethoc: modelling asynchronuous hardware access using concurrency
ethoc: added missing include
ethoc: work around CBMC bug

CBMC builds an endianness map; the code doing so does not properly handle bit
fields smaller than 1 byte
ethoc: model downsizing

- Number of descriptors changed to 8, handled via macro
- No more than 6 registers in Mii
ethoc: further model downsizing

- Change transmit buffer array size to 16
- Permit excluding Mii write functions via defines
ethoc hardware model test: manual unwinding, disable assertion

- CBMC presently cannot handle pointers cast to integers and back again, thus
  the packet contents inspection fails
- Unwind the zero initialisation to otherwise permit an analysis using small
  loop bounds
ethoc test: added preprocessor guards around each test
ethoc: replacing loops by assumes where possible
ethoc: downsizing the software model