diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 9139c2b..b0257eb 100644 --- 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,10 +58,7 @@ 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 @@ -72,7 +66,7 @@ jobs: 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 \ No newline at end of file diff --git a/Dockerfile b/Dockerfile index 8c5bdfa..1b2761f 100644 --- 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 index bb5e4a1..4ad0caf 100644 --- 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 index 249d0ab..9e080d6 100644 --- 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 index e1ad318..7a0928a 100755 --- 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 index 56ff7e5..0083a12 100644 --- 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 index 549b202..ea06595 100644 --- 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 index 6920b64..c18bb93 100644 --- a/src/generated/SystemVerilog/actuation_unit_impl.sv +++ b/src/generated/SystemVerilog/actuation_unit_impl.sv @@ -6,22 +6,22 @@ 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 @@ -29,7 +29,7 @@ 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 @@ -37,7 +37,7 @@ 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 index 6949c59..c571d15 100644 --- 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 diff --git a/src/generated/SystemVerilog/instrumentation_impl.sv b/src/generated/SystemVerilog/instrumentation_impl.sv index f11217a..50dee6e 100644 --- a/src/generated/SystemVerilog/instrumentation_impl.sv +++ b/src/generated/SystemVerilog/instrumentation_impl.sv @@ -4,7 +4,7 @@ module Is_Ch_Tripped input logic sensor_tripped, output logic out ); - // ../models/RTS/InstrumentationUnit.cry:139:1--139:14 + // ../models/RTS/InstrumentationUnit.cry:153:1--153:14 assign out = (mode == 2'h2) | (mode == 2'h1) & sensor_tripped; endmodule module Trip @@ -17,11 +17,11 @@ module Trip ); logic [31:0] v; logic [31:0] sp; - // ../models/RTS/InstrumentationUnit.cry:228:9--228:10 + // ../models/RTS/InstrumentationUnit.cry:242:9--242:10 assign v[31:0] = vals[32 * (NChannels - ch - 1) + 31-:32]; - // ../models/RTS/InstrumentationUnit.cry:229:9--229:11 + // ../models/RTS/InstrumentationUnit.cry:243:9--243:11 assign sp[31:0] = setpoints[32 * (NChannels - ch - 1) + 31-:32]; - // ../models/RTS/InstrumentationUnit.cry:227:1--227:5 + // ../models/RTS/InstrumentationUnit.cry:241:1--241:5 assign out = ch == 2'h2 ? $signed(v) < $signed(sp) : sp < v; endmodule module Generate_Sensor_Trips @@ -30,8 +30,8 @@ module Generate_Sensor_Trips input logic [NChannels * 32 - 1:0] setpoints, output logic [NChannels - 1:0] out ); - // ../models/RTS/InstrumentationUnit.cry:221:1--221:22 - // ../models/RTS/InstrumentationUnit.cry:224:5--224:76 + // ../models/RTS/InstrumentationUnit.cry:235:1--235:22 + // ../models/RTS/InstrumentationUnit.cry:238:5--238:76 Trip Trip_inst1 (.vals(vals), .setpoints(setpoints), .ch(2'h0),