From 111085669ba3f5cdd3bf22db8774378239c49094 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Thu, 14 Dec 2023 16:42:48 +0100 Subject: [PATCH 1/3] smtbmc: Use fewer smt commands while writing .yw traces Depending on the used solver and design this can be a signficant performance improvement. --- backends/smt2/smtbmc.py | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index dd3f9ac48dc..34657be264a 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -1327,6 +1327,9 @@ def write_yw_trace(steps, index, allregs=False, filename=None): sig = yw.add_sig(word_path, overlap_start, overlap_end - overlap_start, True) mem_init_values.append((sig, overlap_bits.replace("x", "?"))) + exprs = [] + all_sigs = [] + for i, k in enumerate(steps): step_values = WitnessValues() @@ -1337,8 +1340,15 @@ def write_yw_trace(steps, index, allregs=False, filename=None): else: sigs = seqs + exprs.extend(smt.witness_net_expr(topmod, f"s{k}", sig) for sig in sigs) + + all_sigs.append(sigs) + + bvs = iter(smt.get_list(exprs)) + + for sigs in all_sigs: for sig in sigs: - value = smt.bv2bin(smt.get(smt.witness_net_expr(topmod, f"s{k}", sig))) + value = smt.bv2bin(next(bvs)) step_values[sig["sig"]] = value yw.step(step_values) From 3fab4d42ec72de70dab01ee99fd7891b74ac6d69 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Thu, 14 Dec 2023 16:44:21 +0100 Subject: [PATCH 2/3] smtbmc: Allow raw SMT-LIBv2 comamnds and expressions for --incremental --- backends/smt2/smtbmc_incremental.py | 43 +++++++++++++++++++++++++++-- 1 file changed, 40 insertions(+), 3 deletions(-) diff --git a/backends/smt2/smtbmc_incremental.py b/backends/smt2/smtbmc_incremental.py index 2be4fb6799f..1a2a4570312 100644 --- a/backends/smt2/smtbmc_incremental.py +++ b/backends/smt2/smtbmc_incremental.py @@ -194,9 +194,31 @@ def expr_yw(self, expr, smt_out): return "Bool" + def expr_smtlib(self, expr, smt_out): + self.expr_arg_len(expr, 2) + + smtlib_expr = expr[1] + sort = expr[2] + + if not isinstance(smtlib_expr, str): + raise InteractiveError( + "raw SMT-LIB expression has to be a string, " + f"got {json.dumps(smtlib_expr)}" + ) + + if not isinstance(sort, str): + raise InteractiveError( + f"raw SMT-LIB sort has to be a string, got {json.dumps(sort)}" + ) + + smt_out.append(smtlib_expr) + return sort + def expr_label(self, expr, smt_out): if len(expr) != 3: - raise InteractiveError(f'expected ["!", label, sub_expr], got {expr!r}') + raise InteractiveError( + f'expected ["!", label, sub_expr], got {json.dumps(expr)}' + ) label = expr[1] subexpr = expr[2] @@ -226,6 +248,7 @@ def expr_label(self, expr, smt_out): "or": expr_andor, "=": expr_eq, "yw": expr_yw, + "smtlib": expr_smtlib, "!": expr_label, } @@ -251,7 +274,8 @@ def expr(self, expr, smt_out, required_sort=None): ) ): raise InteractiveError( - f"required sort {json.dumps(required_sort)} found sort {json.dumps(sort)}" + f"required sort {json.dumps(required_sort)} " + f"found sort {json.dumps(sort)}" ) return sort raise InteractiveError(f"unknown expression {json.dumps(expr[0])}") @@ -287,6 +311,14 @@ def cmd_pop(self, cmd): def cmd_check(self, cmd): return smtbmc.smt_check_sat() + def cmd_smtlib(self, cmd): + command = cmd.get("command") + if not isinstance(command, str): + raise InteractiveError( + f"raw SMT-LIB command must be a string, found {json.dumps(command)}" + ) + smtbmc.smt.write(command) + def cmd_design_hierwitness(self, cmd=None): allregs = (cmd is None) or bool(cmd.get("allreges", False)) if self._cached_hierwitness[allregs] is not None: @@ -326,13 +358,17 @@ def cmd_read_yw_trace(self, cmd): map_steps = {i: int(j) for i, j in enumerate(steps)} - smtbmc.ywfile_constraints(path, constraints, map_steps=map_steps, skip_x=skip_x) + last_step = smtbmc.ywfile_constraints( + path, constraints, map_steps=map_steps, skip_x=skip_x + ) self._yw_constraints[name] = { map_steps.get(i, i): [smtexpr for cexfile, smtexpr in constraint_list] for i, constraint_list in constraints.items() } + return dict(last_step=last_step) + def cmd_ping(self, cmd): return cmd @@ -344,6 +380,7 @@ def cmd_ping(self, cmd): "push": cmd_push, "pop": cmd_pop, "check": cmd_check, + "smtlib": cmd_smtlib, "design_hierwitness": cmd_design_hierwitness, "write_yw_trace": cmd_write_yw_trace, "read_yw_trace": cmd_read_yw_trace, From 94d7c22714dad09b24321835c36ec3100f73f9d7 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Thu, 14 Dec 2023 16:45:19 +0100 Subject: [PATCH 3/3] yosys-witness: Add aiw2yw --present-only to omit unused signals --- backends/smt2/witness.py | 53 +++++++++++++++++++++++++++++++--------- 1 file changed, 41 insertions(+), 12 deletions(-) diff --git a/backends/smt2/witness.py b/backends/smt2/witness.py index a39500c2dc1..b7e25851cbb 100644 --- a/backends/smt2/witness.py +++ b/backends/smt2/witness.py @@ -183,7 +183,8 @@ def __init__(self, mapfile): @click.argument("mapfile", type=click.File("r")) @click.argument("output", type=click.File("w")) @click.option("--skip-x", help="Leave input x bits unassigned.", is_flag=True) -def aiw2yw(input, mapfile, output, skip_x): +@click.option("--present-only", help="Only include bits present in at least one time step.", is_flag=True) +def aiw2yw(input, mapfile, output, skip_x, present_only): input_name = input.name click.echo(f"Converting AIGER witness trace {input_name!r} to Yosys witness trace {output.name!r}...") click.echo(f"Using Yosys witness AIGER map file {mapfile.name!r}") @@ -211,16 +212,23 @@ def aiw2yw(input, mapfile, output, skip_x): if not re.match(r'[0]*$', ffline): raise click.ClickException(f"{input_name}: non-default initial state not supported") - outyw = WriteWitness(output, 'yosys-witness aiw2yw') + if not present_only: + outyw = WriteWitness(output, "yosys-witness aiw2yw") - for clock in aiger_map.clocks: - outyw.add_clock(clock["path"], clock["offset"], clock["edge"]) + for clock in aiger_map.clocks: + outyw.add_clock(clock["path"], clock["offset"], clock["edge"]) - for (path, offset), id in aiger_map.sigmap.bit_to_id.items(): - outyw.add_sig(path, offset, init_only=id in aiger_map.init_inputs) + for (path, offset), id in aiger_map.sigmap.bit_to_id.items(): + outyw.add_sig(path, offset, init_only=id in aiger_map.init_inputs) missing = set() + seen = set() + + buffered_steps = [] + + skip = "x?" if skip_x else "?" + t = -1 while True: inline = next(input, None) if inline is None: @@ -232,17 +240,20 @@ def aiw2yw(input, mapfile, output, skip_x): if inline.startswith("#"): continue - if not re.match(r'[01x]*$', ffline): + t += 1 + + if not re.match(r"[01x]*$", inline): raise click.ClickException(f"{input_name}: unexpected data in AIGER witness file") if len(inline) != aiger_map.input_count: raise click.ClickException( - f"{input_name}: {mapfile.name}: number of inputs does not match, " - f"{len(inline)} in witness, {aiger_map.input_count} in map file") + f"{input_name}: {mapfile.name}: number of inputs does not match, " + f"{len(inline)} in witness, {aiger_map.input_count} in map file" + ) values = WitnessValues() for i, v in enumerate(inline): - if outyw.t > 0 and i in aiger_map.init_inputs: + if v in skip or (t > 0 and i in aiger_map.init_inputs): continue try: @@ -250,11 +261,29 @@ def aiw2yw(input, mapfile, output, skip_x): except IndexError: bit = None if bit is None: - missing.insert(i) + missing.add(i) + elif present_only: + seen.add(i) values[bit] = v - outyw.step(values, skip_x=skip_x) + if present_only: + buffered_steps.append(values) + else: + outyw.step(values) + + if present_only: + outyw = WriteWitness(output, "yosys-witness aiw2yw") + + for clock in aiger_map.clocks: + outyw.add_clock(clock["path"], clock["offset"], clock["edge"]) + + for (path, offset), id in aiger_map.sigmap.bit_to_id.items(): + if id in seen: + outyw.add_sig(path, offset, init_only=id in aiger_map.init_inputs) + + for values in buffered_steps: + outyw.step(values) outyw.end_trace()