22 entries tagged with #Bare-metal

Bare-metal C++ development environment for certifiable safety-critical applications

We are happy to announce the availability of GNAT Pro for C++, a versatile development environment for bare-metal targets capable of supporting different subsets of the C++ language. It constitutes the best choice for safety-critical bare-metal systems that want to reduce complexity, memory footprint and execution-time overhead, paving the way to software certification. GNAT Pro for C++ targets popular hardware in the avionics, defense, railway, and space domains: PowerPC (32 bits), x86 (64 bits), RISC-V (32/64 bits), LEON3 (32 bits) and ARM (32/64 bits).

#C++ #Safety Critical Development #Certification #Bare-metal

by Jose Ruiz

GNAT Pro Roadmap

Every year the GNAT Pro product family acquires new members and capabilities, to help our customers develop safer, more secure and more efficient code on newer hardware and software platforms. Moving forward, our goal is to offer a clear view on the future development of our technology. As part of this effort, we have made available a public roadmap for AdaCore products on our documentation platform.

by Fabien Chouteau

Embedded Ada/SPARK, There's a Shortcut

For years in this blog my colleagues and I have published examples, demos, and how-to’s on Ada/SPARK embedded (as in bare-metal) development. Most of the time, if not always, we focused on one way of doing things: to start from scratch and write everything in Ada/SPARK, from the low level drivers to the application. While this way of doing Ada/SPARK embedded will yield the best results in terms of software quality, it might not be the most efficient in all cases. In this blog post I want to present an alternative method to introduce Ada/SPARK into your embedded development projects.

#Embedded

by Pat Rogers

Task Suspension with a Timeout in Ravenscar/Jorvik

This blog entry shows how to define an abstract data type that allows tasks to block on objects of the type, waiting for resumption signals from other components, for at most a specified amount of time per object. This "timeout" capability has been available in Ada from the beginning, via select statements containing timed entry calls. But what about developers working within the Ravenscar and Jorvik tasking subsets? Select statements and timed calls are not included within either profile. This new abstraction will provide some of the functionality of timed entry calls, with an implementation consistent with the Ravenscar and Jorvik subsets.

#Ada #Tasking #Ravenscar #Jorvik #Timeouts #Timing_Event #Suspension_Object

by Roderick Chapman

SPARKNaCl with GNAT and SPARK Community 2021: Port, Proof and Performance

This post continues our adventures with SPARKNaCl - our verified SPARK version of the TweetNaCl cryptographic library. This time, we'll be looking at yet more performance improvement via proof-driven "operator narrowing", porting the library to GNAT Community 2021, and the effect that has on proof and performance of the code.

#SPARK #Cryptography #Formal Verification #Code generation #RISC-V #Security

by Roderick Chapman

Performance analysis and tuning of SPARKNaCl

This blog goes into the details of both measuring and improving the runtime performance of SPARKNaCl on a real "bare metal" embedded target, and comparing results with those for the original "TweetNaCl" C implementation.

#SPARK #Cryptography #Formal Verification #Code generation #RISC-V #Security

by Arnaud Charlet

Ada 202x support in GNAT

News from the Ada front The next revision of the Ada standard is now almost ready, so it's time for a status update on where GNAT and AdaCore stand on this front!

#GNAT #GNAT Pro #Ada 2022

by Emma Adby

Make with Ada 2020: The SmartBase - IoT Adjustable Bed

John Singleton's The SmartBase makes your existing adjustable bed safer and easier to use by adding voice control and safe (and fun!) LED underbed lighting! Additionally, this project won first place prize in the 2019/20 Make with Ada competition.

#MakewithAda #Ada #SPARK

by Jon Andrew

CuBit: A General-Purpose Operating System in SPARK/Ada

Last year, I started evaluating programming languages for a formally-verified operating system. I've been developing software for a while, but only recently began work in high integrity software development and formal methods. There are several operating system projects, like the SeL4 microkernel and the Muen separation kernel, that make use of formal verification. But I was interested in using a formally-verified language to write a general-purpose OS - an environment for abstracting the underlying hardware while acting as an arbiter for running the normal applications we're used to.

by Johannes Kliemann

Ada on the ESP8266

Not long ago, AdaCore published its LLVM frontend for GNAT. Also quite recently Espressif updated their LLVM backend to LLVM 9 which also happens to be the LLVM version of GNAT. This gave me to the idea to try out if LLVMs promise of providing modular and reusable toolchain technologies is true.

by Roderick Chapman

Proving properties of constant-time crypto code in SPARKNaCl

Over the last few months, I developed a SPARK version of the TweetNaCl cryptographic library. This was made public on GitHub in February 2020, under the 2-clause BSD licence. This blog entry goes into a bit more technical detail on one particular aspect of the project: the challenge of re-writing and verifying "constant time" algorithms using SPARK.

#SPARK #Cryptography #Formal Verification

by Boran Car

Bringing Ada To MultiZone

C is the dominant language of the embedded world, almost to the point of exclusivity. Due to its age, and its goal of being a “portable assembler”, it deliberately lacks type-safety, opening up exploit vectors. Proposed solutions are partitioning the application into smaller intercommunicating blocks, designed with the principle of least privilege in mind; and rewriting the application in a type-safe language. We believe that both approaches are complementary and want to show you how to combine separation and isolation provided by MultiZone together with iteratively rewriting parts in Ada. We will take the MultiZone SDK demo and rewrite one of the zones in Ada.

#Ada #Embedded #Embedded Development #Security #multizone #Hex-Five

by Arnaud Charlet

How Do We Use CodePeer at AdaCore

A question that our users sometimes ask us is "do you use CodePeer at AdaCore and if so, how?". The answer is yes! and this blog post will hopefully give you some insights into how we are doing it for our own needs.

#CodePeer

by Emma Adby , Fabien Chouteau

GNAT Community 2018 is here!

Calling all members of the Ada and SPARK community, we are pleased to announce that GNAT Community 2018 is here! adacore.com/download

by Rob Tice

SPARKZumo Part 2: Integrating the Arduino Build Environment Into GPS

This is part #2 of the SPARKZumo series of blog posts. This post covers the build system that was used to build the SPARKZumo project and how to automate the process in GPS.

#GPS #Python #Libadalang #Arduino #CCG

by Fabien Chouteau

There's a mini-RTOS in my language

The first thing that struck me when I started to learn about the Ada programing language was the tasking support. In Ada, creating tasks, synchronizing them, sharing access to resources, are part of the language

#Ada #Ravenscar #Embedded #STM32

by J. German Rivera

Make with Ada 2017- A "Swiss Army Knife" Watch

SummaryThe Hexiwear is an IoT wearable development board that has two NXP Kinetis microcontrollers. One is a K64F (Cortex-M4 core) for running the main embedded application software. The other one is a KW40 (Cortex M0+ core) for running a wireless connectivity stack (e.g., Bluetooth BLE or Thread). The Hexiwear board also has a rich set of peripherals, including OLED display, accelerometer, magnetometer, gryroscope, pressure sensor, temperature sensor and heart-rate sensor. This blog article describes the development of a "Swiss Army Knife" watch on the Hexiwear platform. It is a bare-metal embedded application developed 100% in Ada 2012, from the lowest level device drivers all the way up to the application-specific code, for the Hexiwear's K64F microcontroller. I developed Ada drivers for Hexiwear-specific peripherals from scratch, as they were not supported by AdaCore's Ada drivers library. Also, since I wanted to use the GNAT GPL 2017 Ada compiler but the GNAT GPL distribution did not include a port of the Ada Runtime for the Hexiwear board, I also had to port the GNAT GPL 2017 Ada runtime to the Hexiwear. All this application-independent code can be leveraged by anyone interested in developing Ada applications for the Hexiwear wearable device.

by Jonas Attertun

Make with Ada 2017: Brushless DC Motor Controller

This project involves the design of a software platform that provides a good basis when developing motor controllers for brushless DC motors (BLDC/PMSM). It consist of a basic but clean and readable implementation of a sensored field oriented control algorithm. Included is a logging feature that will simplify development and allows users to visualize what is happening. The project shows that Ada successfully can be used for a bare-metal project that requires fast execution.

#Makers #MakewithAda #STM32 #Embedded

by Pierre-Marie de Rodat , Nicolas Setton

GNAT GPL 2017 is out!

For those users of the GNAT GPL edition, we are pleased to announce the availability of the 2017 release of GNAT GPL and SPARK GPL.

#GNAT GPL

by Fabien Chouteau

Ada on the first RISC-V microcontroller

Updated July 2018

#Embedded Development #Ada #RISC-V

by Anthony Leonardo Gracio

GPS for bare-metal developers

In my previous blog article, I exposed some techniques that helped me rewrite the Crazyflie’s firmware from C into Ada and SPARK 2014, in order to improve its safety.

#GPS #Embedded Development #Makers

by Emma Adby

AdaCore attends FOSDEM

Earlier this month AdaCore attended FOSDEM in Brussels, an event focused on the use of free and open source software. Two members of our technical team presented.

#SPARK #Events