Arbiter of the AMBA AHB bus, simplified from the specification of R. Bloem,
S. Galler, B. Jobstmann, N. Piterman, A. Pnueli, and M. Weiglhofer,
"Specify, Compile, Run: Hardware from PSL" (COCV 2007, ENTCS 190(4)), after
the AMBA specification of ARM (rev. 2.0). Two masters ask for the bus; the
arbiter gives it to one of them. A master can lock the bus: the arbiter then
lets it keep the bus while it asks for it. The simplification: two masters,
no bursts, no HREADY, and the master that has the grant is the one that has
the bus.

Variables
    hbusreq1, hbusreq2  master 1 or 2 asks for the bus (environment)
    hlock1, hlock2      master 1 or 2 asks for a locked access (environment)
    hgrant1, hgrant2    the bus is given to master 1 or 2 (arbiter)
    hmastlock           the master that has the bus has locked it (arbiter)

The requirements are written as two viewpoints of the same arbiter, in
SystemVerilog Assertions (sva/grant.sv, sva/lock.sv); the labels of the
assertions are the numbers below, with _ for the dot.

Grant
    GR1     Master 1 has the bus at the start (the default master).
    GR2     The bus is given to exactly one master.
    GR3.1   Master 1 does not wait forever: infinitely often it does not
            ask, or it has the bus (G9 of Bloem et al.).
    GR3.2   The same for master 2.

Lock
    LA1.1   Master 1 asks for the bus when it asks for a locked access (A3
            of Bloem et al.).
    LA1.2   The same for master 2.
    LA2     A master that has locked the bus stops asking for it sooner or
            later (A1 of Bloem et al.).
    LK1     The bus is locked when its master asks for a locked access.
    LK2.1   While master 1 has locked the bus and asks for it, it keeps the
            bus (G2 of Bloem et al.).
    LK2.2   The same for master 2.
