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

import Vector
import Util
import FIFO
import FIFOF
import SpecialFIFOs

#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

        -- we really only use tagUsageTracker after emptying out our
        -- `initialTagDistributor` buffer
        tagUsageTracker :: Vector numTags (Reg Bool)
        tagUsageTracker <- 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`.
        initialTagDistributor :: (Reg (Maybe UIntLog2N(numTags)))
        initialTagDistributor <- mkReg |> Just |> reifiedNumTags - 1

        validatedTagToRetire ::  FIFO UIntLog2N(numTags)
        validatedTagToRetire <- mkBypassFIFO

        updateUsageRetireTag ::  RWire UIntLog2N(numTags)
        updateUsageRetireTag <- mkRWire

        updateUsageRequestTag ::  RWire UIntLog2N(numTags)
        updateUsageRequestTag <- mkRWire

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

        debugOnce <- mkReg True

        addRules $
            rules
                "display": when (debugOnce == True) ==>
                    do
                        $display "tagUsageTracker : " (fshow |> readVReg tagUsageTracker)
                        debugOnce := False

                "update_usage_just_retire": when
                                        Just tag <- updateUsageRetireTag.wget,
                                        Nothing  <- updateUsageRequestTag.wget ==>
                    do
                        $display $time " tagUsageTracker after update retire: " (fshow |> readVReg tagUsageTracker)
                        (select tagUsageTracker tag) := False

                "update_usage_just_request": when
                                        Nothing <- updateUsageRetireTag.wget,
                                        Just tag  <- updateUsageRequestTag.wget ==>
                    do
                        $display $time " tagUsageTracker after update request: " (fshow |> readVReg tagUsageTracker)
                        (select tagUsageTracker tag) := True

                "update_usage_request_and_retire": when
                                        Just retireTag  <- updateUsageRetireTag.wget,
                                        Just requestTag <- updateUsageRequestTag.wget ==>
                    do
                        $display $time " tagUsageTracker after update request and retire: " (fshow |> readVReg tagUsageTracker)
                        let
                            tagUsageTrackerInner = readVReg tagUsageTracker
                            tagUsageTracker'  = update tagUsageTrackerInner requestTag True
                            tagUsageTracker'' = update tagUsageTracker' retireTag False
                        writeVReg tagUsageTracker tagUsageTracker''

                "retire_tags": when True ==>
                    do
                        let tagToRetire = validatedTagToRetire.first
                        $display "firing retire_tags" (fshow tagToRetire)
                        validatedTagToRetire.deq
                        tagFIFO.enq tagToRetire
                        updateUsageRetireTag.wset tagToRetire

        return $
          interface TagEngine

            requestTag :: ActionValue UIntLog2N(numTags)
            requestTag =
                do
                    case initialTagDistributor of
                        Just 0 -> do
                            initialTagDistributor := Nothing
                            updateUsageRequestTag.wset 0
                            return 0
                        Just tag -> do
                            initialTagDistributor := Just |> tag - 1
                            updateUsageRequestTag.wset tag
                            return tag
                        Nothing -> do
                            let tag = tagFIFO.first
                            tagFIFO.deq
                            updateUsageRequestTag.wset tag
                            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 tagUsageTracker tag)
                    if (tagValid && tagInUse)
                        then do
                            validatedTagToRetire.enq tag
                        else do
                            action {}