SystemVerilog 2012 Parsing for RVFI

Hello, I am having a similar issue with an earlier post with the title “Support for package import (unexpected TOK_ID)”. Except that I am attempting to run the RVFI verification flow on the cv32e40x
processor, and the rtl code has some features of System Verilog 2012, which I believe is causing the ‘unexpected TOK_ID’.

It seems I need to attach a frontend that supports System Verilog 2012 in order to parse the files correctly, and I found out UHDM seems to serve that purpose. It’s not clear to me how to attach the frontend to RVFI.

I would greatly appreciate your help if you know of any related documentation I am missing, or if you see a better approach to this task. Thanks!

riscv-formal is quite tightly integrated with SBY (and Yosys by extension). There is a blog post about using riscv-formal with another tool (Synopsys) instead, and how the SBY files can be converted to achieve that. Or you could use something like yosys-slang to read the core, and use riscv-formal as normal.