From da761f6e4ec6fe3b3f28431919cc6d3cfb0cbaee Mon Sep 17 00:00:00 2001 From: Yehowshua Immanuel Date: Tue, 8 Apr 2025 13:05:34 -0400 Subject: [PATCH 1/5] Type system progress on bus design --- bs/Bus.bs | 13 ++++++++++ bs/BusTypes.bs | 66 ++++++++++++++++++++++++++++++++++++-------------- 2 files changed, 61 insertions(+), 18 deletions(-) diff --git a/bs/Bus.bs b/bs/Bus.bs index 0faaa54..87ca6ff 100644 --- a/bs/Bus.bs +++ b/bs/Bus.bs @@ -3,5 +3,18 @@ package Bus(a) where import Types import BusTypes +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 { } + a :: UInt 5 a = 3 diff --git a/bs/BusTypes.bs b/bs/BusTypes.bs index 99d0fb4..e6943c5 100644 --- a/bs/BusTypes.bs +++ b/bs/BusTypes.bs @@ -1,12 +1,12 @@ package BusTypes( - BusVal(..), - BusError(..), - TransactionSize(..), - ReadRequest(..), - WriteRequest(..) + BusClient(..), BusServer(..), + BusRequest(..), BusResponse(..), + ReadRequest(..), ReadResponse(..), WriteRequest(..), WriteResponse(..), + BusVal(..), BusError(..), TransactionSize(..) ) where import Types +import Vector data BusError = UnMapped @@ -48,21 +48,51 @@ data BusResponse | BusWriteResponse WriteResponse deriving (Bits, Eq, FShow) -interface BusMaster = - -- The Bus arbiter will call the Bus Master's request method - -- if and only if it's the Bus Master's turn to make a request, and the Bus Master - -- has a request to make. - -- It is up to the BusMaster to guard it's request method such that calling - -- it's request method is only valid when the BusMaster has a request to make. - -- This has implications about for the implementor of BusMaster, namely, that it - -- should hold its request until it's request method gets called. - request :: BusRequest - -- From the masters's perspective, the response should not be called by the - -- arbiter until the master is ready to accept the response. In other words, - -- response should be guarded by the client. - response :: BusResponse -> Action +-- # BusClient.dequeueRequest +-- * The Bus arbiter will call the Bus Client's request method if it is +-- the Bus Client's turn to make a request, or if another client forfits +-- its turn. +-- * The BusClient must guard its request method such that calling its +-- request method is only valid when the BusClient has a request to make. +-- * This has implications about for the implementor of BusClient, +-- namely, that it should hold its request until it's request method +-- gets called. The arbiter tags the request so that the client can +-- later correctly correlate the response. +-- * Although the tag is technically passed in as an argument from the +-- arbiter to the client's request method, given that methods are +-- atomic in Bluespec, this is effectively equivalent to tagging the +-- transaction from the client's perspective. Thus, the client must +-- take care to appropiately store the tag. +-- # BusClient.enqueueResponse +-- * From the client's perspective, the response should not be called +-- 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 :: * -> *) transactionTagType = + dequeueRequest :: transactionTagType -> ActionValue BusRequest + enqueueResponse :: (BusResponse, transactionTagType) -> 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 response has been handed off. +-- # BusServer.peekClientTagDestination +-- * The arbiter looks at (peekClientTagDestination :: clientTagTye) 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 :: * -> * -> *) transactionTagType clientTagType = + enqueueRequest :: (transactionTagType, BusRequest) -> Action + dequeueResponse :: ActionValue (clientTagType, BusResponse, transactionTagType) + peekClientTagDestination :: clientTagTye + +interface (Bus :: # -> # -> * -> * -> *) numClients numServers transactionTagType clientTagType = + clients :: Vector numClients (BusClient transactionTagType) + servers :: Vector numServers (BusServer transactionTagType clientTagType) type Token = UInt 5 +type Numeric = 5 a :: UInt 5 a = 3 From fe2fa21fcc57d03477e82ef0bfa9281de8ea1b10 Mon Sep 17 00:00:00 2001 From: Yehowshua Immanuel Date: Tue, 8 Apr 2025 23:04:30 -0400 Subject: [PATCH 2/5] skeletons of Bus module slowly forming --- bs/Bus.bs | 17 ++++++++++++++++- bs/BusTypes.bs | 5 +---- 2 files changed, 17 insertions(+), 5 deletions(-) diff --git a/bs/Bus.bs b/bs/Bus.bs index 87ca6ff..6d648f1 100644 --- a/bs/Bus.bs +++ b/bs/Bus.bs @@ -2,11 +2,16 @@ package Bus(a) where import Types import BusTypes +import TagEngine +import Vector interface (TestType :: * -> *) t = {} -- doSomething :: t -> Action -mkTestType :: (Bits t n, Arith t, Eq t) => Module (TestType t) +mkTestType :: ( + Bits t n, Arith t, Eq t + ) + => Module (TestType t) mkTestType = do return $ interface TestType {} @@ -16,5 +21,15 @@ mkTestTop = do testType <- mkTestType return $ interface Empty { } +mkBus :: Vector numClients (BusClient (UInt (TLog numClients))) + -> Vector numServers (BusServer (UInt (TLog numClients)) clientTagType) + -> Module Empty +mkBus clientVec serverVec = do + tagEngineByClient :: Vector numClients (TagEngine (TLog numClients)) + tagEngineByClient <- replicateM mkTagEngine + + return $ interface Empty { } + + a :: UInt 5 a = 3 diff --git a/bs/BusTypes.bs b/bs/BusTypes.bs index e6943c5..4828668 100644 --- a/bs/BusTypes.bs +++ b/bs/BusTypes.bs @@ -1,4 +1,5 @@ package BusTypes( + Bus(..), BusClient(..), BusServer(..), BusRequest(..), BusResponse(..), ReadRequest(..), ReadResponse(..), WriteRequest(..), WriteResponse(..), @@ -87,10 +88,6 @@ interface (BusServer :: * -> * -> *) transactionTagType clientTagType = dequeueResponse :: ActionValue (clientTagType, BusResponse, transactionTagType) peekClientTagDestination :: clientTagTye -interface (Bus :: # -> # -> * -> * -> *) numClients numServers transactionTagType clientTagType = - clients :: Vector numClients (BusClient transactionTagType) - servers :: Vector numServers (BusServer transactionTagType clientTagType) - type Token = UInt 5 type Numeric = 5 From 989c4e96167174d1704367ec2424e37b1707ab82 Mon Sep 17 00:00:00 2001 From: Yehowshua Immanuel Date: Tue, 8 Apr 2025 23:36:54 -0400 Subject: [PATCH 3/5] Bus types typecheck!!! --- bs/Bus.bs | 6 +++--- bs/BusTypes.bs | 27 ++++++++++++++++++--------- bs/TagEngine.bs | 11 ++++++----- 3 files changed, 27 insertions(+), 17 deletions(-) diff --git a/bs/Bus.bs b/bs/Bus.bs index 6d648f1..318c029 100644 --- a/bs/Bus.bs +++ b/bs/Bus.bs @@ -21,11 +21,11 @@ mkTestTop = do testType <- mkTestType return $ interface Empty { } -mkBus :: Vector numClients (BusClient (UInt (TLog numClients))) - -> Vector numServers (BusServer (UInt (TLog numClients)) clientTagType) +mkBus :: Vector numClients (BusClient inFlightTransactions) + -> Vector numServers (BusServer inFlightTransactions numClients) -> Module Empty mkBus clientVec serverVec = do - tagEngineByClient :: Vector numClients (TagEngine (TLog numClients)) + tagEngineByClient :: Vector numClients (TagEngine inFlightTransactions) tagEngineByClient <- replicateM mkTagEngine return $ interface Empty { } diff --git a/bs/BusTypes.bs b/bs/BusTypes.bs index 4828668..a9a9125 100644 --- a/bs/BusTypes.bs +++ b/bs/BusTypes.bs @@ -1,5 +1,5 @@ package BusTypes( - Bus(..), + ClientTagType, BusClient(..), BusServer(..), BusRequest(..), BusResponse(..), ReadRequest(..), ReadResponse(..), WriteRequest(..), WriteResponse(..), @@ -8,6 +8,9 @@ package BusTypes( import Types import Vector +import TagEngine + +type ClientTagType a = (UInt (TLog a)) data BusError = UnMapped @@ -68,25 +71,31 @@ data BusResponse -- * From the client's perspective, the response should not be called -- 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 :: * -> *) transactionTagType = - dequeueRequest :: transactionTagType -> ActionValue BusRequest - enqueueResponse :: (BusResponse, transactionTagType) -> Action +interface (BusClient :: # -> *) inFlightTransactions = + dequeueRequest :: TagType inFlightTransactions + -> ActionValue BusRequest + enqueueResponse :: (BusResponse, TagType 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 response has been handed off. -- # BusServer.peekClientTagDestination --- * The arbiter looks at (peekClientTagDestination :: clientTagTye) to +-- * The arbiter looks at (peekClientTagDestination :: clientTagType) 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 :: * -> * -> *) transactionTagType clientTagType = - enqueueRequest :: (transactionTagType, BusRequest) -> Action - dequeueResponse :: ActionValue (clientTagType, BusResponse, transactionTagType) - peekClientTagDestination :: clientTagTye +interface (BusServer :: # -> # -> *) inFlightTransactions numClients = + enqueueRequest :: (TagType inFlightTransactions, BusRequest) + -> Action + dequeueResponse :: ActionValue ( + ClientTagType numClients, + BusResponse, transactionTagType + ) + peekClientTagDestination :: clientTagType type Token = UInt 5 type Numeric = 5 diff --git a/bs/TagEngine.bs b/bs/TagEngine.bs index 921e58e..95b0d33 100644 --- a/bs/TagEngine.bs +++ b/bs/TagEngine.bs @@ -1,4 +1,5 @@ package TagEngine( + TagType, TagEngine(..), Util.BasicResult(..), mkTagEngine) where @@ -9,11 +10,11 @@ import FIFO import FIFOF import SpecialFIFOs -#define UIntLog2N(n) (UInt (TLog n)) +type TagType a = (UInt (TLog a)) interface (TagEngine :: # -> *) numTags = - requestTag :: ActionValue UIntLog2N(numTags) - retireTag :: UIntLog2N(numTags) -> Action + requestTag :: ActionValue (TagType numTags) + retireTag :: (TagType 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 @@ -79,7 +80,7 @@ mkTagEngine = do -- Interface return $ interface TagEngine - requestTag :: ActionValue UIntLog2N(numTags) + requestTag :: ActionValue (TagType numTags) requestTag = do case initialTagDistributor of Just 0 -> do @@ -100,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 :: UIntLog2N(numTags) -> Action + retireTag :: (TagType numTags) -> Action retireTag tag = do let From b4c7537a8542fdb2e9d67cf52c76167e9c231ef4 Mon Sep 17 00:00:00 2001 From: Yehowshua Immanuel Date: Wed, 9 Apr 2025 01:08:42 -0400 Subject: [PATCH 4/5] things still typecheck --- bs/Bus.bs | 34 ++++++++++++++-------------------- bs/BusTypes.bs | 24 +++++++++--------------- bs/TagEngine.bs | 16 ++++++++-------- 3 files changed, 31 insertions(+), 43 deletions(-) diff --git a/bs/Bus.bs b/bs/Bus.bs index 318c029..b554ba1 100644 --- a/bs/Bus.bs +++ b/bs/Bus.bs @@ -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 diff --git a/bs/BusTypes.bs b/bs/BusTypes.bs index a9a9125..818fd3d 100644 --- a/bs/BusTypes.bs +++ b/bs/BusTypes.bs @@ -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 diff --git a/bs/TagEngine.bs b/bs/TagEngine.bs index 95b0d33..2ddb304 100644 --- a/bs/TagEngine.bs +++ b/bs/TagEngine.bs @@ -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 From 076d3aed4367a48aad3cf2d4f297908707223cfa Mon Sep 17 00:00:00 2001 From: Yehowshua Immanuel Date: Wed, 9 Apr 2025 20:58:13 -0400 Subject: [PATCH 5/5] shoudl probably rethink approach... --- bs/Bus.bs | 52 ++++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 44 insertions(+), 8 deletions(-) diff --git a/bs/Bus.bs b/bs/Bus.bs index b554ba1..7df4955 100644 --- a/bs/Bus.bs +++ b/bs/Bus.bs @@ -10,20 +10,56 @@ import Arbiter clientRequest :: Arbiter.ArbiterClient_IFC -> Action clientRequest ifc = ifc.request -mkBus :: Vector numClients (BusClient inFlightTransactions) +busRequestToAddr :: BusRequest -> Addr +busRequestToAddr req = case req of + BusReadRequest (ReadRequest addr _) -> addr + WriteReadRequest (WriteRequest addr _) -> addr + +mkBus :: (Addr -> Integer) + -> Vector numClients (BusClient inFlightTransactions) -> Vector numServers (BusServer inFlightTransactions numClients) -> Module Empty -mkBus clientVec serverVec = do - tagEngineByClient :: Vector numClients (TagEngine inFlightTransactions) - tagEngineByClient <- replicateM mkTagEngine +mkBus addrToServerTranslation clientVec serverVec = do + tagEngineByClientVec :: Vector numClients (TagEngine inFlightTransactions) + tagEngineByClientVec <- replicateM mkTagEngine - arbiterByServer :: Vector numServers (Arbiter_IFC numClients) - arbiterByServer <- replicateM (mkArbiter False) + arbiterByServerVec :: Vector numServers (Arbiter_IFC numClients) + arbiterByServerVec <- replicateM (mkArbiter False) + + -- statically determinate criteria + let + clientIdx :: Integer = 0 + selectedClient ::(BusClient inFlightTransactions) + selectedClient = (select clientVec clientIdx) + selectedTagEngine = (select tagEngineByClientVec clientIdx) addRules |> rules "placeholder rule": when True ==> do - let selectedArbiter = (select arbiterByServer 0) - mapM_ clientRequest selectedArbiter.clients + let selectedServerArbiter = (select arbiterByServerVec 0) + mapM_ clientRequest selectedServerArbiter.clients + + "connect request client 0": + when True + ==> do + tag <- selectedTagEngine.requestTag + + busRequest :: BusRequest + busRequest <- selectedClient.dequeueRequest tag + + -- let + -- addr = busRequestToAddr busRequest + -- targetServerIdx = addrToServerTranslation addr + -- targetServer = (select serverVec targetServerIdx) + -- targetServerArbiter = (select arbiterByServerVec targetServerIdx) + + -- targetServerArbiter.request + + -- if targetServerArbiter.grant + -- then targetServer.enqueueRequest (tag, busRequest) + -- else action {} + + -- targetServer + action {} return $ interface Empty { }