By now, I’ve been using Bluespec, specifically Bluespec Classic/Haskell for a few years in my spare time(since 2022). In fact, I’ve been doing some small experiments on the ULX3S FPGA with hopes and dreams of one day fully implementing a RISC-V SOC.

Bluespec is in many ways a functional language. It has partial functions, sums and product types, monads, and the like. It also has atomic guarded actions with one rule at a time semantics. I won’t take time to dive into the exact mechanics of how ORRAT works as there is already at least one paper that does this formally. But the TLDR is that in Bluespec, you treat hardware design as a distributed systems problem. You first define state that can be mutated, and then you define sets of indivisible/atomic actions that can be taken to mutate that state. There are some conditions that have to be met in order to execute an action. Some of these conditions are intrinsic to the formal execution model of the Bluespec compiler. The remaining conditions are specified by the designer(or in existing libraries) and are rule predicates and guards.

It can take some time to learn to think the Bluespec way. There are some obvious basics such as the compiler making it impossible to dequeue an empty fifo - though this property of fifos in Bluespec is more an artifact of the guards in the FIFO library rather than an intrinsic property of The compiler itself.

In Bluespec, the ability for actions to invoke other actions(somewhat analogous to calling functions in the traditional sequential programming paradigm), enables modular and composable designs. Fair enough. Interesting behavior starts to emerge however when the compiler detects that the subsequent system state depends on the order in which an action invokes its sub-actions. Such behavior breaks Bluespec’s model of causality and can lead to scenarios where information appears to travel back in time(at least I think this was the correct interpretation although I’m not entirely sure). Perhaps I’ll provide a case study for this some day.

Today, however, I’ve chosen an example that provides a representative taste of what Bluespec is really about without being to complicated.

Depth 1 FIFOs in Bluespec

You and your sister really like to make toast. There is a toaster in the kitchen that can only toast one pair of toast at a time. Either you or your sister can toast a pair of toast - but not at the same time - it only supports one pair of toast!

This is a very special toaster. You can only interact with it using the following two operations. Note: it is possible to perform these operations simultaneously:

1. Inserting a single pair of un-toasted bread
2. Removing a single pair of toasted bread

Consider the following sequence of events for a toaster that only toasts one pair of toast at a time:

Precondition: You and your sister are both at the toaster and want to each toast your respective pairs of toast.

1. You insert your toast.
2. You retrieve your toasted toast.
3. Your sister inserts her toast.
4. She retrieve her toasted toast.

Not much to see here. So much for our toaster. It can only toast one pair of toast at a time.

Depth 2 FIFOs in Bluespec

Dad just replaced the toaster with a bigger toaster. The new toaster now toasts two pairs of toast at a time! Yet it is still like the earlier toaster in that it only supports the following actions which can be performed simultaneously:

1. Inserting a single pair of un-toasted bread
2. Removing a single pair of toasted bread

Consider the following sequence of events:

Precondition: You and your sister are both at the toaster and want to each toast your respective pairs of toast.

1. You insert your toast.
2. You retrieve your toasted toast. At the same time your sister inserts her toast.
3. Your sister retrieve her toasted toast.

Much More Toast

Word got out about and now everybody in the family wants to have some toast. For really large families, you’ll notice that we need twice much time for everyone to toast their bread with the old toaster as compared to the new toaster. No surprise here. However, what if we get a toaster that can toast say 10 pairs of toast at once? Unfortunately, the familiy will still consume the same amount of time toasting all their toast as they did when using the two-pair toaster. The limiting factor here is that regardless of how many pairs the toaster can hold simultaneous, we can only enqueue/dequeue a single piece of toast at time.

Back to Bluespec

The FIFO library and Bluespec compiler work together in such a way that depth 1 fifos have an alternating enqueue/dequeue pattern whilst fifos of greater than depth 2 allow simultaneous enqueue and dequeue every cycle(provided there is space to enqueue and data to dequeue).

In designs that only care about eventually receiving data across a fifo communication channel, both the depth 1 and depth 2 fifos are correct, although one is certainly faster(the catch being depth 2 needs more hardware resources).

In this sense, the Bluespec compiler allows you to perform design space exploration whilst preserving correctness. It could be said the Bluespec compiler offers formal safety guarantees for certain kinds of designs. For these designs, the main promise is that correct computation will eventually be yielded, although we make no promises of when. Furthermore Bluespec provides the designer with many tools to encode invariants of interest in the type system, interfaces, and atomic actions. It is up to the designer to avail himself of these facilities. It should be noted that the the facilities Bluespec provides are no substitute for theorem provers.

The Code

Below is Bluespec implementation of our old and new toasters from earlier as well as the code needed to run them. Notice out the depth1 fifo is only able to enqueue two values in four cycles whilst the depth2 fifo is able to enqueue four values.

Depth 1 Fifo

Executing

mkdir  -p build_b_sim && bsc -u -sim -simdir build_b_sim -bdir build_b_sim -info-dir build_b_sim -keep-fires -aggressive-conditions -no-warn-action-shadowing -check-assert -cpp -show-schedule +RTS -K128M -RTS  -show-range-conflict -g mkTop depth1fifo.bs && bsc -e mkTop -sim -o mkTop_b_sim -simdir build_b_sim -bdir build_b_sim -info-dir build_b_sim -keep-fires && ./mkTop_b_sim

Code for depth1fifo.bs

package Top where

import FIFO

mkTop :: Module Empty
mkTop = do
    cycle :: Reg (UInt 32)
    cycle <- mkReg 0

    depth1FIFO :: FIFO (UInt 32)
    depth1FIFO <- mkFIFO1

    addRules $
      rules
        when True ==>
          do
            cycle := cycle + 1

        when True ==>
          do
            $display "enqueuing :" cycle " during cycle :" cycle
            depth1FIFO.enq cycle

        when True ==>
          do
            $display "dequeuing :" depth1FIFO.first " during cycle :" cycle
            depth1FIFO.deq

        when (cycle == 4) ==>
          do
            $finish

Depth 2 Fifo

Executing

mkdir  -p build_b_sim && bsc -u -sim -simdir build_b_sim -bdir build_b_sim -info-dir build_b_sim -keep-fires -aggressive-conditions -no-warn-action-shadowing -check-assert -cpp -show-schedule +RTS -K128M -RTS  -show-range-conflict -g mkTop depth2fifo.bs && bsc -e mkTop -sim -o mkTop_b_sim -simdir build_b_sim -bdir build_b_sim -info-dir build_b_sim -keep-fires && ./mkTop_b_sim

Code for depth2fifo.bs

package Top where

import FIFO

mkTop :: Module Empty
mkTop = do
    cycle :: Reg (UInt 32)
    cycle <- mkReg 0

    depth2FIFO :: FIFO (UInt 32)
    depth2FIFO <- mkFIFO

    addRules $
      rules
        when True ==>
          do
            cycle := cycle + 1

        when True ==>
          do
            $display "enqueuing :" cycle " during cycle :" cycle
            depth2FIFO.enq cycle

        when True ==>
          do
            $display "dequeuing :" depth2FIFO.first " during cycle :" cycle
            depth2FIFO.deq

        when (cycle == 4) ==>
          do
            $finish