Verification Primer

• ImProve Home

Arbiter Verification

In this example we will design and verify a simple arbiter. As inputs, the arbiter will take in requests from some three devices competing for a shared resource, and the the arbiter will output three booleans signals telling each device whether they have been granted the resource:

-- Input requests.
requestA = input bool ["requestA"]
requestB = input bool ["requestB"]
requestC = input bool ["requestC"]

-- Output variables.
grantA = global bool ["grantA"] False
grantB = global bool ["grantB"] False
grantC = global bool ["grantC"] False

-- Some helpers to reference of the output variables expressions.
grantA' = ref grantA
grantB' = ref grantB
grantC' = ref grantC

Some properties we would like the arbiter to adhere too include:

• At most, only one request is granted at a time.
• If a grant is issued, correspond device must me making a request.
• If any request is raised, a grant must be made.

Based on these requirements we can formulate an ImProve specification:

arbiterSpecification :: Stmt ()
arbiterSpecification = do
  -- Only one request is granted at a time.
  theorem "at most one grant" 1 [] $ not_ grantA' &&. not_ grantB' &&. not_ grantC'
                                 ||.      grantA' &&. not_ grantB' &&. not_ grantC'
                                 ||. not_ grantA' &&.      grantB' &&. not_ grantC'
                                 ||. not_ grantA' &&. not_ grantB' &&.      grantC'

  -- A grant must correspond to a request.
  theorem "grant implies request A" 1 [] $ grantA' --> requestA
  theorem "grant implies request B" 1 [] $ grantB' --> requestB
  theorem "grant implies request C" 1 [] $ grantC' --> requestC

  -- Any request implies a grant.
  theorem "any request implies a grant" 2 [] $ (requestA ||. requestB ||. requestC) --> (grantA' ||. grantB' ||. grantC')

  return ()