WEDNESDAY October 30, 13:15 - 14:45 | Forum 5
EVENT TYPE: REGULAR SESSION
Matthias Bauer - Infineon Technologies
|6.1||Gathering Memory Hierarchy Statistics in QEMU|
|Fast functional verification is the goal of Transaction Level Modeling of hardware/software systems making use of fast, dynamic binary translation based, processor models. When it comes to estimating performance figures, either higher level ana- lytical models, or lower level cycle-accurate/approximate models are generally used. However, we believe that metrics relative to the memory hierarchy can be relatively accurately acquired while working with fast processor simulators at transaction level. This, of course, sacrifices some speed for accuracy, but lets the designer work in their usual environment and the resulting model only sacrifices about 30% in terms of performance (for a single core model). In this paper, we detail our memory hierarchy modeling strategy and give preliminary simulation speed results. This work has been carried out with the co-operation of TIMA labs, GreenSocs, the IRT Saint Exupéry and Western Digital Corporation.|
|Speaker:||Mark Burton - GreenSocs SAS
|Authors:||Clement Deschamps - GreenSocs SAS & TIMA Lab, CNRS/Grenoble INP/UJF
Frédéric Pétrot - Univ. Grenoble Alpes
Mark Burton - GreenSocs SAS
Eric Jenn - IRT Saint-Exupery
|6.2||Open Source Solution for RISC-V Verification|
|The paper presents a test program generator for functional verification of RISC-V microprocessors. The generator is implemented on the base of MicroTESK framework and consists of formal specifications of RISC-V ISA and ISA-independent core. The specifications describe instructions’ syntax and semantics and can be easily modified to support more instructions (including custom extensions). The core implements techniques of instruction sequences composition and test data generation. Test programs are generated from test templates, describing the programs’ structural and behavioral properties; among generation techniques, random, combinatorial, and constraint-based ones are supported.|
|Speaker:||Alexander Kamkin - Ivannikov Institute for System Programming of the RAS
|Authors:||Mikhail Chupilko - Ivannikov Institute for System Programming of the RAS
Alexander Kamkin - Ivannikov Institute for System Programming of the RAS
Alexander Protsenko - Ivannikov Institute for System Programming of the RAS
|6.3||Automate and Accelerate RISC-V Verification by Compositional Formal Methods|
|RISC-V is an open-source instruction set architecture (ISA) initialized by UC-Berkeley. We borrow the concept of ARM’s ISA-Formal and extend a RISC-V interface called RVFI to verify the correctness of RISC-V’s ISA implementations. Our proposed work can not only automatically generate the RISC-V RV32I ISA properties for model checking but also accelerate the verification tasks to be convergent efficiently with compositional formal methods. The experimental results show that RISC-V ISA formal properties are completely auto-generated and correctly verified by Cadence JasperGold. We also detect a jalr defect in the latest version of Vscale in 7.1 hours.|
|Speaker:||Cheng-Ting Kao - National Cheng Kung Univ.
|Authors:||Yean-Ru Chen - National Cheng Kung Univ.
Cheng-Ting Kao - National Cheng Kung Univ.
Yi-Chun Kao - National Cheng Kung Univ.
Tien-Yin Cheng - National Cheng Kung Univ.
Chun-Sheng Ke - National Cheng Kung Univ.
Chia-Hao Hsu - National Cheng Kung Univ.