From b636af9751993bd35f02f56e68e63a4ef715aa4e Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 14 Feb 2023 17:09:53 +0100 Subject: chformal: Note about using -coverenable with the Verific frontend --- passes/cmds/chformal.cc | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/passes/cmds/chformal.cc b/passes/cmds/chformal.cc index c3590855b..94da4cb26 100644 --- a/passes/cmds/chformal.cc +++ b/passes/cmds/chformal.cc @@ -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"); -- cgit v1.2.3