77 lines
2.7 KiB
Markdown
77 lines
2.7 KiB
Markdown
# RISC-V Bluespec Classic
|
|
|
|
## Introduction:
|
|
|
|
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
|
|
* 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
|
|
Running `nix-shell` should *just work* on Linux. To be fair, haven't
|
|
tested this yet.
|
|
|
|
## MacOS
|
|
Upstream nix recipes need to be adjusted a bit to work on MacOS, so
|
|
for now do:
|
|
1. [Yosys](https://github.com/YosysHQ/yosys) at git commit: 7ce5011c24b
|
|
2. [nextpnr-0.4-36-gc8406b71](https://github.com/YosysHQ/nextpnr)
|
|
3. [PrjTrellis](https://github.com/YosysHQ/prjtrellis) at git commit: 1.2.1-22-g35f5aff
|
|
4. [openFPGALoader](https://github.com/trabucayre/openFPGALoader)
|
|
|
|
# Programming the ULX3S
|
|
```bash
|
|
make fpga
|
|
# You may need the following line to set your screen device config
|
|
# to one parity and one stop bit. Tested working on MacOS, should
|
|
# work on Linux.
|
|
stty -f /dev/tty.usbserial-K00027 -cstopb -parenb
|
|
screen /dev/tty.usbserial-K00027 9600
|
|
```
|
|
|
|
# Simulation
|
|
## Main Chip Core
|
|
The following command will simulate the UART loopback
|
|
by having the bluespec sources call some C code that
|
|
commandeers the tty, disables echo, exposes the tty write
|
|
buffer to bluespec(what the user types), and exposes
|
|
a buffer bluespec can use to write to terminal.
|
|
|
|
```bash
|
|
TOPMODULE=mkSim make b_all
|
|
```
|
|
|
|
## Experiments
|
|
See experiments README.
|
|
|
|
# Generating Verilog
|
|
```bash
|
|
TOPMODULE=mkTop make v_compile
|
|
```
|
|
|
|
# TODO
|
|
- [ ] debug UART accuracy
|
|
- clk divider should be frequency matched
|
|
- [ ] move to JoyOfHardware
|
|
- [ ] port in [RiscV-Formal](https://git.joyofhardware.com/Yehowshua/RiscV-Formal)
|
|
- [ ] create I and D caches
|
|
- [ ] try to optimize decoder
|
|
|
|
# Notable Reference Files
|
|
``/Users/yehowshuaimmanuel/git/bsc/testsuite/bsc.bsv_examples/cpu/FiveStageCPUQ3sol.bsv``
|