# 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``