GaloisInc · podhrmic · Apr 18, 2024 · Feb 9, 2023 · Feb 9, 2023 · Feb 10, 2023
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
@@ -23,10 +23,7 @@ jobs:
       - name: Prove specs
         uses: addnab/docker-run-action@v3
         with:
-          username: ${{ secrets.ARTIFACTORY_USERNAME }}
-          password: ${{ secrets.ARTIFACTORY_PASSWORD }}
-          registry: artifactory.galois.com:5015
-          image: artifactory.galois.com:5015/hardens
+          image: galoisinc/hardens
           options: -v ${{ github.workspace }}:/HARDENS
           run: |
             make -C saw
@@ -61,18 +58,15 @@ jobs:
       - name: Build RTS and run test scenarios
         uses: addnab/docker-run-action@v3
         with:
-          username: ${{ secrets.ARTIFACTORY_USERNAME }}
-          password: ${{ secrets.ARTIFACTORY_PASSWORD }}
-          registry: artifactory.galois.com:5015
-          image: artifactory.galois.com:5015/hardens
+          image: galoisinc/hardens
           options: -v ${{ github.workspace }}:/HARDENS
           run: |
             make rts
             cd tests && 
             pip3 install -r requirements.txt &&
             RTS_DEBUG=1 QUICK=1 python3 ./run_all.py
 
-  rts_riscv_scenarios:
+  rts_riscv_build_verilator:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout repository and submodules
@@ -82,12 +76,25 @@ jobs:
       - name: Build RTS and run test scenarios
         uses: addnab/docker-run-action@v3
         with:
-          username: ${{ secrets.ARTIFACTORY_USERNAME }}
-          password: ${{ secrets.ARTIFACTORY_PASSWORD }}
-          registry: artifactory.galois.com:5015
-          image: artifactory.galois.com:5015/hardens
+          image: galoisinc/hardens
           options: -v ${{ github.workspace }}:/HARDENS
           run: |
             make rts
             PLATFORM=RV32_bare_metal make rts
-# TODO: run scenarios
+# NOTE: there is currently no way to run RISCV scenarios
+
+  rts_riscv_build_fpga:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout repository and submodules
+        uses: actions/checkout@v2
+        with:
+          submodules: recursive
+      - name: Build RTS and run test scenarios
+        uses: addnab/docker-run-action@v3
+        with:
+          image: galoisinc/hardens
+          options: -v ${{ github.workspace }}:/HARDENS
+          run: |
+            make rts
+            PLATFORM=RV32_bare_metal DEV_BOARD=LFE5UM5G_85F_EVN make rts
diff --git a/Dockerfile b/Dockerfile
@@ -32,13 +32,12 @@ RUN apt-get install -y wget git python3 pip \
     autoconf automake autotools-dev curl libmpc-dev \
     libmpfr-dev libgmp-dev texinfo gperf \
     libtool patchutils bc zlib1g-dev libexpat-dev \
-    libftdi-dev unzip \
-    cabal-install libffi7 \
+    libftdi-dev unzip libffi7 \
     libftdi1-2 libftdi1-dev libhidapi-libusb0 libhidapi-dev libudev-dev make g++ \
     libc++-dev libc++abi-dev nodejs python2 npm \
     iverilog verilator \
     vim mercurial libboost-program-options-dev \
-    texlive-full
+    texlive-full pandoc
 
 # Builder
 FROM base as builder
@@ -178,6 +177,14 @@ RUN \
 RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG}
 
 # GHC and Cabal
+RUN \
+    wget https://downloads.haskell.org/~ghcup/x86_64-linux-ghcup -O /usr/local/bin/ghcup \
+    && chmod +x /usr/local/bin/ghcup
+ENV PATH="/root/.ghcup/bin:${PATH}"
+RUN \
+    ghcup install ghc 8.10.7 \
+    && ghcup set ghc 8.10.7 \
+    && ghcup install cabal
 RUN cabal update
 
 # cryptol 2.11
@@ -186,6 +193,9 @@ ARG TAG=dfae4580e322584185235f301bc8a03b6bc19a65
 ARG REPO=https://github.com/GaloisInc/cryptol.git
 RUN git clone ${REPO} /tmp/${TOOL}
 WORKDIR /tmp/${TOOL}
+# Build fix
+RUN echo "constraints:" > cabal.project.local
+RUN echo "  parameterized-utils < 2.1.6" >> cabal.project.local
 RUN \
     git checkout ${TAG} \
     && git submodule update --init \
@@ -252,24 +262,6 @@ RUN cp build/bin/btor* /usr/local/bin/
 RUN cp deps/btor2tools/bin/btorsim /usr/local/bin/
 RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG}
 
-# cryptol-verilog
-ARG TOOL=cryptol-verilog
-COPY ${TOOL} /tmp/${TOOL}
-WORKDIR /tmp/${TOOL}
-RUN \
-    cabal v2-build \
-    && cabal v2-install --installdir=/tools
-
-# Crymp
-ARG TOOL=cryptol-codegen
-COPY ${TOOL} /tmp/${TOOL}
-WORKDIR /tmp/${TOOL}
-RUN \
-    cabal build \
-    && cabal install --installdir=/tools
-
-ENV PATH="/tools/:${PATH}"
-
 # NuSMV
 # wget https://nusmv.fbk.eu/distrib/NuSMV-2.6.0-linux64.tar.gz
 # tar xzf NuSMV-2.6.0-linux64.tar.gz
@@ -319,14 +311,32 @@ RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG}
 # RDE Refinement Finder (aka the DocumentationEnricher)
 ARG TOOL=der
 ARG TAG=0.1.5
-ARG REPO=https://github.com/GaloisInc/RDE_RF/releases/tag/v.0.1.5
+ARG REPO=https://github.com/GaloisInc/RDE_RF
 WORKDIR /tmp
-RUN wget ${REPO}/${TOOL}-${TAG}.zip
+RUN wget ${REPO}/releases/download/v.${TAG}/${TOOL}-${TAG}.zip
 RUN unzip ${TOOL}-${TAG}.zip
-RUN    mv ${TOOL}-${TAG} /tools/${TOOL}
-ENV PATH="/tools/${TOOL}/bin:${PATH}"
+RUN mv ${TOOL}-${TAG} /tools/${TOOL} && rm ${TOOL}-${TAG}.zip
+ENV PATH="/tools/${TOOL}:${PATH}"
 RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG}
 
+# cryptol-verilog
+ARG TOOL=cryptol-verilog
+COPY ${TOOL} /tmp/${TOOL}
+WORKDIR /tmp/${TOOL}
+RUN \
+    cabal v2-build \
+    && cabal v2-install --installdir=/tools
+
+# Crymp
+ARG TOOL=cryptol-codegen
+COPY ${TOOL} /tmp/${TOOL}
+WORKDIR /tmp/${TOOL}
+RUN \
+    cabal build \
+    && cabal install --installdir=/tools
+
+ENV PATH="/tools/:${PATH}"
+
 # Runner
 FROM base as runner
 COPY --from=builder /opt/ /opt/

diff --git a/Makefile b/Makefile
@@ -92,7 +92,7 @@ ifeq ($(DEV_BOARD),LFE5UM5G_85F_EVN)
 CORE_FREQ=2400000
 
 rts:
-	CORE_FREQ=$(CORE_FREQ) PROG=main make -C hardware/SoC/ prog
+	CORE_FREQ=$(CORE_FREQ) PROG=main make -C hardware/SoC/ design.svf
 
 else
 $(info Unsupported dev board!)
@@ -109,7 +109,7 @@ endif # PLATFORM=posix ?
 # Documentation
 #
 
-docs: README.pdf
+docs: README.pdf Assurance.pdf Toolchain.pdf
 
 README.pdf: README.md
 	pandoc -o README.pdf README.md
@@ -123,7 +123,7 @@ Toolchain.pdf: Toolchain.md
 clean: src_clean doc_clean
 
 doc_clean:
-	rm -f README.pdf Assurance.pdf Toolchain.md
+	rm -f README.pdf Assurance.pdf Toolchain.pdf
 
 .PHONY: rts all clean src_clean fw_clean doc_clean docs
 

diff --git a/README.md b/README.md
@@ -285,13 +285,11 @@ tools to this container as necessary during project execution.
 
 #### HARDENS Container
 
-To build and run the core HARDENS Docker image, use the
-`build_docker.sh` script and then `docker run` commands.
+To build and run the core HARDENS Docker image, use the prebuild `galoisinc/hardens:latest` image. Note that `build_docker.sh` currently does not work, as `cryptol-codegen` no longer builds. Best if you use the following command:
 
 ```
-$ ./build_docker.sh
 $ docker run --network host --privileged -v $PWD:/HARDENS -it \
-  hardens:latest
+  galoisinc/hardens:latest
 ```
 
 In order to run a long-lived Docker container for reuse, use a `docker
@@ -300,7 +298,7 @@ directory in order to bind your sandbox properly into the container.
 
 ```
 $ docker run -d -it --name HARDENS --network host --privileged \
-  -v $PWD:/HARDENS hardens:latest
+  -v $PWD:/HARDENS galoisinc/hardens:latest
 ```
 
 If you have stopped a container running and it lists as "exited" when
@@ -317,15 +315,6 @@ use by running a command like:
 $ docker exec -it HARDENS bash -l
 ```
 
-If you are *within Galois network* and *you have access rights*, you
-can download the docker image from artifactory:
-
-```bash
-$ docker pull artifactory.galois.com:5015/hardens:latest
-$ docker run --network host --privileged -v $PWD:/HARDENS -it \
-  artifactory.galois.com:5015/hardens:latest
-```
-
 The helper script `run_docker.sh` executed the above detached run
 command, using Galois's public docker HARDENS image.  The helper
 script `docker_shell.sh` runs a shell in the spawned container.

diff --git a/build_docker.sh b/build_docker.sh
@@ -20,8 +20,7 @@ while [[ $# -gt 0 ]]; do
 done
 
 # Env and settings
-DOCKER_JFROG_PATH=artifactory.galois.com:5015
-IMAGE_TAG=${DOCKER_JFROG_PATH}/hardens:latest
+IMAGE_TAG=galoisinc/hardens:latest
 
 # clone cryptol-verilog and update its submodules prior to building the docker image
 if [ -d "cryptol-verilog" ];
@@ -62,9 +61,7 @@ DOCKER_BUILDKIT=1 sudo docker build \
 
 if [ $doPush -eq 1 ]; then
     echo "Logging in to the docker repository"
-    docker login ${DOCKER_JFROG_PATH}
+    docker login
     echo "INFO: Pushing the image..."
-    docker push ${IMAGE_TAG}
-    echo "INFO: Logout from the docker repo"
-    docker logout ${DOCKER_JFROG_PATH}
+    docker push IMAGE_TAG
 fi
diff --git a/hardware/SoC/Makefile b/hardware/SoC/Makefile
@@ -38,8 +38,12 @@ else
   $(info  INFO: BLUESPEC_HOME is $(BLUESPEC_HOME))
 endif
 
+# NOTE: make sure that these values match what is in
+# https://github.com/GaloisInc/HARDENS/blob/develop/hardware/SoC/src_BSV/NervSoC.bsv#L151
+#
+# NOTE: if this much memory doesn't fit into the FPGA, you will need to adjust it downwards
 IMEMORY_SIZE ?= 0x07000
-DMEMORY_SIZE ?= 0x03000
+DMEMORY_SIZE ?= 0x07000
 
 
 # ================================================================
@@ -82,6 +86,11 @@ BSCDIRS_V = -vdir $(VERILOG_DIR)  -bdir $(BUILD_V_DIR)  -info-dir $(BUILD_V_DIR)
 
 FIRMWARE_DIR = firmware
 PROG 	?= demo
+# NOTE: this value might have to be updated for the simulated target,
+# depending on the host computer
+# 1333333 Hz *should* be OK for the FPGA target
+# See https://github.com/GaloisInc/HARDENS/blob/develop/hardware/SoC/firmware/bsp.c#L43
+# for details
 CORE_FREQ ?= 1333333
 
 dmem_contents.memhex32:

diff --git a/src/Makefile b/src/Makefile
@@ -162,7 +162,7 @@ BUILD_MSG = BUILD CC=$(CC) PLATFORM=$(PLATFORM) EXECUTION=$(EXECUTION) SELF_TEST
 
 .PHONY: all rts clean linux macos proof generate_sources generate_c generate_sv self_test_data/tests.inc.c core.c
 
-all: rts rts_no_self_test
+all: rts
 
 rts: $(SRC:.c=.o) $(EXTRA_SRC)
 	$(CC) $(CFLAGS) $(LIBS) -o $@ $^

diff --git a/src/generated/SystemVerilog/actuation_unit_impl.sv b/src/generated/SystemVerilog/actuation_unit_impl.sv
@@ -6,38 +6,38 @@ module Coincidence_2_4
     logic b;
     logic c;
     logic d;
-    // ../models/RTS/ActuationUnit.cry:60:7--60:8
+    // ../models/RTS/ActuationUnit.cry:74:7--74:8
     assign a = x[31:24] != 8'h0;
-    // ../models/RTS/ActuationUnit.cry:61:7--61:8
+    // ../models/RTS/ActuationUnit.cry:75:7--75:8
     assign b = x[23:16] != 8'h0;
-    // ../models/RTS/ActuationUnit.cry:62:7--62:8
+    // ../models/RTS/ActuationUnit.cry:76:7--76:8
     assign c = x[15:8] != 8'h0;
-    // ../models/RTS/ActuationUnit.cry:63:7--63:8
+    // ../models/RTS/ActuationUnit.cry:77:7--77:8
     assign d = x[7:0] != 8'h0;
-    // ../models/RTS/ActuationUnit.cry:57:3--57:18
+    // ../models/RTS/ActuationUnit.cry:71:3--71:18
     assign out = a & b | ((a | b) & (c | d) | c & d);
 endmodule
 module TemperatureLogic
     ( input logic [31:0] ts,
       output logic out
     );
-    // ../models/RTS/ActuationUnit.cry:44:1--44:17
+    // ../models/RTS/ActuationUnit.cry:58:1--58:17
     Coincidence_2_4 Coincidence_2_4_inst1 (.x(ts),
                                            .out(out));
 endmodule
 module PressureLogic
     ( input logic [31:0] ts,
       output logic out
     );
-    // ../models/RTS/ActuationUnit.cry:47:1--47:14
+    // ../models/RTS/ActuationUnit.cry:61:1--61:14
     Coincidence_2_4 Coincidence_2_4_inst1 (.x(ts),
                                            .out(out));
 endmodule
 module TempPressureTripOut
     ( input logic [1:0] ts,
       output logic out
     );
-    // ../models/RTS/ActuationUnit.cry:53:1--53:20
+    // ../models/RTS/ActuationUnit.cry:67:1--67:20
     assign out = ts[1] | ts[0];
 endmodule
 module Actuate_D0
@@ -48,11 +48,11 @@ module Actuate_D0
     logic [31:0] temperatureTrips;
     logic [31:0] pressureTrips;
     logic d0;
-    // ../models/RTS/ActuationUnit.cry:34:5--34:21
+    // ../models/RTS/ActuationUnit.cry:48:5--48:21
     assign temperatureTrips[31:0] = trips[95:64];
-    // ../models/RTS/ActuationUnit.cry:35:5--35:18
+    // ../models/RTS/ActuationUnit.cry:49:5--49:18
     assign pressureTrips[31:0] = trips[63:32];
-    // ../models/RTS/ActuationUnit.cry:32:5--32:7
+    // ../models/RTS/ActuationUnit.cry:46:5--46:7
     logic TemperatureLogic_out;
     TemperatureLogic TemperatureLogic_inst1 (.ts(temperatureTrips),
                                              .out(TemperatureLogic_out));
@@ -61,14 +61,14 @@ module Actuate_D0
                                        .out(PressureLogic_out));
     TempPressureTripOut TempPressureTripOut_inst1 (.ts({TemperatureLogic_out, PressureLogic_out}),
                                                    .out(d0));
-    // ../models/RTS/ActuationUnit.cry:30:1--30:11
+    // ../models/RTS/ActuationUnit.cry:44:1--44:11
     assign out = d0 | old;
 endmodule
 module SaturationLogic
     ( input logic [31:0] ts,
       output logic out
     );
-    // ../models/RTS/ActuationUnit.cry:50:1--50:16
+    // ../models/RTS/ActuationUnit.cry:64:1--64:16
     Coincidence_2_4 Coincidence_2_4_inst1 (.x(ts),
                                            .out(out));
 endmodule
@@ -79,11 +79,11 @@ module Actuate_D1
     );
     logic [31:0] saturationTrips;
     logic d1;
-    // ../models/RTS/ActuationUnit.cry:41:5--41:20
+    // ../models/RTS/ActuationUnit.cry:55:5--55:20
     assign saturationTrips[31:0] = trips[31:0];
-    // ../models/RTS/ActuationUnit.cry:40:5--40:7
+    // ../models/RTS/ActuationUnit.cry:54:5--54:7
     SaturationLogic SaturationLogic_inst1 (.ts(saturationTrips),
                                            .out(d1));
-    // ../models/RTS/ActuationUnit.cry:38:1--38:11
+    // ../models/RTS/ActuationUnit.cry:52:1--52:11
     assign out = d1 | old;
 endmodule
diff --git a/src/generated/SystemVerilog/actuator_impl.sv b/src/generated/SystemVerilog/actuator_impl.sv
@@ -2,6 +2,6 @@ module ActuateActuator
     ( input logic [1:0] inputs,
       output logic out
     );
-    // ../models/RTS/Actuator.cry:31:1--31:16
+    // ../models/RTS/Actuator.cry:45:1--45:16
     assign out = inputs[1] | inputs[0];
 endmodule