Merge pull request #43 from GaloisInc/develop

Task 1 deliverable release into main

.gitignore

@@ -0,0 +1,2 @@
+*/#*#
+*/.*

.project

@@ -0,0 +1,18 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<projectDescription>
+	<name>hardens</name>
+	<comment></comment>
+	<projects>
+		<project>sysml.library</project>
+	</projects>
+	<buildSpec>
+		<buildCommand>
+			<name>org.eclipse.xtext.ui.shared.xtextBuilder</name>
+			<arguments>
+			</arguments>
+		</buildCommand>
+	</buildSpec>
+	<natures>
+		<nature>org.eclipse.xtext.ui.shared.xtextNature</nature>
+	</natures>
+</projectDescription>

Dockerfile

@@ -0,0 +1,86 @@
+FROM ubuntu:21.04
+
+ARG DEBIAN_FRONTEND=noninteractive
+
+RUN apt-get update && apt-get upgrade
+RUN apt-get install -y wget git vim python pip\
+    python3-dev software-properties-common \
+    iproute2 usbutils srecord
+
+# Yosys
+RUN apt-get install -y build-essential clang bison flex \
+	libreadline-dev gawk tcl-dev libffi-dev git \
+	graphviz xdot pkg-config python3 libboost-system-dev \
+	libboost-python-dev libboost-filesystem-dev zlib1g-dev
+RUN git clone https://github.com/YosysHQ/yosys.git /tools/yosys
+WORKDIR /tools/yosys
+RUN make -j$(nproc)
+RUN make install PREFIX=/opt
+
+# Trellis
+RUN apt-get install -y libboost-all-dev python3 python3-pip \
+    cmake openocd
+RUN git clone --recursive https://github.com/SymbiFlow/prjtrellis /tools/prjtrellis
+WORKDIR /tools/prjtrellis/libtrellis
+RUN cmake -DCMAKE_INSTALL_PREFIX=/opt .
+RUN make -j$(nproc)
+RUN make install
+ENV TRELLIS="/opt/share/trellis"
+
+# nextpnr
+RUN apt-get install -y python3-dev libboost-all-dev \
+    libeigen3-dev qtbase5-dev qtchooser qt5-qmake qtbase5-dev-tools
+RUN git clone https://github.com/YosysHQ/nextpnr.git /tools/nextpnr
+WORKDIR /tools/nextpnr
+RUN cmake . -DARCH=ecp5 -DTRELLIS_INSTALL_PREFIX=/opt
+RUN make -j$(nproc)
+RUN make install
+
+# RISCV toolchain
+RUN apt-get install -y autoconf automake autotools-dev curl libmpc-dev \
+    libmpfr-dev libgmp-dev gawk build-essential bison flex texinfo gperf \
+    libtool patchutils bc zlib1g-dev libexpat-dev
+RUN git clone --recursive https://github.com/riscv/riscv-gnu-toolchain /tools/riscv-gnu-toolchain
+WORKDIR /tools/riscv-gnu-toolchain
+RUN  ./configure --prefix=/opt/riscv --enable-multilib
+RUN export MAKEFLAGS="-j$(nproc)"
+RUN make
+RUN make linux
+ENV PATH="/opt/riscv/bin:/opt/bin:${PATH}"
+
+# ecpprog
+RUN apt-get install -y libftdi-dev
+RUN git clone https://github.com/gregdavill/ecpprog /tools/ecpprog
+WORKDIR /tools/ecpprog/ecpprog
+RUN make -j$(nproc)
+RUN make install
+
+# Iverilog
+RUN apt-get install -y iverilog
+
+# Bluespec compiler
+RUN apt-get install -y libffi7
+WORKDIR /tmp
+RUN wget https://github.com/B-Lang-org/bsc/releases/download/2021.07/bsc-2021.07-ubuntu-20.04.tar.gz
+RUN tar xvzf bsc-2021.07-ubuntu-20.04.tar.gz
+RUN mv bsc-2021.07-ubuntu-20.04 /tools/bsc-2021.07-ubuntu-20.04
+ENV PATH="/tools/bsc-2021.07-ubuntu-20.04/bin:${PATH}"
+
+# Verilator
+RUN apt-get install -y verilator
+
+# OpenFPGAloader
+RUN apt-get install -y libftdi1-2 libftdi1-dev libhidapi-libusb0 libhidapi-dev libudev-dev cmake pkg-config make g++
+RUN git clone https://github.com/trabucayre/openFPGALoader.git /tools/openFPGALoader
+WORKDIR /tools/openFPGALoader
+RUN mkdir build
+WORKDIR /tools/openFPGALoader/build
+RUN cmake ../
+RUN cmake --build .
+RUN make install
+#WORKDIR /tools/openFPGALoader
+#RUN cp 99-openfpgaloader.rules /etc/udev/rules.d/
+#RUN udevadm control --reload-rules && sudo udevadm trigger # force udev to take new rule
+#RUN usermod -a $USER -G plugdev # add user to plugdev group
+
+WORKDIR /

README.md

@@ -1,3 +1,174 @@
 # HARDENS
 
+## Copyright (C) Galois 2021
+## Principal Investigator: Joe Kiniry <[email protected]>
+## Project Lead: Andrew Bivin <[email protected]>
+## Research Engineers: Alexander Bakst <[email protected]> and Michal Podhradsky <[email protected]>
+
 Repository for the HARDENS project for the [Nuclear Regulatory Commission](https://www.nrc.gov/about-nrc.html).
+
+## Overview
+
+The goal of HARDENS is to provide to the NRC expert technical services
+in order to (1) develop a better understanding of how Model-Based
+Systems Engineering (MBSE) methods and tools can support regulatory
+reviews of adequate design and design assurance, and (2) identify any
+barriers or gaps associated with MBSE in a regulatory review of
+Digital Instrumentation and Control Systems for existing Nuclear Power
+Plants (NPPs).
+
+In the HARDENS project Galois will demonstrate to the Nuclear
+Regulatory Commission (NRC) cutting- edge capabilities in the
+model-based design, validation, and verification of safety-critical,
+mission-critical, high-assurance systems. Our demonstrator includes
+high-assurance software and hardware, includes open source RISC-V
+Central Processing Units (CPUs), and lays the groundwork for a
+high-assurance reusable product for safety critical Digital
+Instrumentation and Control Systems systems in NPPs.
+
+Details about the HARDENS project are found in our 
+[original proposal](docs/HARDENS.pdf), which was written in response 
+to the [original NRC RFP](docs/RFP.pdf).
+
+This document summarizes the current state of affairs of the project
+and demonstrator.
+
+## Task 1: Implementation
+
+As described in our proposal and the project Statement of Work, in
+Task 1 (Implementation), the first task of the HARDENS project, Galois
+will implement the system described above using both (1) highly
+integrated computer-based engineering development processes and (2)
+model-based systems engineering.  All the modules of the simple
+protection system will be modeled functionally, and one FPGA-based
+circuit card will be modeled/designed in detail. The deliverable will
+be the model-based design itself. We will use Galois’s RDE process and
+methodology to achieve this goal, as well as the V&V in Task 2.
+
+All project models---the SysMLv2 model, the executable, rigorously
+validated and formally verified Cryptol model, and the semi-formal and
+formal requirements model---are included in this release and are found
+in the `develop` branch of the repository.
+
+Also, the initial implementation of the system which runs as an
+application on a POSIX host (e.g., a Linux or macOS development
+machine or in the HARDENS Docker image) is found in the
+as-of-yet-unmerged `c-impl` branch in the HARDENS repository.  That
+implementation includes both hand-written C code conforming to the
+model-based specifications discussed above, as well as automatically
+synthesized formally verified sub-components, as described in the
+HARDENS proposal, for a small handful of critical sub-components.
+These synthesized components are generated in formally verified C
+source code and in the System Verilog HDL. The POSIX-based simulation 
+can execute both the generated C components and the generated System Verilog
+components by means of a shim library wrapping the Verilated components.
+
+Finally, we have a formally verified RISC-V CPU, called the `nerv`
+CPU, built and tested on the ECP5-5G board.  We have sketched out
+an initial three core SoC design using Bluespec SystemVerilog, but
+have not yet built that SoC for emulation or put it on the FGPA.  We
+will accomplish such early in Task 2, and cross-compile our POSIX C
+implementation to that SoC.  That ongoing work is found in the `nerv`
+branch of the repository.
+
+## Repository Structure
+
+The repository is structured as follows:
+
+- [specs](./specs) contains a domain model (`*.lando`, `*.lobot`), requirements
+  (exported from `FRET` to `RTS_requirements.json`), and a specification of the RTS architecture
+  (`*.sysml`).
+- [models](./models) contains the executable Cryptol model
+- [assets](./assets) and [docs](./docs) contain project and device documentation
+
+## Submodules
+
+This repository does not currently use any submodules.  If/when it
+does, initialize with:
+
+```
+$ git submodule init
+$ git submodule update --recursive
+```
+
+## Docker
+
+A Docker container has been built to make for easier use, evaluation,
+reusability, and repeatibility of project results.  We are adding
+tools to this container as necessary during project execution.
+
+### HARDENS Container
+
+To build and run the core HARDENS Docker image, use the `build` and
+`run` commands.
+
+```
+$ docker build -t hardens:latest .
+$ docker run --network host --privileged -v $PWD:/HARDENS -it hardens:latest
+```
+
+In order to run a long-lived Docker container for reuse, use a `docker
+run` command like the following, ensuring that you are in the right
+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
+```
+
+After running such a detacted container, attach to it for interactive
+use by running a command like:
+```
+$ docker exec -it HARDENS bash -l
+```
+
+### SysMLv2 Container
+
+To pull and use the pre-build SysMLv2 container, use the following
+`pull` command to pull the container from DockerHub.  See
+https://hub.docker.com/r/gorenje/sysmlv2-jupyter for details.
+
+```
+$ docker pull gorenje/sysmlv2-jupyter:latest
+$ docker run -d -it --name SysMLv2 --network host -v $PWD:/HARDENS gorenje/sysmlv2-jupyter:latest
+```
+
+## Lattice ECP5 evaluation board
+
+We are using an ECP5-5G FPGA board for the RTS demonstrator.
+
+Details [here](https://www.latticesemi.com/products/developmentboardsandkits/ecp5evaluationboard#_C694C444BC684AD48A3ED64C227B6455). The board uses ECP5-5G FPGA ([LFE5UM5G-85F-8BG381](https://www.latticesemi.com/en/Products/FPGAandCPLD/ECP5)) which has:
+
+- 84k LUTs
+- On-board Boot Flash – 128 Mbit Serial Peripheral Interface (SPI) Flash, with Quad read featu
+- 8 input DIP switches, 3 push buttons and 8 LEDs for demo purposes
+
+![ECP_board](assets/ecp5_top.png)
+
+### GPIO headers
+
+Headers are: J5, J8, J32, J33 and Max I_OUT for 3V3 is 1.35A
+
+J5 Pinout:
+
+* 1, 2 - VCCIO2 (Sensor 1 VIN, Sensor 2 VIN)
+* 3, 4 - H20, G19 (Sensor 1 I2C)
+* 5, 6 - GND (Sensor 1 GND, Sensor 2 GND)
+* 7, 8 - K18, J18 (Sensor 2 I2C)
+
+### LEDs:
+
+![ECP_LED](assets/ecp5_leds.png)
+
+### Switches
+
+![ECP_DIP](assets/ecp5_dip.png)
+
+### Buttons
+
+General purpose button `SW4` is connected to `P4`
+
+## Sensors/Actuators
+
+* MOSFET power control kit: https://www.sparkfun.com/products/12959
+* 12 V Latch solenoid: https://www.sparkfun.com/products/15324
+* Pressure sensor: https://www.sparkfun.com/products/11084

Toolchain.md

@@ -0,0 +1,79 @@
+# Toolchain
+
+Internal documentation explaining different pieces of the toolchain.
+
+Note that [this page](https://craigjb.com/2020/01/22/ecp5/#appendix---installing-the-symbiflow-tools) was very helpful for setting up the toolchains.
+
+## Symbiflow
+
+- https://symbiflow.readthedocs.io/en/latest/
+- https://github.com/SymbiFlow/symbiflow-arch-defs
+
+Symbiflow claims to be an umbrella tool encapsulating all the elements of Electronic Design Automation ([EDA](https://en.wikipedia.org/wiki/Electronic_design_automation)) workflow:
+
+![eda](assets/symbiflow_eda.svg)
+
+Specifically we are talking about the following tools:
+
+![tools](assets/symbiflow_parts.svg)
+
+Interestingly, Symbiflow claims to support Lattice ECP5 board, but doesn't provide any examples so the usability of Symbiflow proper is questionable.
+A brief google search also indicates that for ECP5 a combination of Yosys+Prjtrellis is used, not Symbiflow.
+
+## Yosys
+
+- https://github.com/YosysHQ/yosys
+
+Yosys is tool suite that contains a Verilog synthesis tool.  The way I understand it is that it reads multiple Verilog files, does some optimizations, and returns a single Verilog file that can be then used to generate a bitstream.
+
+## Project Trellis
+
+- https://github.com/YosysHQ/prjtrellis
+
+Project Trellis enables a fully open-source flow for ECP5 FPGAs using *Yosys* for Verilog synthesis and *nextpnr* for place and route. Project Trellis itself provides the device database and tools for bitstream creation.
+
+## nextpnr
+
+- https://github.com/YosysHQ/nextpnr
+
+nextpnr portable FPGA place and route tool.
+
+## ecpprog
+
+- https://github.com/gregdavill/ecpprog
+
+For programming the flash memory of ECP5.
+
+## Icarus Verilog
+
+- http://iverilog.icarus.com/
+
+Stricter Verilog parser than Yosys, used by the *icicle* project for validation.
+
+## Other tools
+
+### Migen, Litex
+
+- https://github.com/m-labs/migen
+- https://github.com/litex-hub
+
+High level tools for designing hardware. *Migen* lets you create hardware in Python.
+
+### Older prebuilt ECP5 toolchain 
+
+- https://github.com/xobs/ecp5-toolchain
+
+For reference only.
+
+### icicle
+
+- https://github.com/grahamedgecombe/icicle
+
+32-bit RISC-V system on chip for iCE40 and ECP5 FPGAs, has instructions for a build using Symbiflow/Yosys.
+
+```
+$ git clone https://github.com/grahamedgecombe/icicle
+$ cd icicle
+$ make BOARD=ecp5-evn syntax
+$ make BOARD=ecp5-evn
+```