alternate approach not so successful

* clean up state machine in Top
 * `requestTag` method now emits Maybe type
 * put more thought into comments around asynchronous bus

Makefile

@@ -61,7 +61,7 @@ $(BDPI_OBJ): $(BDPI_SRC)
 
 BSC_LINK_FLAGS += -keep-fires
 
-BSC_PATHS = -p bs/:bsv/:+
+BSC_PATHS = -p bs/:bs/Tests/:bsv/:+
 
 .PHONY: help
 help:

README.md

@@ -1,25 +1,17 @@
-# RISC-V Bluespec Classic
+# MannaChip
 
 ## Introduction:
+Manna was the miraculous food provided by God requiring no effort on behalf of the Israelites. In a similar vein, the POWER3.0 compliant MannaChip 
+processor delivers groundbreaking performance, necessitating minimal intervention on the developer's or user's part.
 
-The beginnings of an implementation of a Linux capable RISCV processor in Bluespec
-Haskell. Here, we plan to take full advantage of the Haskell type system embedded
-in Bluespec Haskell. Given that the Bluespec semantics are inspired by TLA+ which
-is different from traditional Haskell semantics, we're doing functional design
-exploration first in [Haskell](https://git.joyofhardware.com/Yehowshua/RiscV-Formal)
-and iteratively transforming it into Bluespec. Most of the Haskell code is valid
-Bluespec, we merely need to partition the functional Haskell definition of a CPU into
-atomic actions/transactions that can be resolved and scheduled across time.
+Just as "man does not live by bread alone, but by every word that proceeds from the mouth of God," this chip thrives on every instruction word you provide. It's not just about raw computational power, but the synergy between user input and hardware optimization.
+
+``TOPMODULE=mkTop make v_compile`` to generate verilog. The generated verilog can
+be found in the ``verilog_RTL/`` folder.
 
 # Status
- * Basic peripheral working on FPGA such as UART and
-   BRAM(work on this is out of tree - need to merge)
- * Much of the grunt-work for a functional definition of RV64i already
-   [exists](https://git.joyofhardware.com/Yehowshua/RiscV-Formal/src/branch/main/hs)
-   and some porting work has been done offline
- * I've begun the implementation of an asynchronous bus that supports tagged
-   transactions using a Free List based stack.
-
+Admittedly, not very far. Perhaps one could say we've got the beginnings 
+of what would make for LED and UART controllers.
 
 # Dependencies
 ## Linux
@@ -73,4 +65,4 @@ TOPMODULE=mkTop make v_compile
       - [ ] try to optimize decoder
 
 # Notable Reference Files
-``/Users/yehowshuaimmanuel/git/bsc/testsuite/bsc.bsv_examples/cpu/FiveStageCPUQ3sol.bsv``
+``/Users/yehowshuaimmanuel/git/bsc/testsuite/bsc.bsv_examples/cpu/FiveStageCPUQ3sol.bsv``

bs/BusTypes.bs

@@ -57,9 +57,9 @@ interface BusMaster =
   -- 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 until
-  -- the client is ready to accept the response. In other words, response
-  -- should be guarded by the client.
+  -- 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
 
 type Token = UInt 5

bs/TagEngine.bs

@@ -9,7 +9,7 @@ import Util
 #define UIntLog2N(n) (UInt (TLog n))
 
 interface (TagEngine :: # -> *) numTags =
-    requestTag :: ActionValue UIntLog2N(numTags)
+    requestTag :: ActionValue (Maybe UIntLog2N(numTags))
     retireTag  :: UIntLog2N(numTags) -> ActionValue BasicResult
 
 -- The tag engine returns a tag that is unique for the duration of
@@ -19,6 +19,7 @@ interface (TagEngine :: # -> *) numTags =
 mkTagEngine :: Module (TagEngine numTags)
 mkTagEngine =
     do
+
         let reifiedNumTags = fromInteger |> valueOf numTags
 
         freeStackVec :: Vector numTags (Reg UIntLog2N(numTags))
@@ -30,6 +31,16 @@ mkTagEngine =
         stackPtr :: (Reg (Maybe(UIntLog2N(numTags))))
         stackPtr <- mkReg |> Just |> reifiedNumTags - 1
 
+        methodRequestTagCalled :: PulseWire
+        methodRequestTagCalled <- mkPulseWire
+
+        methodRetireTagCalledValid :: RWire UIntLog2N(numTags)
+        methodRetireTagCalledValid <- mkUnsafeRWire
+        -- methodRetireTagCalledValid <- mkRWireSBR
+
+        computedTagResult :: Wire (Maybe UIntLog2N(numTags))
+        computedTagResult <- mkBypassWire
+
         debugOnce <- mkReg True
 
         addRules $
@@ -41,41 +52,76 @@ mkTagEngine =
                         $display "stackPtr : " (fshow stackPtr)
                         debugOnce := False
 
-        counter <- mkReg(0 :: UIntLog2N(numTags))
+                "update stack pointer": when True ==>
+                    do
+                        stackPtr :=
+                            case (methodRequestTagCalled, methodRetireTagCalledValid.wget) of
+                                (True, Just _) -> stackPtr
+                                (True, Nothing) ->
+                                    case stackPtr of
+                                        Just 0 -> Nothing
+                                        Just sampledStackPtr -> Just |> sampledStackPtr - 1
+                                        Nothing -> Nothing
+                                (False, Just _) ->
+                                    case stackPtr of
+                                        Just sampledStackPtr -> Just |> sampledStackPtr + 1
+                                        Nothing -> Nothing
+                                (False, Nothing) -> stackPtr
+
+                "update free stack": when True ==>
+                    do
+                        case (methodRequestTagCalled, methodRetireTagCalledValid.wget) of
+                            (True, Just _) -> do action {}
+                            (True, Nothing) -> do action {}
+                            (False, Just tag) -> do
+                                case stackPtr of
+                                    Just sampledStackPtr -> do
+                                        (select freeStackVec (sampledStackPtr + 1)) := tag
+                                    Nothing -> do
+                                        (select freeStackVec 0) := tag
+                            (False, Nothing) -> do action {}
+
+                "update in use": when True ==>
+                    do
+                        case (methodRequestTagCalled, methodRetireTagCalledValid.wget) of
+                            (True, Just _) -> do action {}
+                            (True, Nothing) ->
+                                case stackPtr of
+                                    Just sampledStackPtr -> do
+                                        (select inUseVec sampledStackPtr) := True
+                                    Nothing -> do action {}
+                            (False, Just tag) -> do
+                                (select inUseVec tag) := False
+                            (False, Nothing) -> do action {}
+
+                "compute tag": when True ==>
+                    computedTagResult :=
+                        case methodRetireTagCalledValid.wget of
+                            Just tag -> Just tag
+                            Nothing ->
+                                case stackPtr of
+                                    Just sampledStackPtr ->
+                                        Just |> readReg (select freeStackVec sampledStackPtr)
+                                    Nothing -> Nothing
+
         return $
           interface TagEngine
 
-            requestTag :: ActionValue UIntLog2N(numTags)
+            requestTag :: ActionValue (Maybe UIntLog2N(numTags))
             requestTag =
                 do
-                    stackPtr :=
-                        if sampledStackPtr == 0
-                            then Nothing
-                            else Just |> sampledStackPtr - 1
-                    (select inUseVec sampledStackPtr) := True
-                    return |> readReg (select freeStackVec sampledStackPtr)
-                when
-                    Just sampledStackPtr <- stackPtr
+                    methodRequestTagCalled.send
+                    return computedTagResult
 
-            -- retireTag isn't guarded so its up to external module to only attempt to
-            -- retire valid tags... At any rate, we can notify the requestor of failures
-            -- to retire tags - although the requestor can merely ignore this
-            -- notification.
             retireTag :: UIntLog2N(numTags) -> ActionValue BasicResult
             retireTag tag =
                 do
                     let
                         tagValid = tag < reifiedNumTags
                         tagInUse = readReg (select inUseVec tag)
-                        nextStackPtrUint =
-                            case stackPtr of
-                                Nothing -> 0
-                                Just n -> n + 1
                     if (tagValid && tagInUse)
                         then do
-                            (select inUseVec tag) := False
-                            (select freeStackVec nextStackPtrUint) := tag
-                            stackPtr := Just nextStackPtrUint
+                            methodRetireTagCalledValid.wset tag
                             return Success
                         else do
                             return Failure

bs/Tests/TagEngineTester.bs

@@ -0,0 +1,53 @@
+package TagEngineTester(mkTagEngineTester) where
+
+import TagEngine
+import ActionSeq
+
+mkTagEngineTester :: Module Empty
+mkTagEngineTester = do
+  tagEngine :: TagEngine 5 <- mkTagEngine
+  count            :: Reg (UInt 4) <- mkReg 0;
+  runOnce :: Reg Bool <- mkReg False
+
+  s :: ActionSeq
+  s <- 
+    let
+      requestTagAction :: Action
+      requestTagAction =
+        do
+          tag <- tagEngine.requestTag
+          $display "got tag : " (fshow tag)
+
+      retireTagAction :: UInt 3 -> Action
+      retireTagAction tag =
+        do
+          res <- tagEngine.retireTag tag
+          $display "retiring tag : " (fshow tag) " " (fshow res)
+          action {}
+
+    in
+      actionSeq $
+      do requestTagAction
+      |> do requestTagAction
+      |> do requestTagAction
+      |> do retireTagAction 3
+      |> do $display "BEGIN TRY SIMULTANEOUS RETIRE and REQUEST"
+      |> do 
+          retireTagAction 4
+          requestTagAction
+      |> do $display "END TRY SIMULTANEOUS RETIRE and REQUEST"
+      |> do requestTagAction
+      |> do retireTagAction 4
+      |> do retireTagAction 4
+      |> do retireTagAction 0
+      |> do requestTagAction
+      |> do requestTagAction
+      |> do retireTagAction 1
+      |> do requestTagAction
+
+  addRules $
+    rules
+      "testIncrement": when (runOnce == False) ==>
+        do
+          s.start
+          runOnce := True

bs/Top.bs

@@ -10,6 +10,8 @@ import TagEngine
 import List
 import ActionSeq
 
+import TagEngineTester
+
 type FCLK = 25000000
 type BAUD = 9600
 
@@ -66,8 +68,6 @@ mkTop = do
 
   bus          :: Bus <- mkBus
   busClient    :: BusClient <- mkBusClient
-  let a :: List Integer = 1 :> 2 :> Nil
-      b = length a
 
   persistLed  :: Reg (Bit 8) <- mkReg 0
   messageM $ "Hallo!!" + (realToString 5)
@@ -100,58 +100,12 @@ mkTop = do
 
 mkSim :: Module Empty
 mkSim = do
-  let cfg          :: BRAM_Configure = defaultValue
-
-  tagEngine :: TagEngine 5 <- mkTagEngine
-  count            :: Reg (UInt 4) <- mkReg 0;
+  _ :: Empty <- mkTagEngineTester
   initCFunctions :: Reg Bool <- mkReg False;
   core             :: Core FCLK <- mkCore;
 
-  s :: ActionSeq
-  s <- actionSeq
-    $  do
-         $display "got tag : " tagEngine.requestTag
-    |> do
-         $display "got tag : " tagEngine.requestTag
-    |> do
-         $display "got tag : " tagEngine.requestTag
-    |> do
-         res <- tagEngine.retireTag 3
-         $display "retiring tag :   3 " (fshow res)
-         action {}
-    |> do
-         $display "got tag : " tagEngine.requestTag
-    |> do
-         $display "got tag : " tagEngine.requestTag
-    |> do
-         res <- tagEngine.retireTag 4
-         $display "retiring tag :   4 " (fshow res)
-         action {}
-    |> do
-         res <- tagEngine.retireTag 4
-         $display "retiring tag :   4 " (fshow res)
-         action {}
-    |> do
-         res <- tagEngine.retireTag 0
-         $display "retiring tag :   0 " (fshow res)
-         action {}
-    |> do
-         $display "got tag : " tagEngine.requestTag
-    |> do
-         $display "got tag : " tagEngine.requestTag
-    |> do
-         res <- tagEngine.retireTag 1
-         $display "retiring tag :   1 " (fshow res)
-         action {}
-    |> do
-         $display "got tag : " tagEngine.requestTag
-
   addRules $
     rules
-      "testIncrement": when (count < 10) ==>
-        do
-          count := count + 1
-          s.start
       "initCFunctionsOnce":  when not initCFunctions ==>
         do
           initTerminal