Computer Science – Logic in Computer Science
Scientific paper
2012-02-29
Computer Science
Logic in Computer Science
First International Conference on Certified Programs and Proofs 7086 (2011)
Scientific paper
10.1007/978-3-642-25379-9_25
The simulation of Systems-on-Chip (SoC) is nowadays a hot topic because, beyond providing many debugging facilities, it allows the development of dedicated software before the hardware is available. Low-consumption CPUs such as ARM play a central role in SoC. However, the effectiveness of simulation depends on the faithfulness of the simulator. To this effect, we propose here to prove significant parts of such a simulator, SimSoC. Basically, on one hand, we develop a Coq formal model of the ARM architecture while on the other hand, we consider a version of the simulator including components written in Compcert-C. Then we prove that the simulation of ARM operations, according to Compcert-C formal semantics, conforms to the expected formal model of ARM. Size issues are partly dealt with using automatic generation of significant parts of the Coq model and of SimSoC from the official textual definition of ARM. However, this is still a long-term project. We report here the current stage of our efforts and discuss in particular the use of Compcert-C in this framework.
Blanqui Frédéric
Monin Jean-François
Shi Xiaomu
Tuong Frederic
No associations
LandOfFree
First steps towards the certification of an ARM simulator using Compcert does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with First steps towards the certification of an ARM simulator using Compcert, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and First steps towards the certification of an ARM simulator using Compcert will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-523834