`copilot-bluespec`: Flip direction of interface inputs and outputs in Bluespec. Refs #677. #678

RyanGlScott · 2025-11-03T12:31:59Z

The current Bluespec backend leads to Verilog code that requires manual manipulations in order to work correctly. Specifically, Copilot externs, which are inputs to the Copilot monitoring system, are treated as outputs in Verilog, and Copilot triggers, which can be considered outputs of the monitoring system, are treated as inputs. This order of inputs and outputs is the opposite what we would like users to work with, and of what other backends generate (e.g., C99).

This PR updates copilot-bluespec to flip the order in which generated Bluespec module interfaces declare their inputs and outputs. A module interface now represents each Copilot extern as a method of type <ty> -> Action (where <ty> is the type of the extern), as this type directly translates to a Verilog input. Moreover, a module interface now represents trigger arguments as interface methods of type <ty>_i, where each <ty>_i is the type of each trigger argument. Each <ty>_i directly translates to a Verilog output.

In addition to changing the module interface definitions, this PR also changes the generated modules that instantiate the new interfaces. One of the more notable changes is that all extern values are stored as a Bluespec Wire in the module internals, as this leads to compact Verilog code without adding any user-visible inputs or outputs. Every time a value is read from an extern, the corresponding Wire must be read from, which means that several parts of the module internals have been updated to reference these Wires.

This PR also updates the test suite and DESIGN.md document accordingly.

Fixes #677.

RyanGlScott · 2025-11-03T13:39:47Z

I'm not quite sure why Travis CI is timing out... any ideas?

copilot-bluespec/src/Copilot/Compile/Bluespec/CodeGen.hs

ivanperez-keera · 2025-11-06T15:43:08Z

copilot-bluespec/src/Copilot/Compile/Bluespec/CodeGen.hs

+        [ BS.PIPrefixStr ""
+        , BS.PIArgNames [BS.mkId BS.NoPos $ fromString $ lowercaseName name]
+        ]
+        (BS.tArrow `BS.TAp` transType ty `BS.TAp` BS.tAction)


Change Manager: What is this?

(BS.tArrow BS.TAptransType tyBS.TAp BS.tAction)

That is the Bluespec abstract syntax for the type ty -> Action, which is the type of the generated interface method for an extern.

Like in Haskell, the function type (->) is represented as a type constructor that is applied (using BS.TAp, short for "type application") to two type arguments, the argument type <ty> and the result type Action. As a result, the AST for this type is:

BS.TAp BS.tArrow (BS.TAp (transType ty) BS.tAction)

It becomes a bit difficult to read these ASTs when there are a lot of applications (i.e., a lot of BS.TAps) involved, so I usually write the BS.TAp applications as infix to cut down on the amount of parentheses required. This is just a stylistic preference, however—I'm fine with writing using prefix applications (like in the code shown above) if you'd prefer that.

Change Manager: We decide to keep it in its expanded form for now but note an opportunity to simplify the code in the future.

copilot-bluespec/src/Copilot/Compile/Bluespec/CodeGen.hs

copilot-bluespec/src/Copilot/Compile/Bluespec/Compile.hs

ivanperez-keera · 2025-11-06T16:02:05Z

Change Manager:

See change list above.
In the second commit message: Now that copilot-bluespec has been updated to invert the order in which
Verilog inputs and outputs are declared" -> rephrase to read "A prior commit has . ."
Do not use this as a pronoun to refer to this commit. Best to always qualify what this is (e.g., this commit, this module, this ...).
Is the change to use input1 instead of input something that resulted from this PR, or something that was a problem before but only was detected now?

ivanperez-keera

Change Manager: See individual comments.

…luespec. Refs Copilot-Language#677. The current Bluespec backend leads to Verilog code that requires manual manipulations in order to work correctly. Specifically, Copilot externs, which are inputs to the Copilot monitoring system, are treated as _outputs_ in Verilog, and Copilot triggers, which can be considered outputs of the monitoring system, are treated as _inputs_. This order of inputs and outputs is the opposite what we would like users to work with, and of what other backends generate (e.g., C99). This commit updates the internals of `copilot-bluespec` to flip the order in which generated Bluespec module interfaces declare their inputs and outputs. A module interface now represents each Copilot extern as a method of type `<ty> -> Action` (where `<ty>` is the type of the extern), as this type directly translates to a Verilog input. Moreover, a module interface now represents trigger arguments as interface methods of type `<ty>_i`, where each `<ty>_i` is the type of each trigger argument. Each `<ty>_i` directly translates to a Verilog output. In addition to changing the module interface definitions, this commit also changes the generated modules that instantiate the new interfaces. One of the more notable changes is that all extern values are stored as a Bluespec `Wire` in the module internals, as using `Wire`s leads to compact Verilog code without adding any user-visible inputs or outputs. Every time a value is read from an extern, the corresponding `Wire` must be read from, which means that several parts of the module internals have been updated to reference these `Wire`s.

RyanGlScott · 2025-11-07T00:51:30Z

Is the change to use input1 instead of input something that resulted from this PR, or something that was a problem before but only was detected now?

The former.

Whenever you run bsc -g <function>, Bluespec requires that <function> have the result type Module <Ifc>, and moreover, <Ifc> must not have any methods with names that clash with reserved Verilog keywords (e.g., input). Prior to this PR, we were always compiling <function>s with types that look like:

mkMod :: Module <Ifc> -> Module Empty

Here, the result type is Module Empty, and because Empty has no interface methods, it trivially meets the requirement that none of its interface methods clash with Verilog keywords. Note that it did not matter what the names of <Ifc>'s methods were, as the naming requirements only apply to the result type.

After this PR, however, we now compile <function>s with types that look like this:

mkMod :: Module <Ifc>

Now Bluespec does check if <Ifc>'s methods clash with reserved Verilog keywords, so it rejected the use of input as a method name in the copilot-blue spec test suite. Renaming input to input1 was the most straightforward way to fix this. Moreover, it parallels how we handle test cases with multiple externs, where we distinguish the externs by naming them input1 and input2.

RyanGlScott · 2025-11-07T00:53:30Z

Implementor: Fix implemented, review requested.

copilot-bluespec/src/Copilot/Compile/Bluespec/Compile.hs

ivanperez-keera · 2025-11-07T19:19:00Z

Change Manager: Please address the comments above.

…new input/output order. Refs Copilot-Language#677. The current Bluespec backend leads to Verilog code that requires manual manipulations in order to work correctly. Specifically, Copilot externs, which are inputs to the Copilot monitoring system, are treated as _outputs_ in Verilog, and Copilot triggers, which can be considered outputs of the monitoring system, are treated as _inputs_. This order of inputs and outputs is the opposite what we would like users to work with, and of what other backends generate (e.g., C99). A prior commit has updated the internals of `copilot-bluespec` to invert the order in which Verilog inputs and outputs are declared. This commit adapts the top-level code in `Copilot.Compile.Bluespec.Compile` accordingly. In particular, the `compileWith` function now generates a `<Prefix>.bs` file that defines two module interfaces: one interface that contains the core methods that will comprise the generated Verilog code, and another interface that helps automate the process of defining a `Module Empty` value that is more suitable for software simulation purposes. Previously, `compileWith` generated a separate `<Prefix>Ifc.bs` file that contained nothing but the module interface in isolation so that it could be used separately from the interface's `Module` definition. This distinction no longer makes as much sense, as in the new design, as (1) there are now multiple interfaces, and (2) it is unlikely that the interfaces are not particularly useful without having the `Module` definitions to accompany them. As such, this commit now omits generating a `<Prefix>Ifc.bs` file, instead opting to generate the interfaces as part of `<Prefix>.bs`.

…Refs Copilot-Language#677. The current Bluespec backend leads to Verilog code that requires manual manipulations in order to work correctly. Specifically, Copilot externs, which are inputs to the Copilot monitoring system, are treated as _outputs_ in Verilog, and Copilot triggers, which can be considered outputs of the monitoring system, are treated as _inputs_. This order of inputs and outputs is the opposite what we would like users to work with, and of what other backends generate (e.g., C99). A prior commit has updated the internals of `copilot-bluespec` to invert the order in which Verilog inputs and outputs are declared. This commit updates the test suite to work with the new design. In addition to changing the code to reflect the new order of inputs and outputs, this commit also updates the names of some internal variables from "`input`" to "`input1`". This change is necessary because "`input`" is a reserved keyword in Verilog, and giving a Bluespec interface method the same name as a reserved Verilog keyword becomes an error when the interface is used in the result type of a synthesized module.

… Refs Copilot-Language#677. The current Bluespec backend leads to Verilog code that requires manual manipulations in order to work correctly. Specifically, Copilot externs, which are inputs to the Copilot monitoring system, are treated as _outputs_ in Verilog, and Copilot triggers, which can be considered outputs of the monitoring system, are treated as _inputs_. This order of inputs and outputs is the opposite what we would like users to work with, and of what other backends generate (e.g., C99). A prior commit has updated the internals of `copilot-bluespec` to invert the order in which Verilog inputs and outputs are declared. This commit updates the prose in the `DESIGN.md` document to reflect the new design. The new design is just different enough from the old one that it made sense to completely rewrite certain portions of the document. One of the more notable changes is that there are now separate sections about running the generated Verilog code on hardware versus simulating the generated code in software, as these are distinct use cases that require separate discussion.

…e#677.

RyanGlScott · 2025-11-07T19:59:23Z

Implementor: Fix implemented, review requested.

copilot-bluespec/src/Copilot/Compile/Bluespec/Compile.hs

copilot-bluespec/DESIGN.md

ivanperez-keera · 2025-11-08T14:46:57Z

Change Manager: Verified that:

Solution is implemented:

The code proposed compiles and passes all tests. Details:
Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/276773685

The solution proposed produces the expected result. Details:
The following Dockerfile checks that the existing FPGA example can be compiled, executed, and that the execution matches the expectation for the first 10 lines of output, both in the Bluespec simulator and in iverilog without any changes to the Verilog code, and it checks the same for an additional example that produces the Fibonacci sequence, after which it prints the message "Success":

--- Dockerfile-verify-677
FROM ubuntu:jammy

WORKDIR /root
SHELL ["/bin/bash", "-c"]

ENV DEBIAN_FRONTEND=noninteractive
RUN apt-get update

RUN apt-get install --yes \
      libz-dev \
      git \
      curl \
      gcc \
      g++ \
      make \
      libgmp3-dev  \
      pkg-config

RUN mkdir -p $HOME/.ghcup/bin
RUN curl https://downloads.haskell.org/~ghcup/0.1.40.0/x86_64-linux-ghcup-0.1.40.0 -o $HOME/.ghcup/bin/ghcup
RUN chmod a+x $HOME/.ghcup/bin/ghcup
ENV PATH=$PATH:/root/.ghcup/bin/
ENV PATH=$PATH:/root/.cabal/bin/

RUN ghcup install ghc 9.8.4
RUN ghcup install cabal 3.2
RUN ghcup set ghc 9.8.4
RUN cabal update

RUN apt-get install --yes iverilog libtcl8.6

RUN curl -L https://github.com/B-Lang-org/bsc/releases/download/2025.01.1/bsc-2025.01.1-ubuntu-22.04.tar.gz -o $HOME/bsc.tar.gz
RUN tar -zxvpf bsc.tar.gz
ENV PATH=$PATH:/root/bsc-2025.01.1-ubuntu-22.04/bin/

ADD Top.bs /root/
ADD Fibs.hs /root/
ADD Leds.bs /root/

CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \
  && cabal v1-sandbox init \
  && cabal v1-install alex happy --constraint='happy <= 2' \
  && cabal v1-install \
       $NAME/copilot/ \
       $NAME/copilot-bluespec/ \
       $NAME/copilot-c99/ \
       $NAME/copilot-core/ \
       $NAME/copilot-prettyprinter/ \
       $NAME/copilot-interpreter/ \
       $NAME/copilot-language/ \
       $NAME/copilot-libraries/ \
       $NAME/copilot-theorem/ \
  && cabal v1-exec -- runhaskell $NAME/copilot/examples/fpga/HelloWorld/HelloWorld.hs \
  && cabal v1-exec -- runhaskell Fibs.hs \
  && bsc -sim -g mkLeds -u Leds.bs \
  && bsc -sim -e mkLeds -o mkLeds \
  && [[ "$(./mkLeds -m 11 | grep -e '^Led value is: 55$' | wc -l)" -eq "10" ]] && echo "mkLeds run successfully" || exit 1 \
  && bsc -sim -g mkTop -u Top.bs \
  && bsc -sim -e mkTop -o mkTop \
  && [[ "$(./mkTop -m 11 | grep -e 'Fibonacci' | wc -l)" -eq "10" ]] && echo "mkTop run successfully" || exit 1 \
  && ./mkTop -m 11 | grep "^Odd" | awk -F: '{if ($2 % 2 != 1) exit 1}' \
  && ./mkTop -m 11 | grep "^Even" | awk -F: '{if ($2 % 2 != 0) exit 1}' \
  && bsc -verilog -g mkLeds -u Leds.bs \
  && bsc -verilog -e mkLeds -o mkLedsV \
  && [[ "$(./mkLedsV | head | grep -e '^Led value is: 55$' | wc -l)" -eq "10" ]] && echo "mkLedsV run successfully" || exit 1 \
  && bsc -verilog -g mkTop -u Top.bs \
  && bsc -verilog -e mkTop -o mkTopV \
  && [[ "$(./mkTopV | head | grep -e 'Fibonacci' | wc -l)" -eq "10" ]] && echo "mkTop run successfully" || exit 1 \
  && ./mkTopV | head | grep "^Odd" | awk -F: '{if ($2 % 2 != 1) exit 1}' \
  && ./mkTopV | head | grep "^Even" | awk -F: '{if ($2 % 2 != 0) exit 1}' \
  && echo "Success"

--- Top.bs
package Top where

import Fibs
import FibsTypes

mkTop :: Module Empty
mkTop =
  module
    fibsMod <- mkFibs
    addFibsRules fibsMod $
      interface FibsRulesIfc
        even_action x =
          $display "Even Fibonacci number: %0d" x

        odd_action x =
          $display "Odd  Fibonacci number: %0d" x

--- Fibs.hs
module Main (main) where

import qualified Prelude as P ()

import Language.Copilot
import Copilot.Compile.Bluespec

fibs :: Stream Word32
fibs = [1, 1] ++ (fibs + drop 1 fibs)

evenStream :: Stream Word32 -> Stream Bool
evenStream n = (n `mod` constant 2) == constant 0

oddStream :: Stream Word32 -> Stream Bool
oddStream n = not (evenStream n)

spec :: Spec
spec = do
  trigger "even" (evenStream fibs) [arg fibs]
  trigger "odd"  (oddStream fibs) [arg fibs]

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

--- Leds.bs
package Leds where

import HelloWorld
import HelloWorldTypes

mkLeds :: Module Empty
mkLeds =
  module
    helloMod <- mkHelloWorld
    addHelloWorldRules helloMod $
      interface HelloWorldRulesIfc
        sw_action   = return 55
        leds_action x =
          $display "Led value is: %0d" x

Command (substitute variables based on new path after merge):

$ docker run -e REPO=https://github.com/GaloisInc/copilot-1 -e NAME=copilot-1 -e COMMIT=dab5669f4459bcea5a624b4357c46552c8f40c49 copilot-verify-677

Implementation is documented. Details:
The new code includes comments, and the DESIGN.md document is updated to match new implementation.
Change history is clear.
Commit messages are clear.
Changelogs are updated.
Examples are updated. Details:
The existing example is tested by the Dockerfile; the documentation will need to be updated to reflect the new, simpler linking process.
Required version bumps are evaluated. Details:
Bump required; change modifies interface of the code produced by Bluespec backend.

RyanGlScott force-pushed the develop-hardware-friendly-bluespec branch from ec63500 to b7573e4 Compare November 3, 2025 12:34

ivanperez-keera reviewed Nov 4, 2025

View reviewed changes

copilot-bluespec/src/Copilot/Compile/Bluespec/CodeGen.hs Outdated Show resolved Hide resolved