Designing a CPU model: from a pseudo-formal document to fast code
Autor: | Blanqui, Fr��d��ric, Helmstetter, Claude, Joloboff, Vania, Monin, Jean-Fran��ois, Shi, Xiaomu |
---|---|
Přispěvatelé: | Formal Methods for Embedded Systems (FORMES), Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées (LIAMA), Centre de Coopération Internationale en Recherche Agronomique pour le Développement (Cirad)-Institut National de la Recherche Agronomique (INRA)-Chinese Academy of Sciences [Changchun Branch] (CAS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Institute of Automation - Chinese Academy of Sciences-Centre National de la Recherche Scientifique (CNRS)-Centre de Coopération Internationale en Recherche Agronomique pour le Développement (Cirad)-Institut National de la Recherche Agronomique (INRA)-Chinese Academy of Sciences [Changchun Branch] (CAS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Institute of Automation - Chinese Academy of Sciences-Centre National de la Recherche Scientifique (CNRS)-Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria), Université Joseph Fourier - Grenoble 1 (UJF), ANR-08-BLAN-0326-01,SIVES,A Simulation and Verification based platform for developing Embedded Systems(2009), ANR-08-BLAN-0326,SIVES,Simulation rapide et sûre de systèmes embarqués complets(2008) |
Jazyk: | angličtina |
Rok vydání: | 2011 |
Předmět: |
Software Engineering (cs.SE)
FOS: Computer and information sciences [INFO.INFO-AR]Computer Science [cs]/Hardware Architecture [cs.AR] Computer Science - Software Engineering Hardware Architecture (cs.AR) [INFO.INFO-ES]Computer Science [cs]/Embedded Systems [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] Computer Science - Hardware Architecture Hardware_REGISTER-TRANSFER-LEVELIMPLEMENTATION [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation |
Zdroj: | 3rd Workshop on: Rapid Simulation and Performance Evaluation: Methods and Tools 3rd Workshop on: Rapid Simulation and Performance Evaluation: Methods and Tools, Jan 2011, Heraklion, Greece |
Popis: | For validating low level embedded software, engineers use simulators that take the real binary as input. Like the real hardware, these full-system simulators are organized as a set of components. The main component is the CPU simulator (ISS), because it is the usual bottleneck for the simulation speed, and its development is a long and repetitive task. Previous work showed that an ISS can be generated from an Architecture Description Language (ADL). In the work reported in this paper, we generate a CPU simulator directly from the pseudo-formal descriptions of the reference manual. For each instruction, we extract the information describing its behavior, its binary encoding, and its assembly syntax. Next, after automatically applying many optimizations on the extracted information, we generate a SystemC/TLM ISS. We also generate tests for the decoder and a formal specification in Coq. Experiments show that the generated ISS is as fast and stable as our previous hand-written ISS. 3rd Workshop on: Rapid Simulation and Performance Evaluation: Methods and Tools (2011) |
Databáze: | OpenAIRE |
Externí odkaz: |