diff --git a/bin/crymp b/bin/crymp new file mode 120000 index 0000000..44057f2 --- /dev/null +++ b/bin/crymp @@ -0,0 +1 @@ +crymp-Darwin-21.2.0-i386 \ No newline at end of file diff --git a/bin/crymp-Darwin-21.2.0-i386 b/bin/crymp-Darwin-21.2.0-i386 new file mode 100755 index 0000000..75a7c22 Binary files /dev/null and b/bin/crymp-Darwin-21.2.0-i386 differ diff --git a/bin/cryptol-verilog b/bin/cryptol-verilog new file mode 120000 index 0000000..c9384e9 --- /dev/null +++ b/bin/cryptol-verilog @@ -0,0 +1 @@ +cryptol-verilog-Darwin-21.2.0-i386 \ No newline at end of file diff --git a/bin/cryptol-verilog-Darwin-21.2.0-i386 b/bin/cryptol-verilog-Darwin-21.2.0-i386 new file mode 100755 index 0000000..a872df9 Binary files /dev/null and b/bin/cryptol-verilog-Darwin-21.2.0-i386 differ diff --git a/bin/cryptol-verilogc b/bin/cryptol-verilogc new file mode 120000 index 0000000..0b210a7 --- /dev/null +++ b/bin/cryptol-verilogc @@ -0,0 +1 @@ +cryptol-verilogc-Darwin-21.2.0-i386 \ No newline at end of file diff --git a/bin/cryptol-verilogc-Darwin-21.2.0-i386 b/bin/cryptol-verilogc-Darwin-21.2.0-i386 new file mode 100755 index 0000000..35d1c44 Binary files /dev/null and b/bin/cryptol-verilogc-Darwin-21.2.0-i386 differ diff --git a/specs/HARDENS.sysml b/specs/HARDENS.sysml index 8acaf03..4006e84 100644 --- a/specs/HARDENS.sysml +++ b/specs/HARDENS.sysml @@ -675,7 +675,7 @@ package 'RTS Hardware Artifacts' { // end: PCB; // } // connection: DevMachineToDevBoard connect 'Developer Machine' to Board; -} +//} /** * All requirements that the RTS system must fulfill, as driven by the diff --git a/src/README.md b/src/README.md index ffddb48..e301cbc 100644 --- a/src/README.md +++ b/src/README.md @@ -1,24 +1,33 @@ # RTS implementation sources -This directory contains the source (both hand-written and generated, `C` and -`SystemVerilog`) for the reactor trip system: +This directory contains the source (both hand-written and generated, +`C` and `SystemVerilog`) for the reactor trip system: - The root directory contains hand-written `C` sources -- [](./generated_csrc) contains `C` sources generated from the `Cryptol` model -- [](./generated_vsrc) contains `SystemVerilog` sources generated from the `Cryptol` model +- [](./generated_csrc) contains `C` sources generated from the + `Cryptol` model +- [](./generated_vsrc) contains `SystemVerilog` sources generated from + the `Cryptol` model ## Dependencies -Besides a normal `clang` toolchain, the `Makefile` targets depend on the following tools: +Besides a normal `clang` toolchain, the `Makefile` targets depend on +the following tools: - `cryptol-verilogc` - `crymp` +<<<<<<< HEAD - `verilator` *Note* on macOS (tested on 11.6.1) it seems there is an issue with recent versions: version 4.108 seems to work. Verification with `frama-c` additionally requires `frama-c` version 24.0 . +======= +- `verilator` *Note* on macOS + (tested on 11.6.1) it seems there is an issue with recent versions: + version 4.108 seems to work. +>>>>>>> 46b6c90 (Snapshots of new builds of three dependencies. Small edits to docs.) ## Implementation status @@ -26,6 +35,7 @@ The RTS can be built for simulation on a macOS or Linux host, or (not yet implemented) on a NERV-based SoC. ### Simulation Targets +<<<<<<< HEAD The `Makefile` in this directory can generate simulation builds of the `RTS` that execute on the host system, controllable via the command-line/stdin. @@ -57,8 +67,25 @@ The simulation build can be configured to accept user input for sensor values (s - `make SENSORS= rts` will build a simulator that allows the user to provide sensor values (`V #I #C #V`) sets channel `#C` of division `#I` to `#V` +======= -An example of how to script the system is given in [](tests/sense_actuate_0); you can execute +The `Makefile` in this directory can generate simulation builds of the +`RTS` that execute on the host system, controllable via the +command-line/stdin. + +The simulation build can be configured to accept user input for sensor +values (see [](tests/sense_actuate_0) or to generate a "random walk" +of sensor values. This is controlled via the `SENSORS` build flag: +>>>>>>> 46b6c90 (Snapshots of new builds of three dependencies. Small edits to docs.) + +- `make SENSORS=Simulated rts` will build a simulator that generates + random temperature/pressure data; +- `make SENSORS=rts` will build a simulator that allows the user to + provide sensor values (`V #I #C #V`) sets channel `#C` of division + `#I` to `#V` + +An example of how to script the system is given in +[](tests/sense_actuate_0); you can execute ``` sh cat tests/sense_actuate_0 | ./rts.posix @@ -68,11 +95,13 @@ to run the script. ### Notes and Current Limitations -- Currently the simulator build does *not* model failure or other exceptional conditions. +- Currently the simulator build does *not* model failure or other + exceptional conditions. - The self-test functionality is not yet implemented. -- Hand-written equivalents of the generated `C` and `SystemVerilog` are not yet included. -- The build system does not yet support mixing implementations of different components. - +- Hand-written equivalents of the generated `C` and `SystemVerilog` + are not yet included. +- The build system does not yet support mixing implementations of + different components. ## Building