Complete Verification ofWeakly Programmable IPs against their Operational ISA Model

Conference: Zuverlässigkeit und Entwurf - 4. GMM/GI/ITG-Fachtagung
09/13/2010 - 09/15/2010 at Wildbad Kreuth, Germany

Proceedings: Zuverlässigkeit und Entwurf

Pages: 8Language: englishTyp: PDF

Personal VDE Members are entitled to a 10% discount on this title

Loitz, Sacha; Wedler, Markus; Stoffel, Dominik; Brehm, Christian; Kunz, Wolfgang; Wehn, Norbert (Department of Electrical and Computer Engineering, University of Kaiserslautern, Germany)

This paper suggests an operational instruction set architecture (OISA) model for specifying weakly programmable IPs (WPIPs). WPIPs are application-specific programmable System-on-Chip (SoC) modules such as application-specific instruction set processors (ASIPs). The individual instructions of WPIPs often implement large segments of an application algorithm corresponding to hundreds of conventional RISC instructions. The pipeline structure of a WPIP design is commonly determined by basic operations of the application algorithm. For this reason, the pipeline is designed in a bottom-up manner where the components for the individual operations are developed first. Our OISA model reflects this design style by specifying the instruction semantics in terms of predefined operations that are associated with specific pipeline stages. After creation of the OISA model a property set can be generated automatically that uniquely specifies the entire design. Moreover, the verification process used to design the OISA model explicitly reveals hardware restrictions imposing constraints on the software to be considered by the programmer.