Ada & PolarFire SoC, a software and hardware alloy for Safety & Security

Ada & PolarFire SoC, a software and hardware alloy for Safety & Security



next up we have Fabian shot off from a decor as well as pure cell phone from microchip talking about well Aida on total fire so see very exciting ok can you I mean okay so I'm Fabio shoot Oh from a decor thank you and Pia from microchip is over here so today we went to present a partnership between microchip and a decor to bring a safe and secure software and hardware solution to the risk 5 ecosystem yep so first I will talk about the polar Phi also see platform and then the software development tools for me the code that you can use to develop on this platform so the polar fire SOC is based around the qualifier FPGA that we all know and love in particular for the low power consumption with a so it's combined with with risk 5 such system and ship the system and ship itself is based on erogenous architecture so there is for high performance linux linux capable cores and fifth core monitor core better suited or safety critical application if if need be one of the interesting property of this platform is the deterministic execution that you can achieve with configuration of the caches and branch prediction and of course this is very important for safety critical applications where you need worst case execution time analysis schedulability analysis and of course you want to achieve reliable real time deterministic behavior so i know that maybe software development is not every topic over here but when you know what's the point of having the best risk 5 implementation if you are your user cannot program good software for it and also probably for most of you software programming means only C and C++ and you're like well you know I'm fine with C and C++ it's ok and you maybe don't even consider changing the language as being an option so I'm not here to talk about the Stockholm Syndrome right so what I'm going to do is try to present alternative programming language and what you can get from them so this is all of the question that you should ask yourself when actually choosing a programming language and they are alternative out there today I'm going to talk about two programming languages ada in spark spark is a subset of ada for formal verification I will come back to that later these are the two programming languages that that we support that at ADA go so what what can you get when using different programming languages and in particular with data so this is just a simple C example of an API and so as you can see this is already a pretty advanced C developer because the use of type def yeah but we see we have to use pointers probably probably this value will be changed or the value pointing but it's not really clear so let's see now what what we can write with Ada and this is to show how in Ada you can have a lot of specification power for your application so the developer can really express what is really expected from the application so ada being a strongly typed language it's actually not only strongly typed there's also a lot of features too too your own type and so for instance here we are defining a floating point type we say that we expect at least 17 digits of precision and we specify a range so typically this would come from if you're using a temperature sensor the sensor has a working ranch and you can express that a new application which is important because if there's a value outside the trench it means there's a problem and you have to to fix this problem this is the high-level view but the compiler will actually pick the best hardware presentation depending on the architecture of course we can see here as well that instead of using a pointer here we just specify that the the parameter of t is an output so it's going to be changed by the program and this is one way in which in Ada you use a lot less pointers that you so another property of Ada is that you have to specify what you really mean and what you really want so again reading just this line here probably in C you won't know exactly what what what developer is really really wants to do is it is it a floating point division or is it integral division in Ada you would have to decide and specify so either you cast B to an integer and this is going to be integer division or you cast a to float and this is going to be a floating point division so there is no undefined behavior there's no guessing here everything has to be explicit and so to sum up the some of the best properties of course explaining ADA in just 12 minutes or 15 minutes is impossible task I guess what you can remember is that the the intent here is to really catch what the developers wants to do and to have a lot of specification power in the language what the specification power brings is that you actually communicate what you want to different actors in the software development process you communicate better with the other programmers that will maintain the code in in a week in a month in 20 years or whatever you communicate better with the compiler that will be able to do optimizations that will be able to select the right hardware representation for your types and you also can use these these specification during your testing campaign and last but not least all those information specification are useful for the static analysis and formal verification that I will explain later we perform a better and more accurate analysis of your of your application so going back to spark spark with a que is a subset of the ADA language that is designed for formal verification so actually it's a language and also a suite of tools that perform the automatic formal proof on your on your application so just one example of what you can get from from spark so this is the very the the first level the low level of what you can get you get the proof of absence of runtime error so for example it for example that means no division by zero no out of wound array index or buffer overflows no overflows on integral exit right cetera so which is already quite powerful so for instance in in a security context if we say ok I have a proof that there is no buffer overflow in my application this is already a very very strong property you can also with this park do programming by contract so for instance here we have an access to an array and usually in defensive code you would check if the index is within the range of your rate so that DEA doesn't act with more or less it's saying okay is the index within the range of my array with spark you export that constraint to the user of the API with the precondition and and the formal verification framework will prove that there is no instance of this happening so that the property is always verified which means you can remove the check at execution here and actually edge achieve better performances and so the let's say the highest level that you can achieve with the spark and formal verification is to prove the functional properties of your software so here we define just just a function to find the index of a value in an array and so here we clearly have expressed in in the programming language itself the requirement for this function so basically it says if the if the value is not in the array and we return -1 otherwise we return an index that the index of the value in the array and this spark will also give you a mathematical proof that the implementation of this our program respect the specification ok so last point this is different than the the formal verification but another interesting feature of Aveda so there is in the ADA language ada in spark languages there is a notion of task that is building in the language so tasks or threads or lightweight process this is really a fully integrated and part of the language and there's a a profile within this tasking it's called ravans car which is made for real-time safety critical application and so this is this can be used in different ways you can use it on Linux on Windows you can also use it on real-time operating systems such as fix works for instance we support all that and we also have a small lightweight runtime that actually implements this tasking feature on barometer and for instance so if you go to our table outside we have a demonstration of using this Hammond's car tasking on the i-5 Unleashed which is the the SOC that you will find in the polar fires and so yeah to finish so we are bringing the truth hardware and software solution so far for safety critical application in the in the risk 5 ecosystem and so I didn't talk a lot about I've talked about languages a lot not a lot about the company echo so we do software development tools so we support the idea and sparkling which is with compilers IDE formal verification static analysis code coverage etc etcetera and yeah that's it for me [Applause]

Related Posts

Leave a Reply

Your email address will not be published. Required fields are marked *