Compare commits
3 commits
7836ac5f3f
...
2308058d33
| Author | SHA1 | Date | |
|---|---|---|---|
|
2308058d33 | ||
|
|
3afca5b0f9 | ||
|
|
1c8ebeb238 |
26
README.md
26
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
|
||||
|
|
|
|||
|
|
@ -1,81 +1,10 @@
|
|||
package TagEngine(
|
||||
TagEngine(..),
|
||||
Util.BasicResult(..),
|
||||
mkTagEngine) where
|
||||
package TagEngine() where
|
||||
|
||||
import Vector
|
||||
import Util
|
||||
|
||||
#define UIntLog2N(n) (UInt (TLog n))
|
||||
|
||||
interface (TagEngine :: # -> *) numTags =
|
||||
requestTag :: ActionValue UIntLog2N(numTags)
|
||||
retireTag :: UIntLog2N(numTags) -> ActionValue BasicResult
|
||||
requestTag :: ActionValue (UInt (TLog numTags))
|
||||
retireTag :: UInt (TLog numTags) -> Action
|
||||
|
||||
-- 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
|
||||
a :: Integer
|
||||
a = 3
|
||||
47
bs/Top.bs
47
bs/Top.bs
|
|
@ -8,7 +8,6 @@ import CBindings
|
|||
import Bus
|
||||
import TagEngine
|
||||
import List
|
||||
import ActionSeq
|
||||
|
||||
type FCLK = 25000000
|
||||
type BAUD = 9600
|
||||
|
|
@ -102,56 +101,12 @@ mkSim :: Module Empty
|
|||
mkSim = do
|
||||
let cfg :: BRAM_Configure = defaultValue
|
||||
|
||||
tagEngine :: TagEngine 5 <- mkTagEngine
|
||||
count :: Reg (UInt 4) <- mkReg 0;
|
||||
count :: Reg (UInt 3) <- 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
|
||||
|
|
|
|||
22
bs/Util.bs
22
bs/Util.bs
|
|
@ -1,24 +1,4 @@
|
|||
package Util(
|
||||
(|>),
|
||||
BasicResult(..),
|
||||
simulate_for) where
|
||||
|
||||
infixr 0 |>
|
||||
|
||||
data BasicResult = Success
|
||||
| Failure
|
||||
deriving (Bits, Eq, FShow)
|
||||
package Util((|>)) where
|
||||
|
||||
(|>) :: (a -> b) -> a -> b
|
||||
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
|
||||
|
|
|
|||
Loading…
Reference in a new issue