diff options
Diffstat (limited to 'backends/smt2')
| -rw-r--r-- | backends/smt2/smt2.cc | 9 | ||||
| -rw-r--r-- | backends/smt2/witness.py | 156 | ||||
| -rw-r--r-- | backends/smt2/ywio.py | 5 |
3 files changed, 165 insertions, 5 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index fe50ca7f6..1ab39a405 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -458,7 +458,7 @@ struct Smt2Worker { RTLIL::SigSpec sig_a, sig_b; RTLIL::SigSpec sig_y = sigmap(cell->getPort(ID::Y)); - bool is_signed = cell->getParam(ID::A_SIGNED).as_bool(); + bool is_signed = type == 'U' ? false : cell->getParam(ID::A_SIGNED).as_bool(); int width = GetSize(sig_y); if (type == 's' || type == 'S' || type == 'd' || type == 'b') { @@ -483,6 +483,7 @@ struct Smt2Worker if (ch == 'A') processed_expr += get_bv(sig_a); else if (ch == 'B') processed_expr += get_bv(sig_b); else if (ch == 'P') processed_expr += get_bv(cell->getPort(ID::B)); + else if (ch == 'S') processed_expr += get_bv(cell->getPort(ID::S)); else if (ch == 'L') processed_expr += is_signed ? "a" : "l"; else if (ch == 'U') processed_expr += is_signed ? "s" : "u"; else processed_expr += ch; @@ -639,6 +640,9 @@ struct Smt2Worker if (cell->type == ID($xor)) return export_bvop(cell, "(bvxor A B)"); if (cell->type == ID($xnor)) return export_bvop(cell, "(bvxnor A B)"); + if (cell->type == ID($bweqx)) return export_bvop(cell, "(bvxnor A B)", 'U'); + if (cell->type == ID($bwmux)) return export_bvop(cell, "(bvor (bvand A (bvnot S)) (bvand B S))", 'U'); + if (cell->type == ID($shl)) return export_bvop(cell, "(bvshl A B)", 's'); if (cell->type == ID($shr)) return export_bvop(cell, "(bvlshr A B)", 's'); if (cell->type == ID($sshl)) return export_bvop(cell, "(bvshl A B)", 's'); @@ -994,7 +998,7 @@ struct Smt2Worker if (contains_clock && GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig))) comments.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire), clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : "")); - if (contains_clock) { + if (wire->port_input && contains_clock) { for (int i = 0; i < GetSize(sig); i++) { bool is_posedge = clock_posedge.count(sig[i]); bool is_negedge = clock_negedge.count(sig[i]); @@ -1744,7 +1748,6 @@ struct Smt2Backend : public Backend { log_push(); Pass::call(design, "bmuxmap"); Pass::call(design, "demuxmap"); - Pass::call(design, "bwmuxmap"); log_pop(); size_t argidx; diff --git a/backends/smt2/witness.py b/backends/smt2/witness.py index a1e65569d..8d0cc8112 100644 --- a/backends/smt2/witness.py +++ b/backends/smt2/witness.py @@ -110,6 +110,10 @@ class AigerMap: def __init__(self, mapfile): data = json.load(mapfile) + version = data.get("version") if isinstance(data, dict) else {} + if version != "Yosys Witness Aiger map": + raise click.ClickException(f"{mapfile.name}: unexpected file format version {version!r}") + self.latch_count = data["latch_count"] self.input_count = data["input_count"] @@ -250,5 +254,157 @@ def yw2aiw(input, mapfile, output): click.echo(f"Converted {len(inyw)} time steps.") +class BtorMap: + def __init__(self, mapfile): + self.data = data = json.load(mapfile) + + version = data.get("version") if isinstance(data, dict) else {} + if version != "Yosys Witness BTOR map": + raise click.ClickException(f"{mapfile.name}: unexpected file format version {version!r}") + + self.sigmap = WitnessSigMap() + + for mode in ("states", "inputs"): + for btor_signal_def in data[mode]: + if btor_signal_def is None: + continue + if isinstance(btor_signal_def, dict): + btor_signal_def["path"] = tuple(btor_signal_def["path"]) + else: + for chunk in btor_signal_def: + chunk["path"] = tuple(chunk["path"]) + + +@cli.command(help=""" +Convert a BTOR witness trace into a Yosys witness trace. + +This requires a Yosys witness BTOR map file as generated by 'write_btor -ywmap'. +""") +@click.argument("input", type=click.File("r")) +@click.argument("mapfile", type=click.File("r")) +@click.argument("output", type=click.File("w")) +def wit2yw(input, mapfile, output): + input_name = input.name + click.echo(f"Converting BTOR witness trace {input_name!r} to Yosys witness trace {output.name!r}...") + click.echo(f"Using Yosys witness BTOR map file {mapfile.name!r}") + btor_map = BtorMap(mapfile) + + input = filter(None, (line.split(';', 1)[0].strip() for line in input)) + + sat = next(input, None) + if sat != "sat": + raise click.ClickException(f"{input_name}: not a BTOR witness file") + + props = next(input, None) + + t = -1 + + line = next(input, None) + + frames = [] + bits = {} + + while line and not line.startswith('.'): + current_t = int(line[1:].strip()) + if line[0] == '#': + mode = "states" + elif line[0] == '@': + mode = "inputs" + else: + raise click.ClickException(f"{input_name}: unexpected data in BTOR witness file") + + if current_t > t: + t = current_t + values = WitnessValues() + array_inits = set() + frames.append(values) + + line = next(input, None) + while line and line[0] not in "#@.": + if current_t > 0 and mode == "states": + line = next(input, None) + continue + tokens = line.split() + line = next(input, None) + + btor_sig = btor_map.data[mode][int(tokens[0])] + btor_sigs = [btor_sig] + + if btor_sig is None: + continue + + if isinstance(btor_sig, dict): + addr = tokens[1] + if not addr.startswith('['): + addr = '[*]' + value = tokens[1] + else: + value = tokens[2] + if not addr.endswith(']'): + raise click.ClickException(f"{input_name}: expected address in BTOR witness file") + path = btor_sig["path"] + width = btor_sig["width"] + size = btor_sig["size"] + if addr == '[*]': + btor_sigs = [ + [{ + "path": (*path, f"\\[{addr}]"), + "width": width, + "offset": 0, + }] + for addr in range(size) + if (path, addr) not in array_inits + ] + array_inits.update((path, addr) for addr in range(size)) + else: + addr = int(addr[1:-1], 2) + + if addr < 0 or addr >= size: + raise click.ClickException(f"{input_name}: out of bounds address in BTOR witness file") + + array_inits.add((path, addr)) + btor_sig = [{ + "path": (*path, f"\\[{addr}]"), + "width": width, + "offset": 0, + }] + btor_sigs = [btor_sig] + else: + value = tokens[1] + + for btor_sig in btor_sigs: + value_bits = iter(reversed(value)) + + for chunk in btor_sig: + offset = chunk["offset"] + path = chunk["path"] + for i in range(offset, offset + chunk["width"]): + key = (path, i) + bits[key] = mode == "inputs" + values[key] = next(value_bits) + + if next(value_bits, None) is not None: + raise click.ClickException(f"{input_name}: excess bits in BTOR witness file") + + + if line is None: + raise click.ClickException(f"{input_name}: unexpected end of BTOR witness file") + if line.strip() != '.': + raise click.ClickException(f"{input_name}: unexpected data in BTOR witness file") + if next(input, None) is not None: + raise click.ClickException(f"{input_name}: unexpected trailing data in BTOR witness file") + + outyw = WriteWitness(output, 'yosys-witness wit2yw') + + outyw.signals = coalesce_signals((), bits) + for clock in btor_map.data["clocks"]: + outyw.add_clock(clock["path"], clock["offset"], clock["edge"]) + + for values in frames: + outyw.step(values) + + outyw.end_trace() + click.echo(f"Converted {outyw.t} time steps.") + if __name__ == "__main__": cli() diff --git a/backends/smt2/ywio.py b/backends/smt2/ywio.py index 8469b4162..39cfac41e 100644 --- a/backends/smt2/ywio.py +++ b/backends/smt2/ywio.py @@ -175,8 +175,9 @@ class WitnessSig: return self.sort_key < other.sort_key -def coalesce_signals(signals): - bits = {} +def coalesce_signals(signals, bits=None): + if bits is None: + bits = {} for sig in signals: for bit in sig.bits(): if sig.init_only: |