SimSoC-Cert, a toolkit for generating certified processor simulators See the COPYRIGHTS and LICENSE files -------------------------------------------------------------------- SimSoC-Cert is available on http://formes.asia/cms/software/simsoc-cert . The aim of SimSoC-Cert is to provide tools for: - extracting useful information (assembly syntax, instruction binary encoding, instruction semantics/pseudo-code) from the PDF documentation of various processors (ARMv6, SH4), - generating from this extracted information instructions set simulators in various programming languages (Coq, C), - automatically check in the Coq proof assistant (http://coq.inria.fr) that the generated C code is equivalent to the generated Coq code by using the semantics of C formalized in the Coq library of the CompCert project (http://compcert.inria.fr). LICENSE: this file describes the license governing this tool. COPYRIGHTS: this file describes the copyrights holders. INSTALL: this file describes a compilation procedure. THANKS: thanks to various people for their comments or help.