Complete verification of weakly programmable IPs against their operational ISA model

This paper suggests an operational instruction set architecture (OISΛ) 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 WPfPs often implement large segments of an application algorithm corresponding to hundreds of conventional RISC instructions. The pipeline structure of a WPIP design is commonly deter mined 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.