From 98f2f5cdfd7886ea3907c48ffa8655cb2331a24f Mon Sep 17 00:00:00 2001 From: Yehowshua Immanuel Date: Fri, 11 Apr 2025 20:35:26 -0400 Subject: [PATCH] having trouble with type constraints around clientIdx --- bs/Bus.bs | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/bs/Bus.bs b/bs/Bus.bs index b9d5b32..3afe1e8 100644 --- a/bs/Bus.bs +++ b/bs/Bus.bs @@ -67,6 +67,9 @@ mkBus serverMap = do selectedClientRequestQueue = (select clientRequestQueues clientIdx) in rules + "rule" : when True ==> do + $display "Bus.bs:71" + (sprintf "request server from client %d" clientIdx): when True ==> do let clientRequest :: TaggedBusRequest inFlightTransactions @@ -75,6 +78,7 @@ mkBus serverMap = do targetAddr :: Addr = busRequestToAddr |> clientRequest.busRequest targetServerIdx :: (Maybe ServerIdx) = serverMap targetAddr -- $display "clientRequest" (fshow clientRequest) + $display "Bus.bs:81" (fshow clientRequest) case targetServerIdx of Just serverIdx -> do let @@ -83,7 +87,20 @@ mkBus serverMap = do arbiterClientSlot :: Arbiter.ArbiterClient_IFC arbiterClientSlot = (select targetServerArbiter.clients clientIdx) arbiterClientSlot.request - Nothing -> do action {} + Nothing -> do + let + idx = fromInteger clientIdx + targetClientResponseArbiter :: Arbiter.Arbiter_IFC numClients + targetClientResponseArbiter = (select responseArbiterByClient idx) + + clientResponseArbiterSlot :: Arbiter.ArbiterClient_IFC + -- arbiters 0 to n-1 are where `n:=numServer` are reserved + -- for servers to make requests to. Arbiter n is reserved for + -- when this rule needs to skip making a request to a server + -- and should instead forward the `BusError UnMapped` response + -- back to the client. Vector.last selects arbiter `n` + clientResponseArbiterSlot = Vector.last targetClientResponseArbiter + clientResponseArbiterSlot.request