Merge pull request #3383 from jix/write_formal_map_roms

smt2, btor: Use memory_map -rom-only to make ROMs usable for k-induction
This commit is contained in:
Jannis Harder 2022-06-17 19:08:14 +02:00 committed by GitHub
commit e6a5d84149
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 2 additions and 0 deletions

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();

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();