diff options
| author | Clifford Wolf <clifford@clifford.at> | 2016-08-21 15:56:22 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2016-08-21 15:56:22 +0200 |
| commit | 7a33b9892a7a542ca1ac0b503c4368a1721a9afb (patch) | |
| tree | 54b3bc699e12b6ce3295f11b9443d0fad1755fe6 /backends/smt2/smtbmc.py | |
| parent | cdd0b85e47d6c1718ec5c0d2d80c87af3e3bbc83 (diff) | |
| download | yosys-7a33b9892a7a542ca1ac0b503c4368a1721a9afb.tar.gz yosys-7a33b9892a7a542ca1ac0b503c4368a1721a9afb.tar.bz2 yosys-7a33b9892a7a542ca1ac0b503c4368a1721a9afb.zip | |
yosys-smtbmc: improved --dump-vlogtb handling of memories
Diffstat (limited to 'backends/smt2/smtbmc.py')
| -rw-r--r-- | backends/smt2/smtbmc.py | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index a6e8bf67a..170671483 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -200,13 +200,23 @@ def write_vlogtb_trace(steps): mems = sorted(smt.hiermems(topmod)) for mempath in mems: - mem, abits, width = smt.mem_expr(topmod, "s0", mempath) + abits, width, ports = smt.mem_info(topmod, "s0", mempath) + mem = smt.mem_expr(topmod, "s0", mempath) + + addr_expr_list = list() + for i in range(steps): + for j in range(ports): + addr_expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, j)) + + addr_list = set() + for val in smt.get_list(addr_expr_list): + addr_list.add(smt.bv2int(val)) expr_list = list() - for i in range(2**abits): + for i in addr_list: expr_list.append("(select %s #b%s)" % (mem, format(i, "0%db" % abits))) - for i, val in enumerate(smt.get_list(expr_list)): + for i, val in zip(addr_list, smt.get_list(expr_list)): val = smt.bv2bin(val) print(" UUT.%s[%d] = %d'b%s;" % (".".join(mempath), i, len(val), val), file=f) |