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 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 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 at git commit: 7ce5011c24b
2. nextpnr-0.4-36-gc8406b71
3. PrjTrellis at git commit: 1.2.1-22-g35f5aff
4. openFPGALoader

Programming the ULX3S

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.

TOPMODULE=mkSim make b_all

Experiments

See experiments README.

Generating Verilog

TOPMODULE=mkTop make v_compile

TODO

• debug UART accuracy - clk divider should be frequency matched
• move to JoyOfHardware
• port in 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