things still typecheck

This commit is contained in:
Yehowshua Immanuel 2025-04-09 01:08:42 -04:00
parent 989c4e9616
commit b4c7537a85
3 changed files with 31 additions and 43 deletions

View file

@ -1,25 +1,14 @@
package Bus(a) where
package Bus(mkBus) where
import Types
import BusTypes
import TagEngine
import Vector
import Util
import Arbiter
interface (TestType :: * -> *) t = {}
-- doSomething :: t -> Action
mkTestType :: (
Bits t n, Arith t, Eq t
)
=> Module (TestType t)
mkTestType = do
return $ interface TestType {}
mkTestTop :: Module Empty
mkTestTop = do
testType :: TestType (UInt 5)
testType <- mkTestType
return $ interface Empty { }
clientRequest :: Arbiter.ArbiterClient_IFC -> Action
clientRequest ifc = ifc.request
mkBus :: Vector numClients (BusClient inFlightTransactions)
-> Vector numServers (BusServer inFlightTransactions numClients)
@ -28,8 +17,13 @@ mkBus clientVec serverVec = do
tagEngineByClient :: Vector numClients (TagEngine inFlightTransactions)
tagEngineByClient <- replicateM mkTagEngine
arbiterByServer :: Vector numServers (Arbiter_IFC numClients)
arbiterByServer <- replicateM (mkArbiter False)
addRules |>
rules
"placeholder rule": when True ==> do
let selectedArbiter = (select arbiterByServer 0)
mapM_ clientRequest selectedArbiter.clients
return $ interface Empty { }
a :: UInt 5
a = 3

View file

@ -1,5 +1,5 @@
package BusTypes(
ClientTagType,
MkClientTagType,
BusClient(..), BusServer(..),
BusRequest(..), BusResponse(..),
ReadRequest(..), ReadResponse(..), WriteRequest(..), WriteResponse(..),
@ -10,7 +10,7 @@ import Types
import Vector
import TagEngine
type ClientTagType a = (UInt (TLog a))
type MkClientTagType a = (UInt (TLog a))
data BusError
= UnMapped
@ -72,33 +72,27 @@ data BusResponse
-- by the arbiter until the client is ready to accept the response.
-- In other words, the response method should be guarded by the client.
interface (BusClient :: # -> *) inFlightTransactions =
dequeueRequest :: TagType inFlightTransactions
dequeueRequest :: MkTagType inFlightTransactions
-> ActionValue BusRequest
enqueueResponse :: (BusResponse, TagType inFlightTransactions)
enqueueResponse :: (BusResponse, MkTagType inFlightTransactions)
-> Action
-- # BusServer.dequeueResponse
-- * If the arbiter is able to successfully call `dequeueResponse`, then
-- the BusServer's internal logici must update such that it understand
-- the BusServer's internal logic must update such that it understands
-- the response has been handed off.
-- # BusServer.peekClientTagDestination
-- * The arbiter looks at (peekClientTagDestination :: clientTagType) to
-- * The arbiter looks at (peekClientTagDestination :: MkClientTagType) to
-- determine whether or not it is currently safe whether to dequeue the
-- response as well as where to route the response should it dequeue the
-- response.
-- * `peekClientTagDestination` should be guarded on whether or not there is
-- a valid response available.
interface (BusServer :: # -> # -> *) inFlightTransactions numClients =
enqueueRequest :: (TagType inFlightTransactions, BusRequest)
enqueueRequest :: (MkTagType inFlightTransactions, BusRequest)
-> Action
dequeueResponse :: ActionValue (
ClientTagType numClients,
MkClientTagType numClients,
BusResponse, transactionTagType
)
peekClientTagDestination :: clientTagType
type Token = UInt 5
type Numeric = 5
a :: UInt 5
a = 3
peekClientTagDestination :: MkClientTagType numClients

View file

@ -1,5 +1,5 @@
package TagEngine(
TagType,
MkTagType,
TagEngine(..),
Util.BasicResult(..),
mkTagEngine) where
@ -10,11 +10,11 @@ import FIFO
import FIFOF
import SpecialFIFOs
type TagType a = (UInt (TLog a))
type MkTagType numTags = (UInt (TLog numTags))
interface (TagEngine :: # -> *) numTags =
requestTag :: ActionValue (TagType numTags)
retireTag :: (TagType numTags) -> Action
requestTag :: ActionValue (MkTagType numTags)
retireTag :: (MkTagType 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
@ -45,7 +45,7 @@ mkTagEngine = do
debugOnce <- mkReg True
-- Rules
addRules $
addRules |>
rules
"debug_initial_state": when debugOnce ==> do
$display "tagUsage: " (fshow (readVReg tagUsage))
@ -78,9 +78,9 @@ mkTagEngine = do
(Nothing, Nothing) -> action {}
-- Interface
return $
return |>
interface TagEngine
requestTag :: ActionValue (TagType numTags)
requestTag :: ActionValue (MkTagType numTags)
requestTag = do
case initialTagDistributor of
Just 0 -> do
@ -101,7 +101,7 @@ mkTagEngine = do
-- 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 :: (TagType numTags) -> Action
retireTag :: (MkTagType numTags) -> Action
retireTag tag =
do
let