diff options
| author | Jannis Harder <me@jix.one> | 2023-02-14 17:09:53 +0100 |
|---|---|---|
| committer | Jannis Harder <me@jix.one> | 2023-02-14 17:10:43 +0100 |
| commit | b636af9751993bd35f02f56e68e63a4ef715aa4e (patch) | |
| tree | 210b83acac34fdca8e73e8fb5090804d4e9cb3ed /passes | |
| parent | 5dfad5101d92edb484da2e5306cde58b8d958e7d (diff) | |
| download | yosys-b636af9751993bd35f02f56e68e63a4ef715aa4e.tar.gz yosys-b636af9751993bd35f02f56e68e63a4ef715aa4e.tar.bz2 yosys-b636af9751993bd35f02f56e68e63a4ef715aa4e.zip | |
chformal: Note about using -coverenable with the Verific frontend
Diffstat (limited to 'passes')
| -rw-r--r-- | passes/cmds/chformal.cc | 5 |
1 files changed, 5 insertions, 0 deletions
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"); |