Make make fpga work

`ERROR: IO 'ftdi_txd_1' is unconstrained in LPF (override this error with --lpf-allow-unconstrained)`

README.md

@@ -1,17 +1,25 @@
-# MannaChip
+# RISC-V Bluespec Classic
 
 ## 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.
 
-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.
+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.
 
 # Status
-Admittedly, not very far. Perhaps one could say we've got the beginnings
-of what would make for LED and UART controllers.
+ * 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.
+
 
 # Dependencies
 ## Linux
@@ -65,4 +73,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/TagEngine.bs

@@ -1,10 +1,81 @@
-package TagEngine() where
+package TagEngine(
+    TagEngine(..),
+    Util.BasicResult(..),
+    mkTagEngine) where
 
+import Vector
 import Util
 
-interface (TagEngine :: # -> *) numTags =
-    requestTag :: ActionValue (UInt (TLog numTags))
-    retireTag  :: UInt (TLog numTags) -> Action
+#define UIntLog2N(n) (UInt (TLog n))
 
-a :: Integer
-a = 3
+interface (TagEngine :: # -> *) numTags =
+    requestTag :: ActionValue UIntLog2N(numTags)
+    retireTag  :: UIntLog2N(numTags) -> ActionValue BasicResult
+
+-- 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
+-- on a bus for example.
+-- This implementation is stack based.
+mkTagEngine :: Module (TagEngine numTags)
+mkTagEngine =
+    do
+        let reifiedNumTags = fromInteger |> valueOf numTags
+
+        freeStackVec :: Vector numTags (Reg UIntLog2N(numTags))
+        freeStackVec <- mapM (\i -> mkReg |> fromInteger i) genVector
+
+        inUseVec :: Vector numTags (Reg Bool)
+        inUseVec <- replicateM |> mkReg False
+
+        stackPtr :: (Reg (Maybe(UIntLog2N(numTags))))
+        stackPtr <- mkReg |> Just |> reifiedNumTags - 1
+
+        debugOnce <- mkReg True
+
+        addRules $
+            rules
+                "display": when (debugOnce == True) ==>
+                    do
+                        $display "freeStackVec : " (fshow |> readVReg freeStackVec)
+                        $display "inUseVec : " (fshow |> readVReg inUseVec)
+                        $display "stackPtr : " (fshow stackPtr)
+                        debugOnce := False
+
+        counter <- mkReg(0 :: UIntLog2N(numTags))
+        return $
+          interface TagEngine
+
+            requestTag :: ActionValue 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
+
+            -- 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
+                            return Success
+                        else do
+                            return Failure

bs/Top.bs

@@ -8,6 +8,7 @@ import CBindings
 import Bus
 import TagEngine
 import List
+import ActionSeq
 
 type FCLK = 25000000
 type BAUD = 9600
@@ -101,12 +102,56 @@ mkSim :: Module Empty
 mkSim = do
   let cfg          :: BRAM_Configure = defaultValue
 
-  count            :: Reg (UInt 3) <- mkReg 0;
+  tagEngine :: TagEngine 5 <- mkTagEngine
+  count            :: Reg (UInt 4) <- mkReg 0;
   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

bs/Util.bs

@@ -1,4 +1,24 @@
-package Util((|>)) where
+package Util(
+  (|>),
+  BasicResult(..),
+  simulate_for) where
+
+infixr 0 |>
+
+data BasicResult = Success
+                 | Failure
+                 deriving (Bits, Eq, FShow)
 
 (|>) :: (a -> b) -> a -> b
-f |> x = f x;
+f |> x = f x;
+
+simulate_for :: (Bits a n, Arith a, Eq a) => Reg a -> Reg a -> Rules
+simulate_for curr_cycle end_cycle =
+  rules
+    "count_cycle_rule": when True ==> action
+      curr_cycle := curr_cycle + 1
+      if curr_cycle == end_cycle
+        then
+          $finish
+        else
+          $display "cycle = " curr_cycle