-
Notifications
You must be signed in to change notification settings - Fork 1
/
dataflow.lando
143 lines (116 loc) · 5.91 KB
/
dataflow.lando
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
// Copyright 2021, 2022, 2023 Galois, Inc.
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
subsystem RTS Implementation Artifacts (Artifacts)
component Cryptol System Specification (CryptolSpec)
A specification of a model written in the Cryptol domain-specific
language (DSL), either as Literate Cryptol, which can be Cryptol
embedded in Markdown or LaTeX, or plain Cryptol. Cryptol is a strongly
typed, functional DSL for specifying and reasoning about bit-level
algorithms and their correctness properties and is mainly used to
specify cryptographic algorithms. See https://crypto.net/ for more
information.
component Cryptol Software Compiler (CryptolToC)
Multiple versions of a Cryptol software compiler exist which can
compile different subsets of the Cryptol language into implementations
and test benches written in the C, Java, and LLVM languages.
component Cryptol Hardware Compiler (CryptolToSystemVerilog)
Multiple versions of a Cryptol hardware compiler exist which can
compile different subsets of the Cryptol language into implementations
and test benches written in the VHDL, Verilog, and SystemVerilog.
component Software Implementation (Software)
A software implementation of the RTS system, encompassing the
development of software components, their integration, and
testing. This includes the implementation of algorithms, interfaces,
and protocols defined in the system specification.
component Hand-written Software Implementation (SWImpl)
inherit Hand-written Software
An implementation of software components for the RTS system, manually
coded by developers. This method focuses on achieving optimized
performance and tailored solutions for specific parts of the system.
component Synthesized Software Implementation (SynthSW)
inherit Machine-generated Software
An automated generation of software components for the RTS system,
utilizing tools and compilers to convert high-level specifications
into executable code, ensuring consistency and reducing manual errors.
component Hardware Implementation (Hardware)
The development of hardware components for the RTS system, including
design, fabrication, and testing of electronic circuits and other
hardware elements essential for the system functionality.
component Hand-written Hardware Implementation (HWImpl)
inherit Hand-written Hardware
A manual approach to hardware development for the RTS system,
involving direct design and layout of circuits and components by
hardware engineers, often for specialized or critical parts of the
system.
component Synthesized Hardware Implementation (SynthHW)
inherit Machine-generated Hardware
Automated generation of hardware components for the RTS system using
hardware description languages and synthesis tools, allowing for rapid
prototyping and consistent design implementation.
component COTS High-Assurance RV32I RISC-V CPU (CPU)
A commercially available, high-assurance implementation of the RV32I
RISC-V CPU architecture. This component provides a reliable and tested
processing unit for the RTS system, adhering to rigorous safety and
performance standards.
component CompCert Compiler (CompCert)
A formally verified compiler for the C programming language, providing
high-assurance and reliability in the compilation process, crucial for
safety-critical systems like the RTS.
component Bluespec Compiler (BSC)
A high-level compiler for hardware design, allowing for the
development of hardware components using the Bluespec language, which
offers formal verification capabilities and facilitates the creation
of high-assurance hardware systems.
component SymbiFlow Synthesizer (SymbiFlow)
An open-source toolchain for FPGA (Field-Programmable Gate Array)
hardware synthesis, supporting a variety of hardware description
languages and platforms, crucial for the flexible and robust
development of the RTS system's hardware components.
component Software Binaries (Binaries)
The compiled and executable form of the software components of the RTS
system. These binaries are the result of the compilation process and
are ready for deployment in the system.
component Demonstrator Verilog (RTL)
The Register Transfer Level (RTL) representation of the RTS system in
Verilog, providing a detailed description of the hardware components
at the logic gate level, essential for hardware synthesis and
analysis.
component FPGA Bitstream (Bitstream)
The binary configuration file used to program FPGA devices in the RTS
system. This bitstream is generated from the RTL description and is
loaded onto the FPGA to implement the hardware design.
subsystem Dataflow of RTS Implementation Artifacts (Dataflow)
This specification, which comes from the Galois HARDENS proposal,
describes the relationships between various levels of specifications,
implementations, and assurance artifacts for the HARDENS demonstrator.
indexing
proposal_figure: 3
figure_name: Dataflow of RTS Implementation Artifacts.
relation CryptolToC client CryptolSpec
relation CryptolToSystemVerilog client CryptolSpec
relation SynthSW client CryptolToC
relation SynthHW client CryptolToSystemVerilog
relation SynthHW client BSC
relation CompCert client SynthSoftImpl
relation CompCert client SoftImpl
relation BSC inherit Compiler
relation BSC client HWImpl
relation SymbiFlow client SynthHW
relation SymbiFlow client CPU
relation Binaries client CompCert
relation RTL client SymbiFLow
relation RTL contains Soft-core RISC-V CPU
relation Bitstream contains SynthHW
relation Bitstream contains CPU
relation BitStream client SymbiFlow