package TagEngine(
    TagEngine(..),
    Util.BasicResult(..),
    mkTagEngine) where

import Vector
import Util
import FIFO
import FIFOF

#define UIntLog2N(n) (UInt (TLog n))

interface (TagEngine :: # -> *) numTags =
    requestTag :: ActionValue UIntLog2N(numTags)
    retireTag  :: UIntLog2N(numTags) -> Action

-- The tag engine returns a tag that is unique for the duration of
-- the lifetime of the tag. Useful when you need to tag transactions
-- on a bus for example.
-- This implementation is FIFO based.
mkTagEngine :: Module (TagEngine numTags)
mkTagEngine =
    do
        let reifiedNumTags = fromInteger |> valueOf numTags

        inUseVec :: Vector numTags (Reg Bool)
        inUseVec <- replicateM |> mkReg False

        -- Since Bluespec doesn't allow us to initialize FIFOs with values at
        -- reset, we can pretend as if the buffer within our tagFIFO is populated
        -- with sequentially incrementing values(starting from 0) on reset
        -- by having our tag engine effectively return the value of a decrementing
        -- counter initialized to (numTags - 1) for the first n tag requests made 
        -- to TagEngine where `n := numTags`.
        resetTagCounter :: (Reg (Maybe UIntLog2N(numTags)))
        resetTagCounter <- mkReg |> Just |> reifiedNumTags - 1

        retireQueue ::  FIFOF UIntLog2N(numTags)
        retireQueue <- mkSizedFIFOF reifiedNumTags

        freeQueue ::  FIFOF UIntLog2N(numTags)
        freeQueue <- mkSizedFIFOF reifiedNumTags

        debugOnce <- mkReg True

        addRules $
            rules
                "display": when (debugOnce == True) ==>
                    do
                        $display "inUseVec : " (fshow |> readVReg inUseVec)
                        debugOnce := False
            
                -- The "retire_tags" rule can't fire when the `requestTag` method is called.
                -- In practice, this is Ok since:
                --    1. the `requestTag` method should take priority over the "retire_tags" rule
                --    2. the `requestTag` method handles the case where there are some tags to retire.
                "retire_tags": when True ==>
                    do
                        let tag = retireQueue.first
                        $display "firing retire_tags" (fshow tag)
                        retireQueue.deq
                        freeQueue.enq tag
                        (select inUseVec tag) := False

        return $
          interface TagEngine

            requestTag :: ActionValue UIntLog2N(numTags)
            requestTag =
                do
                    case resetTagCounter of
                        Just 0 -> do
                            resetTagCounter := Nothing
                            (select inUseVec 0) := True
                            return 0
                        Just tag -> do
                            resetTagCounter := Just |> tag - 1
                            (select inUseVec tag) := True
                            return tag
                        Nothing -> do
                            let tag = freeQueue.first
                            freeQueue.deq
                            return tag

            -- `retireTag` isn't guarded on tag validity(this would break Bluespec's safety model) 
            -- so it is advisable that the caller of `retireTag` only attempt to retire valid tags.
            -- Internally, the tagEngine will keep a correct and consistent state since TagEngine
            -- validates tags before attempting to retire them.
            retireTag :: UIntLog2N(numTags) -> Action
            retireTag tag =
                do
                    let
                        tagValid = tag < reifiedNumTags
                        tagInUse = readReg (select inUseVec tag)
                    if (tagValid && tagInUse)
                        then do
                            retireQueue.enq tag
                        else do
                            action {}