Author:
(1) David S. Hardin, Cedar Rapids, IA USA (david.s.hardin@gmail.com). Table of Links 1 Introduction 2 Dancing Links 3 The Rust Programming Language 4 RAC: Hardware/Software Co-Assurance at Scale 5 Rust and RAR 5.1 Restricted Algorithmic Rust 6 Dancing Links in Rust and 6.1 Definitions 6.2 Translation to ACL2 6.3 Dancing Links Theorems 7 Related Work 8 Conclusion 9 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. This paper is available on arxiv under CC BY 4.0 DEED license. Author: (1) David S. Hardin, Cedar Rapids, IA USA (david.s.hardin@gmail.com). Author: Author: (1) David S. Hardin, Cedar Rapids, IA USA (david.s.hardin@gmail.com). Table of Links 1 Introduction 1 Introduction 2 Dancing Links 2 Dancing Links 3 The Rust Programming Language 3 The Rust Programming Language 4 RAC: Hardware/Software Co-Assurance at Scale 4 RAC: Hardware/Software Co-Assurance at Scale 5 Rust and RAR 5 Rust and RAR 5.1 Restricted Algorithmic Rust 5.1 Restricted Algorithmic Rust 6 Dancing Links in Rust and 6.1 Definitions 6 Dancing Links in Rust and 6.1 Definitions 6.2 Translation to ACL2 6.2 Translation to ACL2 6.3 Dancing Links Theorems 6.3 Dancing Links Theorems 7 Related Work 7 Related Work 8 Conclusion 8 Conclusion 9 Acknowledgments and References 9 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. This paper is available on arxiv under CC BY 4.0 DEED license. This paper is available on arxiv under CC BY 4.0 DEED license. available on arxiv

Part of HackerNoon's growing list of open-source research papers, promoting free access to academic material.

Scaling Hardware/Software Co-Assurance with Restricted Algorithmic C

About Author

Comments

TOPICS

THIS ARTICLE WAS FEATURED IN

Related Stories

The Algorithm That Makes Data Dance—and Solve Complex Problems Fast

Why Odin Deserves a Place Beside C, Zig, and Rust in Your Toolbox

Rust Tips: Saving Collections of Trait Objects Made Easy with typetag

Getting Started with Building a Markdown Parser in Rust

Future Work in Rust Co-Assurance

Proving Theorems for Rust’s Dancing Links in ACL2

The Algorithm That Makes Data Dance—and Solve Complex Problems Fast

Why Odin Deserves a Place Beside C, Zig, and Rust in Your Toolbox

Rust Tips: Saving Collections of Trait Objects Made Easy with typetag

Getting Started with Building a Markdown Parser in Rust

Future Work in Rust Co-Assurance

Proving Theorems for Rust’s Dancing Links in ACL2

Light-Mode

Classic

Newspaper

Minty

Dark-Mode

Neon Noir

Minty

HN StartUps