FORMAL VERIFICATION OF A DUAL CORE SINGLE-CYCLE RISC-V CORE WITH PART OF MEMORY SUBSYSTEM

Abstract

This paper presents the way that dual core single-cycle RISC-V processor with part of memory subsystem is verified with formal methods by using a formal tool JasperGold developed by Cadence. Basic description of design is given, alongside with basic SystemVerilog operators and verification tecniques that were used for efficent verification of the system.