Answers to Designer Questions About RISC-V verification (Sweden)
By: Rob van Blommestein
It can certainly be said that interest in RISC-V is showing a sharp increase in design circles. It's not only that the whole idea behind open-source has made it a cost-effective alternative, but also that its ISA (instruction set architecture) is built to provide great flexibility.
You need to design a large number of properties to be able to fully verify the RISC-V design. This may take several months to complete and requires detailed knowledge of the formal tool to achieve complete coverage. There are solutions on the market that can drastically shorten this time.
Q: RISC-V is a very comprehensive design, so how can it be verified and what initial assumptions are required?
A: It is difficult to answer what the initial assumptions should be because these are different depending on the specific design.
But when it comes to verifying a huge design as a RISC-V core, the best method is to split and defeat. Focusing on the core should be the first step. This includes ensuring that nothing violates the protocols, verifying the caches separately to detect associated complexities, looking more closely at the connections between different blocks and performing "x-propagation". It is important to note that x-propagation should be performed at the block and unit level and not at the whole core during this step. Another method is to use "assume guarantee" to validate the interfaces.
[..]
As we have seen, the RISC-V offers the benefits of flexibility and adaptability, in addition to lowering the cost barrier of processors. But with these benefits comes an increased complexity that can complicate the verification process. Understanding the verification issues that may arise and how to resolve them is a necessity for any designer interested in RISC-V. We hope that the answers we have given have increased the understanding of how verification and associated tools and methods should be used to achieve a complete verification.
