Skip to content

Commit

Permalink
Snapshots of new builds of three dependencies. Small edits to docs.
Browse files Browse the repository at this point in the history
  • Loading branch information
kiniry authored and abakst committed Feb 7, 2022
1 parent 418a653 commit 8d1d55e
Show file tree
Hide file tree
Showing 8 changed files with 43 additions and 11 deletions.
1 change: 1 addition & 0 deletions bin/crymp
Binary file added bin/crymp-Darwin-21.2.0-i386
Binary file not shown.
1 change: 1 addition & 0 deletions bin/cryptol-verilog
Binary file added bin/cryptol-verilog-Darwin-21.2.0-i386
Binary file not shown.
1 change: 1 addition & 0 deletions bin/cryptol-verilogc
Binary file added bin/cryptol-verilogc-Darwin-21.2.0-i386
Binary file not shown.
2 changes: 1 addition & 1 deletion specs/HARDENS.sysml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
49 changes: 39 additions & 10 deletions src/README.md
Original file line number Diff line number Diff line change
@@ -1,31 +1,41 @@
# 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` <https://gitlab-ext.galois.com/cryptol/cryptol-verilog>
- `crymp` <https://gitlab-ext.galois.com/cryptol/cryptol-codegen/-/tree/hardens-tweaks>
<<<<<<< HEAD
- `verilator` <https://www.veripool.org/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
<https://frama-c.com>.
=======
- `verilator` <https://www.veripool.org/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

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.
Expand Down Expand Up @@ -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
Expand All @@ -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

Expand Down

0 comments on commit 8d1d55e

Please sign in to comment.