Merge branch 'develop-hardware-friendly-bluespec'. Close #677.

**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.

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/Copilot-Language/copilot" -e "NAME=copilot" -e "COMMIT=<HASH>" -it copilot-verify-677
```

**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.

Author: ivanperez-keera

copilot-bluespec/CHANGELOG

@@ -1,3 +1,6 @@
+2025-11-03
+        * Flip direction of interface inputs and outputs in Bluespec. (#677)
+
 2025-09-07
         * Version bump (4.5.1). (#666)