Make make fpga work

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

.gitignore

@@ -15,6 +15,8 @@ verilog_RTL
 # files generated for FPGA ULX3s implementation
 ulx3s_fpga/mkTop.d
 ulx3s_fpga/mkTop.json
+ulx3s_fpga/mkTop.bit
+ulx3s_fpga/mkTop.config
 
 # generated experiment outputs
 experiments/bram/*.cxx

Makefile

@@ -100,7 +100,7 @@ b_all: b_compile  b_link    b_sim
 b_compile:
 	mkdir  -p build_b_sim
 	@echo Compiling for Bluesim ...
-	bsc -u -sim $(B_SIM_DIRS) $(BSC_COMP_FLAGS) $(BSC_PATHS) -g $(TOPMODULE)  $(TOPFILE) 
+	bsc -u -sim $(B_SIM_DIRS) $(BSC_COMP_FLAGS) $(BSC_PATHS) -g $(TOPMODULE)  $(TOPFILE)
 	@echo Compiling for Bluesim finished
 
 .PHONY: b_link
@@ -142,7 +142,7 @@ v_compile:
 .PHONY: v_link
 v_link: $(BDPI_OBJ)
 	@echo Linking for Verilog sim ...
-	bsc -e $(TOPMODULE) -verilog -o ./$(V_SIM_EXE) $(V_DIRS) -vsim $(V_SIM)  verilog_RTL/$(TOPMODULE).v 
+	bsc -e $(TOPMODULE) -verilog -o ./$(V_SIM_EXE) $(V_DIRS) -vsim $(V_SIM)  verilog_RTL/$(TOPMODULE).v
 	@echo Linking for Verilog sim finished
 
 .PHONY: v_sim
@@ -160,7 +160,7 @@ v_sim_vcd:
 # ----------------------------------------------------------------
 
 fpga:
-	make -C ulx3s_fpga
+	make -C ulx3s_fpga mkTop.bit
 
 .PHONY: clean
 clean:

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.
+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
-``TOPMODULE=mkTop make v_compile`` to generate verilog. The generated verilog can
+in Bluespec Haskell. Given that the Bluespec semantics are inspired by TLA+ which
-be found in the ``verilog_RTL/`` folder.
+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 
+ * Basic peripheral working on FPGA such as UART and
-of what would make for LED and UART controllers.
+   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/ClkDivider.bs

@@ -9,7 +9,7 @@ interface (ClkDivider :: # -> *) hi =
 
 mkClkDivider :: Handle -> Module (ClkDivider hi)
 mkClkDivider fileHandle = do
-    counter <- mkReg(0 :: UInt (TLog hi))   
+    counter <- mkReg(0 :: UInt (TLog hi))
     let hi_value :: UInt (TLog hi) = (fromInteger $ valueOf hi)
     let half_hi_value :: UInt (TLog hi) = (fromInteger $ valueOf (TDiv hi 2))
 
@@ -28,7 +28,7 @@ mkClkDivider fileHandle = do
           counter := if (counter == hi_value)
                     then 0
                     else counter + 1
-    
+
     return $
       interface ClkDivider
         reset :: Action

bs/Deserializer.bs

@@ -1,15 +1,15 @@
 package Deserializer(
   mkDeserialize,
   IDeserializer(..),
-  State(..)) 
+  State(..))
   where
 
 import ClkDivider
 import State
 
 
-interface (IDeserializer :: # -> # -> *) clkFreq baudRate = 
+interface (IDeserializer :: # -> # -> *) clkFreq baudRate =
-  get         ::  Bit 8            
+  get         ::  Bit 8
   putBitIn    :: (Bit 1) -> Action {-# always_enabled, always_ready #-}
 
 mkDeserialize :: Handle -> Module (IDeserializer clkFreq baudRate)
@@ -35,10 +35,10 @@ mkDeserialize fileHandle = do
           ftdiState := ftdiState' ftdiState
 
       {-# ASSERT fire when enabled #-}
-        "SAMPLING" : when 
+        "SAMPLING" : when
           DATA(n) <- ftdiState,
           n >= 0,
-          n <= 7, 
+          n <= 7,
           let sampleTrigger = clkDivider.isHalfCycle
             in sampleTrigger
           ==>
@@ -48,6 +48,6 @@ mkDeserialize fileHandle = do
   return $
     interface IDeserializer
     {get      = shiftReg when (ftdiState == STOP), (clkDivider.isAdvancing)
-    ;putBitIn bit = 
+    ;putBitIn bit =
       ftdiRxIn := bit
     }

bs/Serializer.bs

@@ -1,7 +1,7 @@
 package Serializer(
   mkSerialize,
   ISerializer(..),
-  State(..)) 
+  State(..))
   where
 
 import ClkDivider
@@ -14,7 +14,7 @@ serialize ftdiState dataReg =
         (DATA n) -> dataReg[n:n]
         _        -> 1'b1
 
-interface (ISerializer :: # -> # -> *) clkFreq baudRate = 
+interface (ISerializer :: # -> # -> *) clkFreq baudRate =
   putBit8    :: (Bit 8) -> Action {-# always_enabled, always_ready #-}
   bitLineOut ::  Bit 1            {-# always_ready #-}
 
@@ -29,8 +29,8 @@ mkSerialize fileHandle = do
   addRules $
     rules
       {-# ASSERT fire when enabled #-}
-      "ADVANCE UART STATE WHEN NOT IDLE" : when 
+      "ADVANCE UART STATE WHEN NOT IDLE" : when
-        (ftdiState /= IDLE), 
+        (ftdiState /= IDLE),
         (clkDivider.isAdvancing) ==>
         do
           ftdiState := ftdiState' ftdiState
@@ -42,11 +42,10 @@ mkSerialize fileHandle = do
 
   return $
     interface ISerializer
-      putBit8  bit8Val = 
+      putBit8  bit8Val =
         do
           clkDivider.reset
-          dataReg := bit8Val 
+          dataReg := bit8Val
           ftdiState := ftdiState' ftdiState
         when (ftdiState == IDLE)
       bitLineOut = ftdiTxOut
-    

bs/State.bs

@@ -2,15 +2,15 @@ package State(
   State(..),
   ftdiState') where
 
-data State = IDLE 
+data State = IDLE
-           | START 
+           | START
-           | DATA (UInt (TLog 8)) 
+           | DATA (UInt (TLog 8))
-           | PARITY 
+           | PARITY
            | STOP
            deriving (Bits, Eq, FShow)
 
 ftdiState' :: State -> State
-ftdiState' state = 
+ftdiState' state =
   case state of
     IDLE    -> START
     START   -> DATA(0)

bs/TagEngine.bs

@@ -1,10 +1,81 @@
-package TagEngine() where
+package TagEngine(
+    TagEngine(..),
+    Util.BasicResult(..),
+    mkTagEngine) where
 
+import Vector
 import Util
 
-interface (TagEngine :: # -> *) numTags =
+#define UIntLog2N(n) (UInt (TLog n))
-    requestTag :: ActionValue (UInt (TLog numTags))
-    retireTag  :: UInt (TLog numTags) -> Action
 
-a :: Integer
+interface (TagEngine :: # -> *) numTags =
-a = 3
+    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

flake.lock

@@ -0,0 +1,61 @@
+{
+  "nodes": {
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1735821806,
+        "narHash": "sha256-cuNapx/uQeCgeuhUhdck3JKbgpsml259sjUQnWM7zW8=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "d6973081434f88088e5321f83ebafe9a1167c367",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixpkgs-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "nixpkgs": "nixpkgs",
+        "utils": "utils"
+      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
+    },
+    "utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1731533236,
+        "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}

flake.nix

@@ -0,0 +1,69 @@
+{
+  inputs = {
+    nixpkgs = {
+      url = "github:NixOS/nixpkgs/nixpkgs-unstable";
+    };
+    utils.url = "github:numtide/flake-utils";
+  };
+
+  outputs =
+    inputs:
+    inputs.utils.lib.eachDefaultSystem (
+      system:
+      let
+        pkgs = import inputs.nixpkgs {
+          localSystem = system;
+          overlays = [
+            (final: prev: {
+
+              riscv-bluespec-classic = pkgs.callPackage (
+                {
+                  stdenv,
+                  bluespec,
+                  nextpnr,
+                  openfpgaloader,
+                  trellis,
+                  which,
+                  yosys,
+                  TOPMODULE ? "mkTop",
+                  makeFlags ? [ ],
+                }:
+                stdenv.mkDerivation {
+                  pname = "riscv-bluespec-classic";
+                  version = "0.1.0";
+                  src = ./.;
+
+                  # Versions can be checked with
+                  # `nix eval --json ".#bluespec-joh-template.nativeBuildInputs" | nix-shell -p jq --run jq`
+                  nativeBuildInputs = [
+                    bluespec
+                    nextpnr
+                    openfpgaloader
+                    trellis
+                    which
+                    yosys
+                  ];
+
+                  # TODO: Build and install something
+
+                }
+              ) { };
+
+            })
+          ];
+        };
+      in
+      {
+        packages = {
+          default = inputs.self.packages."${system}".riscv-bluespec-classic;
+          riscv-bluespec-classic = pkgs.riscv-bluespec-classic;
+        };
+
+        devShells.default =
+          with pkgs;
+          mkShell {
+            inputsFrom = [ riscv-bluespec-classic ];
+          };
+      }
+    );
+}

shell.nix

@@ -1,14 +0,0 @@
-{ pkgs ? import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/d34a98666913267786d9ab4aa803a1fc75f81f4d.tar.gz") {} }:
-
-pkgs.mkShell {
-  buildInputs = [
-    pkgs.yosys
-    pkgs.nextpnr
-    pkgs.bluespec
-    pkgs.yosys-bluespec
-  ];
-
-  shellHook = ''
-    echo "Dev environment for Manna Chip."
-  '';
-}

ulx3s_fpga/makefile

@@ -5,7 +5,7 @@ IDCODE ?= 0x41113043 # 85f
 
 all: prog
 
-../verilog_RTL/$(TOPMODULE).v: ../src/Top.bsv
+../verilog_RTL/$(TOPMODULE).v: ../bs/Top.bs
 	V_SIM=verilator TOPMODULE=$(TOPMODULE) make -C ../ v_compile
 
 $(TOPMODULE).json: ../verilog_RTL/$(TOPMODULE).v
@@ -21,6 +21,7 @@ $(TOPMODULE).config: $(TOPMODULE).json
 		--textcfg $@ \
 		--lpf ulx3s_v20.lpf \
 		--85k \
+		--lpf-allow-unconstrained \
 		--package CABGA381
 
 $(TOPMODULE).bit: $(TOPMODULE).config