Semiconductor Engineering Article: Complete Formal Verification Of RISC-V Processor IPs For Trojan-Free Trusted ICs

RISC-V processor IPs are increasingly being integrated into system-on-chip designs for a variety of applications. However, there is still a lack of dedicated functional verification solutions supporting high-integrity, trusted integrated circuits. This paper examines an efficient, novel, formal-based RISC-V processor verification methodology. The RISC-V ISA is formalized in a set of Operational SystemVerilog assertions. Each assertion is formally verified against the processor’s RTL model.
 
To read more, please visit: https://semiengineering.com/complete-formal-verification-of-risc-v-processor-ips-for-trojan-free-trusted-ics/