29 - 30 October, 2019

Holiday Inn Munich City Centre

Munich, Germany

Event Details

MP Associates, Inc.
WEDNESDAY October 30, 1:15pm - 2:45pm | Forum 5
EVENT TYPE: REGULAR SESSION
SESSION 6
RISC-V and Advanced ISS
6.1Gathering 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: Frédéric Pétrot - Univ. Grenoble Alpes
 Authors: Clement Deschamps - GreenSocs Ltd & TIMA Lab, CNRS/Grenoble INP/UJF
Frédéric Pétrot - Univ. Grenoble Alpes
Mark Burton - GreenSocs Ltd
Eric Jenn - IRT Saint-Exupery
6.2Open 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.3Automate 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.