chformal: Note about using -coverenable with the Verific frontend

This commit is contained in:
Jannis Harder 2023-02-14 17:09:53 +01:00
parent 5dfad5101d
commit b636af9751
1 changed files with 5 additions and 0 deletions

View File

@ -58,6 +58,11 @@ struct ChformalPass : public Pass {
log(" -coverenable\n");
log(" add cover statements for the enable signals of the constraints\n");
log("\n");
#ifdef YOSYS_ENABLE_VERIFIC
log(" Note: For the Verific frontend it is currently not guaranteed that a\n");
log(" reachable SVA statement corresponds to an active enable signal.\n");
log("\n");
#endif
log(" -assert2assume\n");
log(" -assume2assert\n");
log(" -live2fair\n");