cva6
cva6 copied to clipboard
openhwgroup
[BUG] replace FORMAL directive by VERILATOR
Is there an existing CVA6 bug for this?
- [X] I have searched the existing bug issues
Bug Description
In PMP modules, some " ifdef FORMAL " are inserted in the code to enable/disable assertions. In other cva6 modules, assertions are enabled by " ifndef VERILATOR ". Can we replace FORMAL by VERILATOR ? The goal is to uniformize the define directives to bettre drive and use them.
The FORMAL ifdef surrounds any kind of assert that was at some point checked by a formal model checker. I am not sure if verilator even compiles with FORMAL defined. I guess one option is to just remove all asserts, as no one has used the formal tool in the last few years.
Hello @Moschn @zchamski is trying to remove the VERILATOR ifndef directives from RTL. From Zbigniew, I understood that Verilator 5 supports the assert. In that case, all the directives could be removed. Zbigniew, can you keep moritz informed?
Hello @Moschn @zchamski is trying to remove the VERILATOR ifndef directives from RTL. From Zbigniew, I understood that Verilator 5 supports the assert. In that case, all the directives could be removed. Zbigniew, can you keep moritz informed?
Sure I will!
@zchamski This issue is stuck from April (of the current year fortunately). Can you provide information ?
I'm getting the issue on the front burner again. As of commit 2745f3edc there are 44 occurrences of ifndef VERILATOR in total: 23 in the core and 21 in corev_apu directories, most relating to static asserts. A notable exception is the mock_uart block which is excluded in Verilator mode using an ifndef VERILATOR.
The assertions guarded by ifndef VERILATOR come in two flavors: assert (...) and assert property (...). The support of the latter appears to be a recent addition to Verilator (corner cases were completed in VL 5.014).
Clearly, some experimentation will be needed to assess if VL v5.008 currently used is sufficient or not. If not, either an upgrade to VL v5.014 or higher will be needed, or the removal of the ìfndef`s will be split into stages (changes supported in VL v5.008, then an upgrade of Verilator and the remaining changes).