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

Fix btor back-end to use "state" instead of "input" for undef init bits 

Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2019-10-02 12:48:04 +02:00
parent da347b9f7e
commit a84a2d74c7
1 changed files with 9 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
backends/btor/btor.cc
View File

@ -569,7 +569,7 @@ struct BtorWorker
int nid_init_val = -1; int nid_init_val = -1;
if (!initval.is_fully_undef()) if (!initval.is_fully_undef())
nid_init_val = get_sig_nid(initval); nid_init_val = get_sig_nid(initval, -1, false, true);
int sid = get_bv_sid(GetSize(sig_q)); int sid = get_bv_sid(GetSize(sig_q));
int nid = next_nid++; int nid = next_nid++;
@ -681,7 +681,7 @@ struct BtorWorker
{ {
if (verbose) if (verbose)
btorf("; initval = %s\n", log_signal(firstword)); btorf("; initval = %s\n", log_signal(firstword));
nid_init_val = get_sig_nid(firstword); nid_init_val = get_sig_nid(firstword, -1, false, true);
} }
else else
{ {
@ -693,8 +693,8 @@ struct BtorWorker
if (thisword.is_fully_undef()) if (thisword.is_fully_undef())
continue; continue;
Const thisaddr(i, abits); Const thisaddr(i, abits);
int nid_thisword = get_sig_nid(thisword); int nid_thisword = get_sig_nid(thisword, -1, false, true);
int nid_thisaddr = get_sig_nid(thisaddr); int nid_thisaddr = get_sig_nid(thisaddr, -1, false, true);
int last_nid_init_val = nid_init_val; int last_nid_init_val = nid_init_val;
nid_init_val = next_nid++; nid_init_val = next_nid++;
if (verbose) if (verbose)
@ -792,7 +792,7 @@ struct BtorWorker
cell_recursion_guard.erase(cell); cell_recursion_guard.erase(cell);
} }
int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false) int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false, bool is_init = false)
{ {
int nid = -1; int nid = -1;
sigmap.apply(sig); sigmap.apply(sig);
@ -823,7 +823,10 @@ struct BtorWorker
int sid = get_bv_sid(GetSize(sig)); int sid = get_bv_sid(GetSize(sig));
int nid_input = next_nid++; int nid_input = next_nid++;
btorf("%d input %d\n", nid_input, sid); if (is_init)
btorf("%d state %d\n", nid_input, sid);
else
btorf("%d input %d\n", nid_input, sid);
int nid_masked_input; int nid_masked_input;
if (sig_mask_undef.is_fully_ones()) { if (sig_mask_undef.is_fully_ones()) {