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

Add workaround for CBMC bug to SimpleC back-end

This commit is contained in:
Clifford Wolf 2017-05-17 21:07:54 +02:00
parent 662a047815
commit 2122ae69b3
1 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
backends/simplec/simplec.cc
View File

@ -482,7 +482,9 @@ struct SimplecWorker
string a_expr = a.wire ? util_get_bit(work->prefix + cid(a.wire->name), a.wire->width, a.offset) : a.data ? "1" : "0";
string b_expr = b.wire ? util_get_bit(work->prefix + cid(b.wire->name), b.wire->width, b.offset) : b.data ? "1" : "0";
string s_expr = s.wire ? util_get_bit(work->prefix + cid(s.wire->name), s.wire->width, s.offset) : s.data ? "1" : "0";
string expr = stringf("%s ? %s : %s", s_expr.c_str(), b_expr.c_str(), a_expr.c_str());
// casts to bool are a workaround for CBMC bug (https://github.com/diffblue/cbmc/issues/933)
string expr = stringf("%s ? (bool)%s : (bool)%s", s_expr.c_str(), b_expr.c_str(), a_expr.c_str());
log_assert(y.wire);
funct_declarations.push_back(util_set_bit(work->prefix + cid(y.wire->name), y.wire->width, y.offset, expr) +