copilot-bluespec: Flip direction of interface in bluespec

Description

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 is the opposite of the interface that we would like users to work with, and of what other backends generate (e.g., C99).

Type

Feature: Update backend to generate code that matches other backends and requires no changes.

Additional context

None.

Requester

Sukhman Kahlon (NASA).

Method to check presence of bug

Not applicable (not a bug).

Expected result

Externs in Copilot are translated into Bluespec code that, when compiled, become inputs in Verilog. Conversely, triggers (and trigger arguments) are translated into Bluespec code that, when compiled, become outputs in Verilog.

Desired result

Externs in Copilot are translated into Bluespec code that, when compiled, become inputs in Verilog. Conversely, triggers (and trigger arguments) are translated into Bluespec code that, when compiled, become outputs in Verilog.

Proposed solution

Modify the existing Bluespec backend to perform the necessary changes in how the interface is generated, as well as any additional definitions (wires, etc.) needed. Modify the definition of the generated Bluespec interface files to match the intention.

Adjusts tests to match the updated interface.

Adjust documentation of the Bluespec backend to match.

Further notes

None.

Change Manager: Confirmed that the issue exists.

Technical Lead: Confirmed that the issue should be addressed.

@RyanGlScott

Technical Lead: Issue scheduled for fixing in Copilot 4.6.

Fix assigned to: @RyanGlScott .

copilot-bluespec: Flip direction of interface inputs and outputs in B…

copilot-bluespec: Update Copilot.Compile.Bluespec.Compile to reflect …

copilot-bluespec: Update test suite to match new input/output order. …

copilot-bluespec: Update DESIGN.md to reflect new input/output order.…

copilot-bluespec: Document changes in CHANGELOG. Refs Copilot-Languag…

copilot-bluespec: Update Copilot.Compile.Bluespec.Compile to reflect …

copilot-bluespec: Update test suite to match new input/output order. …

copilot-bluespec: Update DESIGN.md to reflect new input/output order.…

copilot-bluespec: Document changes in CHANGELOG. Refs Copilot-Languag…

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.

Change Manager: Implementation ready to be merged.

Merge branch 'develop-hardware-friendly-bluespec'. Close Copilot-Lang…

Navigation Menu

Repository navigation

`copilot-bluespec`: Flip direction of interface in bluespec #677

13 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

copilot-bluespec: Flip direction of interface in bluespec #677

Description

Activity

ivanperez-keera commented on Nov 2, 2025

ivanperez-keera commented on Nov 2, 2025

ivanperez-keera commented on Nov 2, 2025

13 remaining items

ivanperez-keera commented on Nov 8, 2025

ivanperez-keera commented on Nov 8, 2025

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

`copilot-bluespec`: Flip direction of interface in bluespec #677