Compare commits

..

3 commits

Author SHA1 Message Date
Artturin 2308058d33 Make make fpga work
`ERROR: IO 'ftdi_txd_1' is unconstrained in LPF (override this error with --lpf-allow-unconstrained)`
2025-04-02 03:10:29 +03:00
Artturin 3afca5b0f9 Remove all trailing spaces
`git grep -I --name-only -z -e '' | xargs -0 sed -i 's/[ \t]\+\(\r\?\)$/\1/'`

Remember to setup your editor so that these are automatically removed :)
2025-04-02 03:04:44 +03:00
Artturin 1c8ebeb238 Add initial flake 2025-04-02 02:59:21 +03:00
4 changed files with 18 additions and 162 deletions

View file

@ -1,25 +1,17 @@
# RISC-V Bluespec Classic # MannaChip
## Introduction: ## 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 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.
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 ``TOPMODULE=mkTop make v_compile`` to generate verilog. The generated verilog can
is different from traditional Haskell semantics, we're doing functional design be found in the ``verilog_RTL/`` folder.
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 # Status
* Basic peripheral working on FPGA such as UART and Admittedly, not very far. Perhaps one could say we've got the beginnings
BRAM(work on this is out of tree - need to merge) of what would make for LED and UART controllers.
* 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 # Dependencies
## Linux ## Linux

View file

@ -1,81 +1,10 @@
package TagEngine( package TagEngine() where
TagEngine(..),
Util.BasicResult(..),
mkTagEngine) where
import Vector
import Util import Util
#define UIntLog2N(n) (UInt (TLog n))
interface (TagEngine :: # -> *) numTags = interface (TagEngine :: # -> *) numTags =
requestTag :: ActionValue UIntLog2N(numTags) requestTag :: ActionValue (UInt (TLog numTags))
retireTag :: UIntLog2N(numTags) -> ActionValue BasicResult retireTag :: UInt (TLog numTags) -> Action
-- The tag engine returns a tag that is unique for the duration of a :: Integer
-- the lifetime of the tag. Useful when you need to tag transactions a = 3
-- 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

View file

@ -8,7 +8,6 @@ import CBindings
import Bus import Bus
import TagEngine import TagEngine
import List import List
import ActionSeq
type FCLK = 25000000 type FCLK = 25000000
type BAUD = 9600 type BAUD = 9600
@ -102,56 +101,12 @@ mkSim :: Module Empty
mkSim = do mkSim = do
let cfg :: BRAM_Configure = defaultValue let cfg :: BRAM_Configure = defaultValue
tagEngine :: TagEngine 5 <- mkTagEngine count :: Reg (UInt 3) <- mkReg 0;
count :: Reg (UInt 4) <- mkReg 0;
initCFunctions :: Reg Bool <- mkReg False; initCFunctions :: Reg Bool <- mkReg False;
core :: Core FCLK <- mkCore; 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 $ addRules $
rules rules
"testIncrement": when (count < 10) ==>
do
count := count + 1
s.start
"initCFunctionsOnce": when not initCFunctions ==> "initCFunctionsOnce": when not initCFunctions ==>
do do
initTerminal initTerminal

View file

@ -1,24 +1,4 @@
package Util( package Util((|>)) where
(|>),
BasicResult(..),
simulate_for) where
infixr 0 |>
data BasicResult = Success
| Failure
deriving (Bits, Eq, FShow)
(|>) :: (a -> b) -> a -> b (|>) :: (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