github.com/YosysHQ.yosys
1
0
Fork 0
mirror of synced 2026-02-26 08:54:54 +00:00
Code Issues Releases Wiki Activity

smt2, btor: Use memory_map -rom-only to make ROMs usable for k-induction

Browse Source 
This avoids provability regressions now that we infer more ROMs.

This fixes #3378
This commit is contained in:
Jannis Harder
2022-06-17 17:23:13 +02:00
parent ab3a9325c3
commit 4adef63cd4
2 changed files with 2 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
backends/btor/btor.cc
View File

@@ -1402,6 +1402,7 @@ struct BtorBackend : public Backend {
log_header(design, "Executing BTOR backend.\n");
log_push();
Pass::call(design, "memory_map -rom-only");
Pass::call(design, "bmuxmap");
Pass::call(design, "demuxmap");
log_pop();

1
backends/smt2/smt2.cc
View File

@@ -1609,6 +1609,7 @@ struct Smt2Backend : public Backend {
log_header(design, "Executing SMT2 backend.\n");
log_push();
Pass::call(design, "memory_map -rom-only");
Pass::call(design, "bmuxmap");
Pass::call(design, "demuxmap");
log_pop();