riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

write_btor: only initialize array with const value when it is fully def 

* If all addresses of an array have the same initial value, they can be
  initialized in one go in btor with the constraint that the initial
  value must be fully const and thus can't have undef bits in
This commit is contained in:
George Rennie 2024-10-09 13:48:26 +02:00
parent 038e262332
commit 6ab3931964
1 changed files with 4 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
backends/btor/btor.cc
View File

@ -832,7 +832,10 @@ struct BtorWorker
}
}
if (constword)
// If not fully defined, undef bits should be able to take a
// different value for each address so we can't initialise from
// one value (and btor2parser doesn't like it)
if (constword && firstword.is_fully_def())
{
if (verbose)
btorf("; initval = %s\n", log_signal(firstword));