A new, more hardware-friendly design for copilot-bluespec

[RyanGlScott]

Currently, the code that copilot-bluespec generates is suitable for simulation, but it is not as suitable for use directly in hardware. One of the more notable challenges is that the generated Bluespec interfaces are compiled to Verilog in the opposite way that one would intuitively expect. Currently, a Copilot external stream is compiled into a Verilog output, and a Copilot trigger is compiled into a series of Verilog inputs. This is counterintuitive, as one would expect the external streams to be inputs instead, and would expect the values associated with a Copilot trigger to be outputs instead.

Fortunately, I think it is possible to fix this design flaw with some changes to how copilot-bluespec generates interfaces. To explain what I mean, I will use the following Copilot program (inspired by a question that @sukhmankkahlon asked here) as a running example:

-- Led.hs
{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where

import Copilot.Compile.Bluespec
import Language.Copilot

sw :: Stream Word8
sw = extern "sw" Nothing

counter :: Stream Word8
counter = [0] ++ (counter + 1)

led :: Stream Word8
led = (sw .&. 0b11111110) .|. (counter .&. 0b00000001)

spec :: Spec
spec = trigger "led" true [arg led]

main :: IO ()
main = do
  spec' <- reify spec
  compile "Led" spec'

This example has one external stream (sw), one stream that is internal to the program (counter), and another stream that is associated with a trigger (led). Our goal is to directly compile this to Verilog such that sw is an input, led comprises the outputs (note that "outputs" is plural—more on this later), and there are no other inputs or outputs (aside from Verilog's default ports, i.e., the CLK and RST signals).

My proposal is to change copilot-bluespec to generate the following Bluespec interface for the program above:

interface LedIfc {-# always_ready, always_enabled #-} =
  -- Assigns the input for the `sw` external stream.
  sw :: UInt 8 -> Action {-# prefix = "", arg_names = ["sw"] #-}
  -- Outputs if the `led` trigger fires on a given clock cycle.
  ledGuard :: Bool
  -- Outputs the `led` trigger's first stream argument.
  ledArg0 :: UInt 8

This looks a bit different than what copilot-bluespec currently generates, so let's review the differences:

• The {-# always_ready, always_enabled #-} pragmas indicate that we should not generate extra "ready" or "enabled" inputs/outputs for the interface methods, which cuts down on the number of inputs/outputs that you have to managed in the generated Verilog code.

• The sw external stream is compiled to an interface method of type UInt 8 -> Action. The fact that UInt 8 occurs in an argument position to a function means that it will turn into an input when compiled to Verilog. (We will see how to define and call this function shortly.)

  Also note the {-# prefix = "", arg_names = ["sw"] #-} pragma, which is used to ensure that the corresponding Verilog input is also named "sw". (Otherwise, Verilog would give it a name like sw_0 or some such.)

• The led trigger is compiled into two interface methods. One method, ledGuard, returns a Bool, and the other method, ledArg0, returns a UInt 8. Because both of these types are return types, they are both turned into outputs when compiled to Verilog. (Note that the numeric suffix in "ledArg0" indicates that it is the first argument associated with the trigger. If there were additional trigger arguments, then they would be compiled to additional interface methods named ledArg1, ledArg2, and so on.)

  I have made a choice to turn each Copilot trigger into multiple interface methods, and thus multiple outputs in the generated Verilog code. This is mainly done for the sake of convenience, as it gives distinct names to the different properties of a trigger handling function. Alternatively, we could bundle all of these things into one type, e.g.,

  led :: (Bool, UInt 8)

  But this has the downside that the generated Verilog would represent led as a single 9-bit value, and one would have to manually perform bit-arithmetic on the 9-bit value to extract the bits corresponding to ledGuard and ledArg0. This seemed a bit clunky, so I have opted not to do this.

In addition to generating LedIfc, copilot-bluespec will also generate a function to create a module instantiating LedIfc:

{-# properties mkLed = { synthesize } #-}
mkLed :: Module LedIfc
mkLed =
  module
    -- We assign the input from the `sw` interface method to this Wire. As the
    -- name "Wire" suggests, this compiles directly to a Verilog wire.
    swWire :: Wire (UInt 8) <- mkBypassWire

    -- Create a ring buffer for the `counter` stream.
    counterReg :: Reg (UInt 8) <- mkReg 0
    let counterRingBuf :: Vector 1 (Reg (UInt 8))
        counterRingBuf = update newVector 0 counterReg
    counterIdx :: Reg (Bit 64) <- mkReg 0
    let counterGet :: Bit 64 -> UInt 8
        counterGet x = (select counterRingBuf ((counterIdx + x) % 1))._read
        counterGen :: UInt 8
        counterGen = counterGet 0 + 1

    interface
      -- Assign the input for the `sw` external stream to `swWire`.
      sw val = swWire := val

      -- Compute if the `led` trigger fires on a given clock cycle.
      ledGuard = True
      -- Compute the `led` trigger's first stream argument.
      ledArg0 = (swWire & 8'b11111110) | (counterGet 0 & 8'b00000001)

    rules
      -- Compute the next value in the `counter` ring buffer.
      "step": when True ==> action
        (select counterRingBuf counterIdx) := counterGen
        counterIdx := (counterIdx + 1) % 1

A lot of this identical to what copilot-bluespec currently does, but note the following differences:

• Instead of giving mkLed the type Module LedIfc -> Module Empty, we simply make mkLed return Module LedIfc directly. An important hardware-related use case is to be able to compile mkLed to Verilog in isolation, and the new type signature streamlines this process.
• We use the {-# properties mkLed = { synthesize } #-} to ensure that the mkLed function can be cleanly compiled to Verilog.
• We create a dedicated Wire (swWire) for the purposes of defining sw in the interface block. When the sw is called, it simply writes its input to swWire, and the written value is then used elsewhere in the module (e.g., in the implementation of ledArg0).
• We no longer have a separate rule for the led trigger. Instead, we do the necessary led-related computation in the interface block, where we define ledGuard and ledArg0.

Now, we can compile mkLed to Verilog:

$ bsc -verilog -g mkLed -u Led.bs

Which yields the following Verilog code:

//
// Generated by Bluespec Compiler, version 2025.01.1 (build 65e3a87)
//
// On Fri Aug  8 10:18:10 EDT 2025
//
//
// Ports:
// Name                         I/O  size props
// ledGuard                       O     1 const
// ledArg0                        O     8
// CLK                            I     1 clock
// RST_N                          I     1 reset
// sw                             I     8
//
// Combinational paths from inputs to outputs:
//   sw -> ledArg0
//
//

`ifdef BSV_ASSIGNMENT_DELAY
`else
  `define BSV_ASSIGNMENT_DELAY
`endif

`ifdef BSV_POSITIVE_RESET
  `define BSV_RESET_VALUE 1'b1
  `define BSV_RESET_EDGE posedge
`else
  `define BSV_RESET_VALUE 1'b0
  `define BSV_RESET_EDGE negedge
`endif

module mkLed(CLK,
	     RST_N,

	     sw,

	     ledGuard,

	     ledArg0);
  input  CLK;
  input  RST_N;

  // action method sw
  input  [7 : 0] sw;

  // value method ledGuard
  output ledGuard;

  // value method ledArg0
  output [7 : 0] ledArg0;

  // signals for module outputs
  wire [7 : 0] ledArg0;
  wire ledGuard;

  // register counterIdx
  reg [63 : 0] counterIdx;
  wire [63 : 0] counterIdx$D_IN;
  wire counterIdx$EN;

  // register counterReg
  reg [7 : 0] counterReg;
  wire [7 : 0] counterReg$D_IN;
  wire counterReg$EN;

  // value method ledGuard
  assign ledGuard = 1'd1 ;

  // value method ledArg0
  assign ledArg0 = { sw[7:1], counterReg[0] } ;

  // register counterIdx
  assign counterIdx$D_IN = 64'd0 ;
  assign counterIdx$EN = 1'd1 ;

  // register counterReg
  assign counterReg$D_IN = counterReg + 8'd1 ;
  assign counterReg$EN = counterIdx == 64'd0 ;

  // handling of inlined registers

  always@(posedge CLK)
  begin
    if (RST_N == `BSV_RESET_VALUE)
      begin
        counterIdx <= `BSV_ASSIGNMENT_DELAY 64'd0;
	counterReg <= `BSV_ASSIGNMENT_DELAY 8'd0;
      end
    else
      begin
        if (counterIdx$EN)
	  counterIdx <= `BSV_ASSIGNMENT_DELAY counterIdx$D_IN;
	if (counterReg$EN)
	  counterReg <= `BSV_ASSIGNMENT_DELAY counterReg$D_IN;
      end
  end

  // synopsys translate_off
  `ifdef BSV_NO_INITIAL_BLOCKS
  `else // not BSV_NO_INITIAL_BLOCKS
  initial
  begin
    counterIdx = 64'hAAAAAAAAAAAAAAAA;
    counterReg = 8'hAA;
  end
  `endif // BSV_NO_INITIAL_BLOCKS
  // synopsys translate_on
endmodule  // mkLed

Aside from the default CLK and RST_N signals, we see exactly one input (sw) and exactly two outputs (ledGuard and ledArg0). Nice!

Besides running the code on hardware, another important use case is to be able to simulate the code (e.g., using Bluesim, Verilator, or some other simulator). The generated Bluespec code above is designed to be straightforward to simulate as well. For instance, here is an example Top.bs package that simply outputs the led value on each clock cycle:

-- Top.bs
package Top where

import Led

mkTop :: Module Empty
mkTop =
  module
    ledMod <- mkLed

    rules
      -- Assign the input for the `sw` external stream.
      "sw": when True ==> ledMod.sw 8'b11111111

      -- When the `led` trigger fires, take its output (ledArg0) and display it.
      "led": when ledMod.ledGuard ==>
        $display (fshow ledMod.ledArg0)

Note that there is a small amount of boilerplate needed here, since we now have to define the rule for the led trigger here instead of in the generated code for mkLed. Previously, we defined a callback function in the generated LedIfc interface for performing the trigger handling function's action, but this would result in unwanted inputs in the Verilog code, which is why I deliberately avoided doing so in the new design. Thankfully, the amount of boilerplate required per trigger isn't that bad: you just write "<trigger name>": when <module>.<trigger guard> ==> action ... and then fill in ... with whatever action you want to take when the trigger fires.

[ivanperez-keera]

@RyanGlScott What would it take to prototype this change to copilot-bluespec?

[RyanGlScott]

Is there a way that the different elements of mkLedRules could be named so that the reader knows what each means just by looking at the Top module?

We could consider generating an interface to accompany mkLedRules such that each argument is given a name, e.g.,

interface LedRulesIfc =
  -- Action to take to compute the value of the `sw` external stream on each clock cycle
  swAction :: ActionValue (UInt 8)
  -- Action to take if `led` trigger fires on a given clock cycle
  ledAction :: UInt 8 -> Action

With this, the generated definition of mkLedRules would then become:

mkLedRules :: LedIfc -> LedRulesIfc -> Rules
mkLedRules ledIfc ledRulesIfc =
  rules
    "sw": when True ==> action
      swVal <- ledRulesIfc.swAction
      ledIfc.sw swVal

    "led": when ledIfc.ledGuard ==>
      ledRulesIfc.ledAction ledIfc.ledArg0

And then one could define the example Top.bs package like so:

mkTop :: Module Empty
mkTop =
  module
    ledMod <- mkLed

    addRules $
      mkLedRules ledMod $
        interface LedRulesIfc
         -- Assign the input for the `sw` external stream.
         swAction = return 8'b11111111
         -- When the `led` trigger fires, take its output (ledArg0) and display it.
         ledAction ledArg0 =
           $display (fshow ledArg0)

This is functionally equivalent to what is shown above, but now it's a bit clearer which callback relates to sw and which callback relates to led.

Will there be any limitations when doing it that way (e.g., difficulty sensing new values from the second argument to mkLedRules).

I don't think so. Defining it using a callback like this is exactly how it's done in copilot-c99, so it should be just as expressive.

[ivanperez-keera]

This is functionally equivalent to what is shown above, but now it's a bit clearer which callback relates to sw and which callback relates to led.

I like this.

Should \ledMod -> addRules . mkLedRules ledMod be called something so that you only need to do:

mkTop :: Module Empty
mkTop =
  module
    ledMod <- mkLed

    addLedRules ledMod $
      interface LedRulesIfc
       -- Assign the input for the `sw` external stream.
       swAction = return 8'b11111111
       -- When the `led` trigger fires, take its output (ledArg0) and display it.
       ledAction ledArg0 =
         $display (fshow ledArg0)

[ivanperez-keera]

I don't think so. Defining it using a callback like this is exactly how it's done in copilot-c99, so it should be just as expressive.

C and bluespec are not similar.

In Haskell, swAction would need an IORef, MVar or similarly mutable container if it's supposed to return different values at different times (a sensor would do, but if the data is generated by a function, instead of being sensed, then one would need to deal with state).

[RyanGlScott]

swAction has the type ActionValue (UInt 8), where ActionValue is a monad that permits the kinds of stateful things needed to return different values at different times. (For instance, you could define swAction to read from a sensor or a register.)

[RyanGlScott]

Should \ledMod -> addRules . mkLedRules ledMod be called something

Sure, we could just as well offer a addLedRules :: LedIfc -> LedRulesIfc -> Module Empty function.

[RyanGlScott]

I've pushed a proof-of-concept implementation to this branch on my Copilot fork. Please do give it a try! Some further work needs to be done in polishing the documentation to reflect the new design, but I'll wait until we reach a consensus that we want to adopt this approach before doing so.

[RyanGlScott]

@sukhmankkahlon recently had a chance to test-drive the proof-of-concept branch, and the results are much better than what you get with the current copilot-bluespec implementation. @sukhmankkahlon provided some feedback on some of the finer points of my branch's implementation:

1. Currently, the generated Verilog code will generate an output for a trigger guard (e.g., ledGuard) even if the boolean expression that defines the guard is simply constant True. This is perhaps a bit redundant, since the output will always be the same on every clock cycle. We may consider omitting the output for the guard entirely in such a scenario.

2. Relatedly, we generate separate outputs for a trigger's arguments (e.g., ledArg0), but there is no relationship between the trigger guard output and the trigger argument outputs in the generated Verilog. This is perhaps a bit strange, as one might expect that the signals from the trigger argument outputs to only be sent when the guard expression holds. It is not clear to me what the best way to encode the relationship between the two types of trigger outputs are, however. For instance, should the trigger argument output some kind of default value (e.g., 0) when the guard expression is false?

   (For now, this is not a huge deal, as @sukhmankkahlon's example always uses constant True for the guard expression.)