Links table
1 Introduction
2 dance links
3 Rust programming language
4 RAC: Hardware/Software Widely Shared Assurance
Rust 5 and RAR
5.1 Constrained Algorithmic Rust
6 Dancing in Rust links and 6.1 definitions
6.2 Translation to ACL2
6.3 Theories of dance connections
7 related works
8 Conclusion
9 Acknowledgments and references
4 RAC: Hardware/Software Widely Shared Assurance
In order to begin to realize hardware/software co-assurance at scale, we have conducted several experiments using a modern toolchain, thanks to Russinoff and O’Leary, which was originally designed for use in floating-point hardware verification [27]to determine their suitability for creating safety/security sensitive applications in different domains. Note that this toolchain has already demonstrated industrial scalability in the area of floating point hardware design and verification, having been used in design verifications of CPU products at both Intel and Arm.
Algorithm c [21] It is a high-level syntax language (HLS), and is supported by hardware/software co-design environments from Mentor Graphics, e.g., Catapult [22]. Algorithmic C defines C++ header files that enable compilation for both hardware and software platforms, including support for distinct bit widths used, for example, in the design of floating-point devices.
The Russinoff-O’Leary Restricted Algorithmic C (RAC) toolchain, shown in Figure 2, translates a subset of the source C algorithm into a Common Lisp subset supported by the ACL2 theorem prover, as enhanced by Russinoff’s Register Transfer Logic (RTL) books.
The ACL2 compiler component in Figure 2 provides a case study in bridging formal modeling and real-world development concerns, as summarized in Table 1. The ACL2 compiler converts necessary RAC code into functional ACL2 code. Loops are translated into tail recursive functions, with automatic generation of scaling functions to ensure acceptance into the ACL2 logic (RAC subset rules ensure that loop scaling can be automatically determined). Structures and arrays are converted into functional ACL2 records. The set of standard arithmetic and bit-vector operations of a typical RAC source code is faithfully translated into the functions supported by Rusinov’s RTL books. ACL2 is capable of reasoning about nonlinear arithmetic functions, so the usual worry about formal reasoning about nonlinear arithmetic functions does not apply. Finally, RTL books are fully capable of reasoning about a set of arithmetic and bit-vector operations, which is very difficult for most automated solvers.
We recently studied the synthesis of field-programmable gate array (FPGA) devices directly from high-level architectural models, in collaboration with colleagues at Kansas State University. The goal of this work is to enable the creation of high-assurance hardware and/or software from high-level architectural specifications expressed in the Architectural Analysis and Design Language (AADL). [9]with proofs in ACL2.
