Semiconductor Engineering Article: Formal Verification Of RISC-V Cores

RISC-V is hot and stands at the beginning of what may be a major shift in the industry. Even a cursory review of upcoming conferences programs and recent technical articles makes that clear. While it is still early in the evolution of the processor architecture, there is certainly the potential that RISC-V will be a game-changer in the IP and semiconductor industry. As “a free and open ISA enabling a new era of processor innovation through open standard collaboration,” it directly challenges several well-established processor families. This definition comes from the RISC-V Foundation, which assumed support and evolution of RISC-V after the original development in the EECS Department at the University of California, Berkeley.
The RISC-V instruction set architecture (ISA) was designed with a large amount of configurability in terms of optional extensions such as IEEE 754-2008 floating-point support. It is not architected towards specific technologies or microarchitecture styles, thus allowing for a wide variety of implementations currently available as open-source cores. Anyone can design a core or use one in a system-on-chip (SoC) project. It is precisely this openness and wide appeal that makes thorough verification of a RISC-V core essential. With traditional processor families, there are only one or two suppliers who have been providing core and chips for many years. The suppliers are expected to verify their products, and it is unusual for SoC designers to feel that they must re-verify the cores they license.
 
To read more, please visit: https://semiengineering.com/formal-verification-of-risc-v-cores/.