BillionaireClubCollc
  • News
  • Notifications
  • Shop
  • Cart
  • Media
  • Advertise with Us
  • Profile
  • Groups
  • Games
  • My Story
  • Chat
  • Contact Us
home shop notifications more
Signin
  •  Profile
  •  Sign Out
Skip to content

Billionaire Club Co LLC

Believe It and You Will Achieve It

Primary Menu
  • Home
  • Politics
  • TSR
  • Anime
  • Michael Jordan vs.Lebron James
  • Crypto
  • Soccer
  • Dating
  • Airplanes
  • Forex
  • Tax
  • New Movies Coming Soon
  • Games
  • CRYPTO INSURANCE
  • Sport
  • MEMES
  • K-POP
  • AI
  • The Bahamas
  • Digital NoMad
  • Joke of the Day
  • RapVerse
  • Stocks
  • SPORTS BETTING
  • Glamour
  • Beauty
  • Travel
  • Celebrity Net Worth
  • TMZ
  • Lotto
  • COVD-19
  • Fitness
  • The Bible is REAL
  • OutDoor Activity
  • Lifestyle
  • Culture
  • Boxing
  • Food
  • LGBTQ
  • Poetry
  • Music
  • Misc
  • Open Source
  • NASA
  • Science
  • Natural & Holstict Med
  • Gardening
  • DYI
  • History
  • Art
  • Education
  • Pets
  • Aliens
  • Astrology
  • Farming and LiveStock
  • LAW
  • Fast & Furious
  • Fishing & Hunting
  • Health
  • Credit Repair
  • Grants
  • All things legal
  • Reality TV
  • Africa Today
  • China Today
  • "DUMB SHIT.."
  • CRYPTO INSURANCE

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

:::info
Author:
(1) David S. Hardin, Cedar Rapids, IA USA [email protected].
:::
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.
\
:::info
This paper is available on arxiv under CC 4.0 license.
:::
\

Welcome to Billionaire Club Co LLC, your gateway to a brand-new social media experience! Sign up today and dive into over 10,000 fresh daily articles and videos curated just for your enjoyment. Enjoy the ad free experience, unlimited content interactions, and get that coveted blue check verification—all for just $1 a month!

Source link

Share
What's your thought on the article, write a comment
0 Comments
×

Sign In to perform this Activity

Sign in
×

Account Frozen

Your account is frozen. You can still view content but cannot interact with it.

Please go to your settings to update your account status.

Open Profile Settings

Ads

  • Premium Billionaire128 Crop Hoodie

    $ 44.00
  • Premium Billionaire128 Women’s Crop Tee

    $ 22.50
  • Billionaire128 Liquid Gold Unisex Tank Top

    $ 33.50
  • News Social

    • Facebook
    • Twitter
    • Facebook
    • Twitter
    Copyright © 2024 Billionaire Club Co LLC. All rights reserved