Rust Implementation of Knuth's Dancing Links: RAC: Hardware/Software Co-Assurance at Scale

Table of Links

• Abstract and Introduction
• Dancing Links
• The Rust Programming Language
• RAC: Hardware/Software Co-Assurance at Scale
• Rust and RAR
• Dancing Links in Rust
• Related Work
• Conclusion, Acknowledgments, and References

4 RAC: Hardware/Software Co-Assurance at Scale

In order to begin to realize hardware/software co-assurance at scale, we have conducted several experiments employing a state-of-the-art toolchain, due to Russinoff and O’Leary, and originally designed for use in floating-point hardware verification [27], to determine its suitability for the creation of safetycritical/security-critical applications in various domains. Note that this toolchain has already demonstrated the capability to scale to industrial designs in the floating-point hardware design and verification domain, as it has been used in design verifications for CPU products at both Intel and Arm.

Algorithmic C [21] is a High-Level Synthesis (HLS) language, 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 to both hardware and software platforms, including support for the peculiar bit widths employed, for example, in floating-point hardware design.

The Russinoff-O’Leary Restricted Algorithmic C (RAC) toolchain, depicted in Fig. 2, translates a subset of Algorithmic C source to the Common Lisp subset supported by the ACL2 theorem prover, as augmented by Russinoff’s Register Transfer Logic (RTL) books.

The ACL2 Translator component of Fig. 2 provides a case study in the bridging of Formal Modeling and Real-World Development concerns, as summarized in Table 1. The ACL2 translator converts imperative RAC code to functional ACL2 code. Loops are translated into tail-recursive functions, with automatic generation of measure functions to guarantee admission into the logic of ACL2 (RAC subsetting rules ensure that loop measures can be automatically determined). Structs and arrays are converted into functional ACL2 records. The combination of modular arithmetic and bit-vector operations of typical RAC source code is faithfully translated to functions supported by Russinoff’s RTL books. ACL2 is able to reason about non-linear arithmetic functions, so the usual concern about formal reasoning about non-linear arithmetic functions does not apply. Finally, the RTL books are quite capable of reasoning about a combination of arithmetic and bit-vector operations, which is a very difficult feat for most automated solvers.

Recently, we have investigated the synthesis of Field-Programmable Gate Array (FPGA) hardware directly from high-level architecture models, in collaboration with colleagues at Kansas State University. The goal of this work is to enable the generation of high-assurance hardware and/or software from highlevel architectural specifications expressed in the Architecture Analysis and Design Language (AADL) [9], with proofs of correctness in ACL2.