Decouple restoring credits from dequeuing an Rx FIFO

Libraries/GenC/GenCMsg/GenCMsg.bs

@@ -307,19 +307,25 @@ instance (GenCRepr a gcrBytes, GenAllCDecls a, Bits a bBits) =>
     fifo <- mkSizedFIFOF (valueOf bFIFOSize)
     let credits :: Reg (UInt 8)
         credits = head rxCredits
+
+    restoreCredits :: FIFOF ()
+    restoreCredits <- mkFIFOF
 
     let fifo_o = Rx {
       first = fifo.first;
-      deq   = do { credits := credits + 1; fifo.deq };
+      deq   = do { restoreCredits.enq (); fifo.deq };
       notEmpty = fifo.notEmpty;
     }
 
-    let ruleName = "handle_rx_" +++ stringOf name
     let rs =
           rules
-            ruleName: when rxTagEq (valueOf i + 1) ==> do
+            ("handle_rx_" +++ stringOf name): when rxTagEq (valueOf i + 1) ==> do
               fifo.enq (unpackBytes rxBody).fst
               deq
+
+            ("restore_credits_" +++ stringOf name): when True ==> do
+              restoreCredits.deq
+              credits := credits + 1
 
     return (Meta $ Conc fifo_o, rs)
 
@@ -376,10 +382,9 @@ instance (GenCRepr a gcrBytes, GenAllCDecls a, Bits a bBits) =>
     let credits :: Reg (UInt 8)
         credits = head txCredits
 
-    let ruleName = "handle_tx_" +++ stringOf name
     let rs =
           rules
-            ruleName: when credits > 0 ==> do
+            ("handle_tx_" +++ stringOf name): when credits > 0 ==> do
               credits := credits - 1
               enq (fromInteger $ valueOf i + 1) $ packBytes fifo.first
               fifo.deq