From 6d3b5aa9602ff130f21a9513c3b079346d67b9e0 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 10 Jan 2023 15:33:18 +0100 Subject: [PATCH 1/4] Unified trace generation using yosys's sim across all engines Currently opt-in using the `fst` or `vcd_sim` options. --- sbysrc/sby_core.py | 240 ++++++++++++++++++++++-- sbysrc/sby_design.py | 88 ++++++++- sbysrc/sby_engine_abc.py | 80 ++------ sbysrc/sby_engine_aiger.py | 78 +++++--- sbysrc/sby_engine_btor.py | 70 ++++--- sbysrc/sby_engine_smtbmc.py | 124 +++++++----- sbysrc/sby_mode_bmc.py | 1 - sbysrc/sby_mode_cover.py | 1 - sbysrc/sby_mode_prove.py | 1 - sbysrc/sby_sim.py | 96 ++++++++++ tests/keepgoing/keepgoing_multi_step.py | 4 +- tests/keepgoing/keepgoing_same_step.py | 2 +- tests/keepgoing/keepgoing_smtc.py | 2 +- tests/unsorted/btor_meminit.sby | 48 +++++ tests/unsorted/cover_unreachable.sby | 34 ++++ 15 files changed, 686 insertions(+), 183 deletions(-) create mode 100644 sbysrc/sby_sim.py create mode 100644 tests/unsorted/btor_meminit.sby create mode 100644 tests/unsorted/cover_unreachable.sby diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 317c958..c91561f 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -20,6 +20,9 @@ import os, re, sys, signal, platform, click if os.name == "posix": import resource, fcntl import subprocess +from dataclasses import dataclass, field +from collections import defaultdict +from typing import Optional from shutil import copyfile, copytree, rmtree from select import select from time import monotonic, localtime, sleep, strftime @@ -100,7 +103,7 @@ class SbyProc: dep.register_dep(self) self.output_callback = None - self.exit_callback = None + self.exit_callbacks = [] self.error_callback = None if self.task.timeout_reached: @@ -112,6 +115,9 @@ class SbyProc: else: self.notify.append(next_proc) + def register_exit_callback(self, callback): + self.exit_callbacks.append(callback) + def log(self, line): if line is not None and (self.noprintregex is None or not self.noprintregex.match(line)): if self.logfile is not None: @@ -130,8 +136,8 @@ class SbyProc: return if self.logfile is not None: self.logfile.close() - if self.exit_callback is not None: - self.exit_callback(retcode) + for callback in self.exit_callbacks: + callback(retcode) def handle_error(self, retcode): if self.terminated: @@ -602,6 +608,199 @@ class SbyTaskloop: for task in self.tasks: task.exit_callback() +@dataclass +class SbySummaryEvent: + engine_idx: int + trace: Optional[str] = field(default=None) + path: Optional[str] = field(default=None) + hdlname: Optional[str] = field(default=None) + type: Optional[str] = field(default=None) + src: Optional[str] = field(default=None) + step: Optional[int] = field(default=None) + prop: Optional[SbyProperty] = field(default=None) + engine_case: Optional[str] = field(default=None) + + @property + def engine(self): + return f"engine_{self.engine_idx}" + +@dataclass +class SbyTraceSummary: + trace: str + path: Optional[str] = field(default=None) + engine_case: Optional[str] = field(default=None) + events: dict = field(default_factory=lambda: defaultdict(lambda: defaultdict(list))) + + @property + def kind(self): + if '$assert' in self.events: + kind = 'counterexample trace' + elif '$cover' in self.events: + kind = 'cover trace' + else: + kind = 'trace' + return kind + +@dataclass +class SbyEngineSummary: + engine_idx: int + traces: dict = field(default_factory=dict) + status: Optional[str] = field(default=None) + unreached_covers: Optional[list] = field(default=None) + + @property + def engine(self): + return f"engine_{self.engine_idx}" + +class SbySummary: + def __init__(self, task): + self.task = task + self.timing = [] + self.lines = [] + + self.engine_summaries = {} + self.traces = defaultdict(dict) + self.engine_status = {} + self.unreached_covers = None + + def append(self, line): + self.lines.append(line) + + def extend(self, lines): + self.lines.extend(lines) + + def engine_summary(self, engine_idx): + if engine_idx not in self.engine_summaries: + self.engine_summaries[engine_idx] = SbyEngineSummary(engine_idx) + return self.engine_summaries[engine_idx] + + def add_event(self, *args, **kwargs): + event = SbySummaryEvent(*args, **kwargs) + if event.prop: + if event.type == "$assert": + event.prop.status = "FAIL" + if event.path: + event.prop.tracefiles.append(event.path) + if event.prop: + if event.type == "$cover": + event.prop.status = "PASS" + if event.path: + event.prop.tracefiles.append(event.path) + + engine = self.engine_summary(event.engine_idx) + + if event.trace not in engine.traces: + engine.traces[event.trace] = SbyTraceSummary(event.trace, path=event.path, engine_case=event.engine_case) + + if event.type: + by_type = engine.traces[event.trace].events[event.type] + if event.hdlname: + by_type[event.hdlname].append(event) + + def set_engine_status(self, engine_idx, status, case=None): + engine_summary = self.engine_summary(engine_idx) + if case is None: + self.task.log(f"{click.style(f'engine_{engine_idx}', fg='magenta')}: Status returned by engine: {status}") + self.engine_summary(engine_idx).status = status + else: + self.task.log(f"{click.style(f'engine_{engine_idx}.{case}', fg='magenta')}: Status returned by engine for {case}: {status}") + if engine_summary.status is None: + engine_summary.status = {} + engine_summary.status[case] = status + + def summarize(self, short): + omitted_excess = False + for line in self.timing: + yield line + + for engine_idx, engine_cmd in self.task.engine_list(): + engine_cmd = ' '.join(engine_cmd) + trace_limit = 5 + prop_limit = 5 + step_limit = 5 + engine = self.engine_summary(engine_idx) + if isinstance(engine.status, dict): + for case, status in sorted(engine.status.items()): + yield f"{engine.engine} ({engine_cmd}) returned {status} for {case}" + elif engine.status: + yield f"{engine.engine} ({engine_cmd}) returned {engine.status}" + else: + yield f"{engine.engine} ({engine_cmd}) did not return a status" + + produced_traces = False + + for i, (trace_name, trace) in enumerate(sorted(engine.traces.items())): + if short and i == trace_limit: + excess = len(engine.traces) - trace_limit + omitted_excess = True + yield f"and {excess} further trace{'s' if excess != 1 else ''}" + break + case_suffix = f" [{trace.engine_case}]" if trace.engine_case else "" + if trace.path: + if short: + yield f"{trace.kind}{case_suffix}: {self.task.workdir}/{trace.path}" + else: + yield f"{trace.kind}{case_suffix}: {trace.path}" + else: + yield f"{trace.kind}{case_suffix}: <{trace.trace}>" + produced_traces = True + for event_type, events in sorted(trace.events.items()): + if event_type == '$assert': + desc = "failed assertion" + short_desc = 'assertion' + elif event_type == '$cover': + desc = "reached cover statement" + short_desc = 'cover statement' + elif event_type == '$assume': + desc = "violated assumption" + short_desc = 'assumption' + else: + continue + for j, (hdlname, same_events) in enumerate(sorted(events.items())): + if short and j == prop_limit: + excess = len(events) - prop_limit + yield f" and {excess} further {short_desc}{'s' if excess != 1 else ''}" + break + + event = same_events[0] + steps = sorted(e.step for e in same_events) + if short and len(steps) > step_limit: + steps = [str(step) for step in steps[:step_limit]] + excess = len(steps) - step_limit + omitted_excess = True + steps[-1] += f" and {excess} further step{'s' if excess != 1 else ''}" + + steps = f"step{'s' if len(steps) > 1 else ''} {', '.join(map(str, steps))}" + yield f" {desc} {event.hdlname} at {event.src} in {steps}" + + if not produced_traces: + yield f"{engine.engine} did not produce any traces" + + if self.unreached_covers is None and self.task.opt_mode == 'cover' and self.task.status != "PASS" and self.task.design: + self.unreached_covers = [] + for prop in self.task.design.hierarchy: + if prop.type == prop.Type.COVER and prop.status == "UNKNOWN": + self.unreached_covers.append(prop) + + if self.unreached_covers: + yield f"unreached cover statements:" + for j, prop in enumerate(self.unreached_covers): + if short and j == prop_limit: + excess = len(self.unreached_covers) - prop_limit + omitted_excess = True + yield f" and {excess} further propert{'ies' if excess != 1 else 'y'}" + break + yield f" {prop.hdlname} at {prop.location}" + + for line in self.lines: + yield line + + if omitted_excess: + yield f"see {self.task.workdir}/{self.task.status} for a complete summary" + def __iter__(self): + yield from self.summarize(True) + + class SbyTask(SbyConfig): def __init__(self, sbyconfig, workdir, early_logs, reusedir, taskloop=None, logfile=None): @@ -644,7 +843,7 @@ class SbyTask(SbyConfig): ru = resource.getrusage(resource.RUSAGE_CHILDREN) self.start_process_time = ru.ru_utime + ru.ru_stime - self.summary = list() + self.summary = SbySummary(self) self.logfile = logfile or open(f"{workdir}/logfile.txt", "a") self.log_targets = [sys.stdout, self.logfile] @@ -696,6 +895,15 @@ class SbyTask(SbyConfig): for target in self.log_targets: click.echo(line, file=target) + def log_prefix(self, prefix, message=None): + prefix = f"{click.style(prefix, fg='magenta')}: " + def log(message): + self.log(f"{prefix}{message}") + if message is None: + return log + else: + log(message) + def error(self, logmessage): tm = localtime() self.log(click.style(f"ERROR: {logmessage}", fg="red", bold=True)) @@ -833,7 +1041,7 @@ class SbyTask(SbyConfig): def instance_hierarchy_error_callback(retcode): self.precise_prop_status = False - proc.exit_callback = instance_hierarchy_callback + proc.register_exit_callback(instance_hierarchy_callback) proc.error_callback = instance_hierarchy_error_callback return [proc] @@ -891,8 +1099,8 @@ class SbyTask(SbyConfig): print("delete -output", file=f) print("dffunmap", file=f) print("stat", file=f) - print("write_btor {}-i design_{m}.info design_{m}.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f) - print("write_btor -s {}-i design_{m}_single.info design_{m}_single.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f) + print("write_btor {}-i design_{m}.info -ywmap design_btor.ywb design_{m}.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f) + print("write_btor -s {}-i design_{m}_single.info -ywmap design_btor_single.ywb design_{m}_single.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f) proc = SbyProc( self, @@ -967,6 +1175,8 @@ class SbyTask(SbyConfig): if new_status == "PASS": assert self.status != "FAIL" self.status = "PASS" + if self.opt_mode in ("bmc", "prove") and self.design: + self.design.pass_unknown_asserts() elif new_status == "FAIL": assert self.status != "PASS" @@ -1004,11 +1214,17 @@ class SbyTask(SbyConfig): self.handle_int_option("timeout", None) self.handle_bool_option("vcd", True) + self.handle_bool_option("vcd_sim", False) + self.handle_bool_option("fst", False) self.handle_str_option("smtc", None) self.handle_int_option("skip", None) self.handle_str_option("tbtop", None) + if self.opt_mode != "live": + self.handle_int_option("append", 0) + self.handle_bool_option("append_assume", False) + self.handle_str_option("make_model", None) def setup_procs(self, setupmode): @@ -1078,18 +1294,18 @@ class SbyTask(SbyConfig): # TODO process time is incorrect when running in parallel - self.summary = [ + self.summary.timing = [ "Elapsed clock time [H:MM:SS (secs)]: {}:{:02d}:{:02d} ({})".format (total_clock_time // (60*60), (total_clock_time // 60) % 60, total_clock_time % 60, total_clock_time), "Elapsed process time [H:MM:SS (secs)]: {}:{:02d}:{:02d} ({})".format (total_process_time // (60*60), (total_process_time // 60) % 60, total_process_time % 60, total_process_time), - ] + self.summary + ] else: - self.summary = [ + self.summary.timing = [ "Elapsed clock time [H:MM:SS (secs)]: {}:{:02d}:{:02d} ({})".format (total_clock_time // (60*60), (total_clock_time // 60) % 60, total_clock_time % 60, total_clock_time), "Elapsed process time unvailable on Windows" - ] + self.summary + ] for line in self.summary: if line.startswith("Elapsed"): @@ -1110,7 +1326,7 @@ class SbyTask(SbyConfig): def write_summary_file(self): with open(f"{self.workdir}/{self.status}", "w") as f: - for line in self.summary: + for line in self.summary.summarize(short=False): click.echo(line, file=f) def print_junit_result(self, f, junit_ts_name, junit_tc_name, junit_format_strict=False): diff --git a/sbysrc/sby_design.py b/sbysrc/sby_design.py index 399ea11..88b6395 100644 --- a/sbysrc/sby_design.py +++ b/sbysrc/sby_design.py @@ -16,9 +16,37 @@ # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. # -import json +import json, re from enum import Enum, auto from dataclasses import dataclass, field +from typing import Optional, Tuple + + +addr_re = re.compile(r'\\\[[0-9]+\]$') +public_name_re = re.compile(r"\\([a-zA-Z_][a-zA-Z0-9_]*(\[[0-9]+\])?|\[[0-9]+\])$") + +def pretty_name(id): + if public_name_re.match(id): + return id.lstrip("\\") + else: + return id + +def pretty_path(path): + out = "" + for name in path: + name = pretty_name(name) + if name.startswith("["): + out += name + continue + if out: + out += "." + if name.startswith("\\") or name.startswith("$"): + out += name + " " + else: + out += name + + return out + @dataclass class SbyProperty: @@ -44,18 +72,36 @@ class SbyProperty: raise ValueError("Unknown property type: " + name) name: str + path: Tuple[str, ...] type: Type location: str hierarchy: str status: str = field(default="UNKNOWN") - tracefile: str = field(default="") + tracefiles: str = field(default_factory=list) + + @property + def tracefile(self): + if self.tracefiles: + return self.tracefiles[0] + else: + return "" + + @property + def celltype(self): + return f"${str(self.type).lower()}" + + @property + def hdlname(self): + return pretty_path(self.path).rstrip() + def __repr__(self): - return f"SbyProperty<{self.type} {self.name} at {self.location}: status={self.status}, tracefile=\"{self.tracefile}\">" + return f"SbyProperty<{self.type} {self.name} {self.path} at {self.location}: status={self.status}, tracefile=\"{self.tracefile}\">" @dataclass class SbyModule: name: str + path: Tuple[str, ...] type: str submodules: dict = field(default_factory=dict) properties: list = field(default_factory=list) @@ -105,15 +151,32 @@ class SbyDesign: hierarchy: SbyModule = None memory_bits: int = 0 forall: bool = False + properties_by_path: dict = field(default_factory=dict) + + def pass_unknown_asserts(self): + for prop in self.hierarchy: + if prop.type == prop.Type.ASSERT and prop.status == "UNKNOWN": + prop.status = "PASS" + + +def cell_path(cell): + path = cell["attributes"].get("hdlname") + if path is None: + if cell["name"].startswith('$'): + return (cell["name"],) + else: + return ("\\" + cell["name"],) + else: + return tuple(f"\\{segment}" for segment in path.split()) def design_hierarchy(filename): design = SbyDesign(hierarchy=None) design_json = json.load(filename) - def make_mod_hier(instance_name, module_name, hierarchy=""): + def make_mod_hier(instance_name, module_name, hierarchy="", path=()): # print(instance_name,":", module_name) sub_hierarchy=f"{hierarchy}/{instance_name}" if hierarchy else instance_name - mod = SbyModule(name=instance_name, type=module_name) + mod = SbyModule(name=instance_name, path=path, type=module_name) for m in design_json["modules"]: if m["name"] == module_name: @@ -129,11 +192,17 @@ def design_hierarchy(filename): location = cell["attributes"]["src"] except KeyError: location = "" - p = SbyProperty(name=cell["name"], type=SbyProperty.Type.from_cell(sort["type"]), location=location, hierarchy=sub_hierarchy) + p = SbyProperty( + name=cell["name"], + path=(*path, *cell_path(cell)), + type=SbyProperty.Type.from_cell(sort["type"]), + location=location, + hierarchy=sub_hierarchy) mod.properties.append(p) if sort["type"][0] != '$' or sort["type"].startswith("$paramod"): for cell in sort["cells"]: - mod.submodules[cell["name"]] = make_mod_hier(cell["name"], sort["type"], hierarchy=sub_hierarchy) + mod.submodules[cell["name"]] = make_mod_hier( + cell["name"], sort["type"], sub_hierarchy, (*path, *cell_path(cell))) if sort["type"] in ["$mem", "$mem_v2"]: for cell in sort["cells"]: design.memory_bits += int(cell["parameters"]["WIDTH"], 2) * int(cell["parameters"]["SIZE"], 2) @@ -145,7 +214,10 @@ def design_hierarchy(filename): for m in design_json["modules"]: attrs = m["attributes"] if "top" in attrs and int(attrs["top"]) == 1: - design.hierarchy = make_mod_hier(m["name"], m["name"]) + design.hierarchy = make_mod_hier(m["name"], m["name"], "", (m["name"],)) + + for prop in design.hierarchy: + design.properties_by_path[prop.path[1:]] = prop return design else: raise ValueError("Cannot find top module") diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py index 47224d8..1cb84b5 100644 --- a/sbysrc/sby_engine_abc.py +++ b/sbysrc/sby_engine_abc.py @@ -16,8 +16,9 @@ # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. # -import re, os, getopt, click +import re, getopt from sby_core import SbyProc +from sby_engine_aiger import aigsmt_exit_callback def run(mode, task, engine_idx, engine): abc_opts, abc_command = getopt.getopt(engine[1:], "", []) @@ -46,6 +47,21 @@ def run(mode, task, engine_idx, engine): else: task.error(f"Invalid ABC command {abc_command[0]}.") + smtbmc_vcd = task.opt_vcd and not task.opt_vcd_sim + run_aigsmt = smtbmc_vcd or (task.opt_append and task.opt_append_assume) + smtbmc_append = 0 + sim_append = 0 + log = task.log_prefix(f"engine_{engine_idx}") + + if task.opt_append_assume: + smtbmc_append = task.opt_append + elif smtbmc_vcd: + if not task.opt_append_assume: + log("For VCDs generated by smtbmc the option 'append_assume off' is ignored") + smtbmc_append = task.opt_append + else: + sim_append = task.opt_append + proc = SbyProc( task, f"engine_{engine_idx}", @@ -79,64 +95,8 @@ def run(mode, task, engine_idx, engine): return line def exit_callback(retcode): - if proc_status is None: - task.error(f"engine_{engine_idx}: Could not determine engine status.") - - task.update_status(proc_status) - task.log(f"{click.style(f'engine_{engine_idx}', fg='magenta')}: Status returned by engine: {proc_status}") - task.summary.append(f"""engine_{engine_idx} ({" ".join(engine)}) returned {proc_status}""") - - task.terminate() - - if proc_status == "FAIL" and task.opt_aigsmt != "none": - trace_prefix = f"engine_{engine_idx}/trace" - - smtbmc_opts = [] - smtbmc_opts += ["-s", task.opt_aigsmt] - if task.opt_tbtop is not None: - smtbmc_opts += ["--vlogtb-top", task.opt_tbtop] - smtbmc_opts += ["--noprogress", f"--append {task.opt_append}"] - if task.opt_vcd: - smtbmc_opts += [f"--dump-vcd {trace_prefix}.vcd"] - smtbmc_opts += [f"--dump-yw {trace_prefix}.yw", f"--dump-vlogtb {trace_prefix}_tb.v", f"--dump-smtc {trace_prefix}.smtc"] - - witness_proc = SbyProc( - task, f"engine_{engine_idx}", [], - f"cd {task.workdir}; {task.exe_paths['witness']} aiw2yw engine_{engine_idx}/trace.aiw model/design_aiger.ywa engine_{engine_idx}/trace.yw", - ) - - proc2 = SbyProc( - task, - f"engine_{engine_idx}", - [*task.model("smt2"), witness_proc], - f"cd {task.workdir}; {task.exe_paths['smtbmc']} {' '.join(smtbmc_opts)} --yw engine_{engine_idx}/trace.yw model/design_smt2.smt2", - logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w") - ) - - proc2_status = None - - def output_callback2(line): - nonlocal proc2_status - - match = re.match(r"^## [0-9: ]+ Status: FAILED", line) - if match: proc2_status = "FAIL" - - match = re.match(r"^## [0-9: ]+ Status: PASSED", line) - if match: proc2_status = "PASS" - - return line - - def exit_callback2(retcode): - if proc2_status is None: - task.error(f"engine_{engine_idx}: Could not determine aigsmt status.") - if proc2_status != "FAIL": - task.error(f"engine_{engine_idx}: Unexpected aigsmt status.") - - if os.path.exists(f"{task.workdir}/engine_{engine_idx}/trace.vcd"): - task.summary.append(f"counterexample trace: {task.workdir}/engine_{engine_idx}/trace.vcd") - - proc2.output_callback = output_callback2 - proc2.exit_callback = exit_callback2 + aigsmt_exit_callback(task, engine_idx, proc_status, + run_aigsmt=run_aigsmt, smtbmc_vcd=smtbmc_vcd, smtbmc_append=smtbmc_append, sim_append=sim_append, ) proc.output_callback = output_callback - proc.exit_callback = exit_callback + proc.register_exit_callback(exit_callback) diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index 18cb876..d6e14d8 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/sbysrc/sby_engine_aiger.py @@ -18,6 +18,7 @@ import re, os, getopt, click from sby_core import SbyProc +from sby_sim import sim_witness_trace def run(mode, task, engine_idx, engine): opts, solver_args = getopt.getopt(engine[1:], "", []) @@ -51,6 +52,22 @@ def run(mode, task, engine_idx, engine): else: task.error(f"Invalid solver command {solver_args[0]}.") + smtbmc_vcd = task.opt_vcd and not task.opt_vcd_sim + run_aigsmt = (mode != "live") and (smtbmc_vcd or (task.opt_append and task.opt_append_assume)) + smtbmc_append = 0 + sim_append = 0 + log = task.log_prefix(f"engine_{engine_idx}") + + if mode != "live": + if task.opt_append_assume: + smtbmc_append = task.opt_append + elif smtbmc_vcd: + if not task.opt_append_assume: + log("For VCDs generated by smtbmc the option 'append_assume off' is ignored") + smtbmc_append = task.opt_append + else: + sim_append = task.opt_append + proc = SbyProc( task, f"engine_{engine_idx}", @@ -92,44 +109,48 @@ def run(mode, task, engine_idx, engine): return None def exit_callback(retcode): + aiw_file.close() + aigsmt_exit_callback(task, engine_idx, proc_status, + run_aigsmt=run_aigsmt, smtbmc_vcd=smtbmc_vcd, smtbmc_append=smtbmc_append, sim_append=sim_append, ) + + proc.output_callback = output_callback + proc.register_exit_callback(exit_callback) + + +def aigsmt_exit_callback(task, engine_idx, proc_status, *, run_aigsmt, smtbmc_vcd, smtbmc_append, sim_append): if proc_status is None: task.error(f"engine_{engine_idx}: Could not determine engine status.") - aiw_file.close() - task.update_status(proc_status) - task.log(f"{click.style(f'engine_{engine_idx}', fg='magenta')}: Status returned by engine: {proc_status}") - task.summary.append(f"""engine_{engine_idx} ({" ".join(engine)}) returned {proc_status}""") - + task.summary.set_engine_status(engine_idx, proc_status) task.terminate() - if proc_status == "FAIL" and task.opt_aigsmt != "none": - if produced_cex: - trace_prefix = f"engine_{engine_idx}/trace" + if proc_status == "FAIL" and (not run_aigsmt or task.opt_aigsmt != "none"): + trace_prefix = f"engine_{engine_idx}/trace" + aiw2yw_suffix = '_aiw' if run_aigsmt else '' + + witness_proc = SbyProc( + task, f"engine_{engine_idx}", [], + f"cd {task.workdir}; {task.exe_paths['witness']} aiw2yw engine_{engine_idx}/trace.aiw model/design_aiger.ywa engine_{engine_idx}/trace{aiw2yw_suffix}.yw", + ) + yw_proc = witness_proc + + if run_aigsmt: smtbmc_opts = [] - if mode == "live": - smtbmc_opts += ["-g"] smtbmc_opts += ["-s", task.opt_aigsmt] if task.opt_tbtop is not None: smtbmc_opts += ["--vlogtb-top", task.opt_tbtop] - smtbmc_opts += ["--noprogress"] - if mode != "live": - smtbmc_opts += [f"--append {task.opt_append}"] - if task.opt_vcd: + smtbmc_opts += ["--noprogress", f"--append {smtbmc_append}"] + if smtbmc_vcd: smtbmc_opts += [f"--dump-vcd {trace_prefix}.vcd"] smtbmc_opts += [f"--dump-yw {trace_prefix}.yw", f"--dump-vlogtb {trace_prefix}_tb.v", f"--dump-smtc {trace_prefix}.smtc"] - witness_proc = SbyProc( - task, f"engine_{engine_idx}", [], - f"cd {task.workdir}; {task.exe_paths['witness']} aiw2yw engine_{engine_idx}/trace.aiw model/design_aiger.ywa engine_{engine_idx}/trace.yw", - ) - proc2 = SbyProc( task, f"engine_{engine_idx}", [*task.model("smt2"), witness_proc], - f"cd {task.workdir}; {task.exe_paths['smtbmc']} {' '.join(smtbmc_opts)} --yw engine_{engine_idx}/trace.yw model/design_smt2.smt2", + f"cd {task.workdir}; {task.exe_paths['smtbmc']} {' '.join(smtbmc_opts)} --yw engine_{engine_idx}/trace{aiw2yw_suffix}.yw model/design_smt2.smt2", logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w") ) @@ -146,20 +167,21 @@ def run(mode, task, engine_idx, engine): return line - def exit_callback2(line): + def exit_callback2(retcode): if proc2_status is None: task.error(f"engine_{engine_idx}: Could not determine aigsmt status.") - if proc2_status != ("PASS" if mode == "live" else "FAIL"): + if proc2_status != "FAIL": task.error(f"engine_{engine_idx}: Unexpected aigsmt status.") - if os.path.exists(f"{task.workdir}/engine_{engine_idx}/trace.vcd"): - task.summary.append(f"counterexample trace: {task.workdir}/engine_{engine_idx}/trace.vcd") + task.summary.add_event(engine_idx, trace="trace", path=f"engine_{engine_idx}/trace.vcd", type="$assert") proc2.output_callback = output_callback2 - proc2.exit_callback = exit_callback2 + proc2.register_exit_callback(exit_callback2) + + yw_proc = proc2 + + if task.opt_fst or (task.opt_vcd and task.opt_vcd_sim): + sim_witness_trace(f"engine_{engine_idx}", task, engine_idx, f"engine_{engine_idx}/trace.yw", append=sim_append, deps=[yw_proc]) else: task.log(f"{click.style(f'engine_{engine_idx}', fg='magenta')}: Engine did not produce a counter example.") - - proc.output_callback = output_callback - proc.exit_callback = exit_callback diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py index 284a49e..a3e744e 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -19,6 +19,7 @@ import re, os, getopt, click from types import SimpleNamespace from sby_core import SbyProc +from sby_sim import sim_witness_trace def run(mode, task, engine_idx, engine): random_seed = None @@ -54,14 +55,27 @@ def run(mode, task, engine_idx, engine): else: task.error(f"Invalid solver command {solver_args[0]}.") + log = task.log_prefix(f"engine_{engine_idx}") + + btorsim_vcd = task.opt_vcd and not task.opt_vcd_sim + run_sim = task.opt_fst or not btorsim_vcd + sim_append = 0 + + if task.opt_append and btorsim_vcd: + log("The BTOR engine does not support the 'append' option when using btorsim.") + else: + sim_append = task.opt_append + + if task.opt_append and task.opt_append_assume: + log("The BTOR engine does not support enforcing assumptions in appended time steps.") + + common_state = SimpleNamespace() common_state.solver_status = None common_state.produced_cex = 0 common_state.expected_cex = 1 common_state.wit_file = None common_state.assert_fail = False - common_state.produced_traces = [] - common_state.print_traces_max = 5 common_state.running_procs = 0 def print_traces_and_terminate(): @@ -87,17 +101,7 @@ def run(mode, task, engine_idx, engine): task.error(f"engine_{engine_idx}: Engine terminated without status.") task.update_status(proc_status.upper()) - task.log(f"{click.style(f'engine_{engine_idx}', fg='magenta')}: Status returned by engine: {proc_status}") - task.summary.append(f"""engine_{engine_idx} ({" ".join(engine)}) returned {proc_status}""") - - if len(common_state.produced_traces) == 0: - task.log(f"""{click.style(f'engine_{engine_idx}', fg='magenta')}: Engine did not produce a{" counter" if mode != "cover" else "n "}example.""") - elif len(common_state.produced_traces) <= common_state.print_traces_max: - task.summary.extend(common_state.produced_traces) - else: - task.summary.extend(common_state.produced_traces[:common_state.print_traces_max]) - excess_traces = len(common_state.produced_traces) - common_state.print_traces_max - task.summary.append(f"""and {excess_traces} further trace{"s" if excess_traces > 1 else ""}""") + task.summary.set_engine_status(engine_idx, proc_status) task.terminate() @@ -113,9 +117,9 @@ def run(mode, task, engine_idx, engine): def make_exit_callback(suffix): def exit_callback2(retcode): - vcdpath = f"{task.workdir}/engine_{engine_idx}/trace{suffix}.vcd" - if os.path.exists(vcdpath): - common_state.produced_traces.append(f"""{"" if mode == "cover" else "counterexample "}trace: {vcdpath}""") + vcdpath = f"engine_{engine_idx}/trace{suffix}.vcd" + if os.path.exists(f"{task.workdir}/{vcdpath}"): + task.summary.add_event(engine_idx=engine_idx, trace=f'trace{suffix}', path=vcdpath, type="$cover" if mode == "cover" else "$assert") common_state.running_procs -= 1 if (common_state.running_procs == 0): @@ -123,6 +127,11 @@ def run(mode, task, engine_idx, engine): return exit_callback2 + def simple_exit_callback(retcode): + common_state.running_procs -= 1 + if (common_state.running_procs == 0): + print_traces_and_terminate() + def output_callback(line): if mode == "cover": if solver_args[0] == "btormc": @@ -153,20 +162,39 @@ def run(mode, task, engine_idx, engine): else: suffix = common_state.produced_cex - if mode == "cover" or task.opt_vcd: + model = f"design_btor{'_single' if solver_args[0] == 'pono' else ''}" + + yw_proc = SbyProc( + task, f"engine_{engine_idx}.trace{suffix}", [], + f"cd {task.workdir}; {task.exe_paths['witness']} wit2yw engine_{engine_idx}/trace{suffix}.wit model/{model}.ywb engine_{engine_idx}/trace{suffix}.yw", + ) + common_state.running_procs += 1 + yw_proc.register_exit_callback(simple_exit_callback) + + btorsim_vcd = (task.opt_vcd and not task.opt_vcd_sim) + + if btorsim_vcd: # TODO cover runs btorsim not only for trace generation, can we run it without VCD generation in that case? proc2 = SbyProc( task, - f"engine_{engine_idx}_{common_state.produced_cex}", + f"engine_{engine_idx}.trace{suffix}", task.model("btor"), - "cd {dir} ; btorsim -c --vcd engine_{idx}/trace{i}.vcd --hierarchical-symbols --info model/design_btor{s}.info model/design_btor{s}.btor engine_{idx}/trace{i}.wit".format(dir=task.workdir, idx=engine_idx, i=suffix, s='_single' if solver_args[0] == 'pono' else ''), + "cd {dir} ; btorsim -c --vcd engine_{idx}/trace{i}{i2}.vcd --hierarchical-symbols --info model/design_btor{s}.info model/design_btor{s}.btor engine_{idx}/trace{i}.wit".format(dir=task.workdir, idx=engine_idx, i=suffix, i2='' if btorsim_vcd else '_btorsim', s='_single' if solver_args[0] == 'pono' else ''), logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w") ) proc2.output_callback = output_callback2 - proc2.exit_callback = make_exit_callback(suffix) + if run_sim: + proc2.register_exit_callback(simple_exit_callback) + else: + proc2.register_exit_callback(make_exit_callback(suffix)) proc2.checkretcode = True common_state.running_procs += 1 + if run_sim: + sim_proc = sim_witness_trace(f"engine_{engine_idx}", task, engine_idx, f"engine_{engine_idx}/trace{suffix}.yw", append=sim_append, deps=[yw_proc]) + sim_proc.register_exit_callback(simple_exit_callback) + common_state.running_procs += 1 + common_state.produced_cex += 1 common_state.wit_file.close() common_state.wit_file = None @@ -226,5 +254,5 @@ def run(mode, task, engine_idx, engine): if solver_args[0] == "pono": proc.retcodes = [0, 1, 255] # UNKNOWN = -1, FALSE = 0, TRUE = 1, ERROR = 2 proc.output_callback = output_callback - proc.exit_callback = exit_callback + proc.register_exit_callback(exit_callback) common_state.running_procs += 1 diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index 6c19268..c5f348e 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -16,8 +16,9 @@ # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. # -import re, os, getopt, click +import re, os, getopt, click, glob from sby_core import SbyProc +from sby_sim import sim_witness_trace def run(mode, task, engine_idx, engine): smtbmc_opts = [] @@ -141,20 +142,37 @@ def run(mode, task, engine_idx, engine): if not progress: smtbmc_opts.append("--noprogress") - if task.opt_skip is not None: t_opt = "{}:{}".format(task.opt_skip, task.opt_depth) else: t_opt = "{}".format(task.opt_depth) + smtbmc_vcd = task.opt_vcd and not task.opt_vcd_sim + + smtbmc_append = 0 + sim_append = 0 + + log = task.log_prefix(f"engine_{engine_idx}") + + if task.opt_append_assume: + smtbmc_append = task.opt_append + elif smtbmc_vcd: + if not task.opt_append_assume: + log("For VCDs generated by smtbmc the option 'append_assume off' is ignored") + smtbmc_append = task.opt_append + else: + sim_append = task.opt_append + + trace_ext = 'fst' if task.opt_fst else 'vcd' + random_seed = f"--info \"(set-option :random-seed {random_seed})\"" if random_seed else "" - dump_flags = f"--dump-vcd {trace_prefix}.vcd " if task.opt_vcd else "" + dump_flags = f"--dump-vcd {trace_prefix}.vcd " if smtbmc_vcd else "" dump_flags += f"--dump-yw {trace_prefix}.yw --dump-vlogtb {trace_prefix}_tb.v --dump-smtc {trace_prefix}.smtc" proc = SbyProc( task, procname, task.model(model_name), - f"""cd {task.workdir}; {task.exe_paths["smtbmc"]} {" ".join(smtbmc_opts)} -t {t_opt} {random_seed} --append {task.opt_append} {dump_flags} model/design_{model_name}.smt2""", + f"""cd {task.workdir}; {task.exe_paths["smtbmc"]} {" ".join(smtbmc_opts)} -t {t_opt} {random_seed} --append {smtbmc_append} {dump_flags} model/design_{model_name}.smt2""", logfile=open(logfile_prefix + ".txt", "w"), logstderr=(not progress) ) @@ -167,12 +185,30 @@ def run(mode, task, engine_idx, engine): proc_status = None last_prop = [] + pending_sim = None + current_step = None + procs_running = 1 def output_callback(line): nonlocal proc_status nonlocal last_prop + nonlocal pending_sim + nonlocal current_step + nonlocal procs_running + + if pending_sim: + sim_proc = sim_witness_trace(procname, task, engine_idx, pending_sim, append=sim_append) + sim_proc.register_exit_callback(simple_exit_callback) + procs_running += 1 + pending_sim = None + smt2_trans = {'\\':'/', '|':'/'} + match = re.match(r"^## [0-9: ]+ .* in step ([0-9]+)\.\.", line) + if match: + current_step = int(match[1]) + return line + match = re.match(r"^## [0-9: ]+ Status: FAILED", line) if match: proc_status = "FAIL" @@ -193,31 +229,45 @@ def run(mode, task, engine_idx, engine): proc_status = "ERROR" return line - match = re.match(r"^## [0-9: ]+ Assert failed in (\S+): (\S+) \((\S+)\)", line) + match = re.match(r"^## [0-9: ]+ Assert failed in (\S+): (\S+)(?: \((\S+)\))?", line) if match: - cell_name = match[3] + cell_name = match[3] or match[2] prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans) prop.status = "FAIL" last_prop.append(prop) return line - match = re.match(r"^## [0-9: ]+ Reached cover statement at (\S+) \((\S+)\) in step \d+.", line) + match = re.match(r"^## [0-9: ]+ Reached cover statement at (\S+)(?: \((\S+)\))? in step \d+\.", line) if match: - cell_name = match[2] + cell_name = match[2] or match[1] prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans) prop.status = "PASS" last_prop.append(prop) return line - match = re.match(r"^## [0-9: ]+ Writing trace to VCD file: (\S+)", line) - if match and last_prop: - for p in last_prop: - if not p.tracefile: - p.tracefile = match[1] - last_prop = [] - return line + if smtbmc_vcd and not task.opt_fst: + match = re.match(r"^## [0-9: ]+ Writing trace to VCD file: (\S+)", line) + if match: + tracefile = match[1] + trace = os.path.basename(tracefile)[:-4] + engine_case = mode.split('_')[1] if '_' in mode else None + task.summary.add_event(engine_idx=engine_idx, trace=trace, path=tracefile, engine_case=engine_case) - match = re.match(r"^## [0-9: ]+ Unreached cover statement at (\S+) \((\S+)\).", line) + if match and last_prop: + for p in last_prop: + task.summary.add_event( + engine_idx=engine_idx, trace=trace, + type=p.celltype, hdlname=p.hdlname, src=p.location, step=current_step) + p.tracefiles.append(tracefile) + last_prop = [] + return line + else: + match = re.match(r"^## [0-9: ]+ Writing trace to Yosys witness file: (\S+)", line) + if match: + tracefile = match[1] + pending_sim = tracefile + + match = re.match(r"^## [0-9: ]+ Unreached cover statement at (\S+) \((\S+)\)\.", line) if match: cell_name = match[2] prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans) @@ -225,43 +275,28 @@ def run(mode, task, engine_idx, engine): return line + def simple_exit_callback(retcode): + nonlocal procs_running + procs_running -= 1 + if not procs_running: + last_exit_callback() + def exit_callback(retcode): if proc_status is None: task.error(f"engine_{engine_idx}: Engine terminated without status.") + simple_exit_callback(retcode) + def last_exit_callback(): if mode == "bmc" or mode == "cover": task.update_status(proc_status) proc_status_lower = proc_status.lower() if proc_status == "PASS" else proc_status - task.log(f"{click.style(f'engine_{engine_idx}', fg='magenta')}: Status returned by engine: {proc_status_lower}") - task.summary.append(f"""engine_{engine_idx} ({" ".join(engine)}) returned {proc_status_lower}""") - - if proc_status == "FAIL" and mode != "cover": - if os.path.exists(f"{task.workdir}/engine_{engine_idx}/trace.vcd"): - task.summary.append(f"counterexample trace: {task.workdir}/engine_{engine_idx}/trace.vcd") - elif proc_status == "PASS" and mode == "cover": - print_traces_max = 5 - for i in range(print_traces_max): - if os.path.exists(f"{task.workdir}/engine_{engine_idx}/trace{i}.vcd"): - task.summary.append(f"trace: {task.workdir}/engine_{engine_idx}/trace{i}.vcd") - else: - break - else: - excess_traces = 0 - while os.path.exists(f"{task.workdir}/engine_{engine_idx}/trace{print_traces_max + excess_traces}.vcd"): - excess_traces += 1 - if excess_traces > 0: - task.summary.append(f"""and {excess_traces} further trace{"s" if excess_traces > 1 else ""}""") - elif proc_status == "PASS" and mode == "bmc": - for prop in task.design.hierarchy: - if prop.type == prop.Type.ASSERT and prop.status == "UNKNOWN": - prop.status = "PASS" + task.summary.set_engine_status(engine_idx, proc_status_lower) task.terminate() elif mode in ["prove_basecase", "prove_induction"]: proc_status_lower = proc_status.lower() if proc_status == "PASS" else proc_status - task.log(f"""{click.style(f'engine_{engine_idx}', fg='magenta')}: Status returned by engine for {mode.split("_")[1]}: {proc_status_lower}""") - task.summary.append(f"""engine_{engine_idx} ({" ".join(engine)}) returned {proc_status_lower} for {mode.split("_")[1]}""") + task.summary.set_engine_status(engine_idx, proc_status_lower, mode.split("_")[1]) if mode == "prove_basecase": for proc in task.basecase_procs: @@ -272,8 +307,6 @@ def run(mode, task, engine_idx, engine): else: task.update_status(proc_status) - if os.path.exists(f"{task.workdir}/engine_{engine_idx}/trace.vcd"): - task.summary.append(f"counterexample trace: {task.workdir}/engine_{engine_idx}/trace.vcd") task.terminate() elif mode == "prove_induction": @@ -287,9 +320,6 @@ def run(mode, task, engine_idx, engine): assert False if task.basecase_pass and task.induction_pass: - for prop in task.design.hierarchy: - if prop.type == prop.Type.ASSERT and prop.status == "UNKNOWN": - prop.status = "PASS" task.update_status("PASS") task.summary.append("successful proof by k-induction.") task.terminate() @@ -298,4 +328,4 @@ def run(mode, task, engine_idx, engine): assert False proc.output_callback = output_callback - proc.exit_callback = exit_callback + proc.register_exit_callback(exit_callback) diff --git a/sbysrc/sby_mode_bmc.py b/sbysrc/sby_mode_bmc.py index 9ba624c..173812f 100644 --- a/sbysrc/sby_mode_bmc.py +++ b/sbysrc/sby_mode_bmc.py @@ -21,7 +21,6 @@ from sby_core import SbyProc def run(task): task.handle_int_option("depth", 20) - task.handle_int_option("append", 0) task.handle_str_option("aigsmt", "yices") for engine_idx, engine in task.engine_list(): diff --git a/sbysrc/sby_mode_cover.py b/sbysrc/sby_mode_cover.py index 3a5fbe9..c94c639 100644 --- a/sbysrc/sby_mode_cover.py +++ b/sbysrc/sby_mode_cover.py @@ -21,7 +21,6 @@ from sby_core import SbyProc def run(task): task.handle_int_option("depth", 20) - task.handle_int_option("append", 0) for engine_idx, engine in task.engine_list(): task.log(f"{click.style(f'engine_{engine_idx}', fg='magenta')}: {' '.join(engine)}") diff --git a/sbysrc/sby_mode_prove.py b/sbysrc/sby_mode_prove.py index b289f31..e50fbfd 100644 --- a/sbysrc/sby_mode_prove.py +++ b/sbysrc/sby_mode_prove.py @@ -21,7 +21,6 @@ from sby_core import SbyProc def run(task): task.handle_int_option("depth", 20) - task.handle_int_option("append", 0) task.handle_str_option("aigsmt", "yices") task.status = "UNKNOWN" diff --git a/sbysrc/sby_sim.py b/sbysrc/sby_sim.py new file mode 100644 index 0000000..dee99de --- /dev/null +++ b/sbysrc/sby_sim.py @@ -0,0 +1,96 @@ +# +# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows +# +# Copyright (C) 2022 Jannis Harder +# +# Permission to use, copy, modify, and/or distribute this software for any +# purpose with or without fee is hereby granted, provided that the above +# copyright notice and this permission notice appear in all copies. +# +# THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES +# WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF +# MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR +# ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES +# WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN +# ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF +# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. +# + +import os, re, glob, json +from sby_core import SbyProc +from sby_design import pretty_path + +def sim_witness_trace(prefix, task, engine_idx, witness_file, *, append, deps=()): + trace_name = os.path.basename(witness_file)[:-3] + formats = [] + tracefile = None + if task.opt_vcd and task.opt_vcd_sim: + tracefile = f"engine_{engine_idx}/{trace_name}.vcd" + formats.append(f"-vcd {trace_name}.vcd") + if task.opt_fst: + tracefile = f"engine_{engine_idx}/{trace_name}.fst" + formats.append(f"-fst {trace_name}.fst") + + # for warnings / error messages + error_tracefile = f"{task.workdir}/{tracefile}" or f"{task.workdir}/engine_{engine_idx}/{trace_name}.yw" + + sim_log = task.log_prefix(f"{prefix}.{trace_name}") + + sim_log(f"Generating simulation trace for witness file: {witness_file}") + + with open(f"{task.workdir}/engine_{engine_idx}/{trace_name}.ys", "w") as f: + print(f"# running in {task.workdir}/engine_{engine_idx}/", file=f) + print(f"read_rtlil ../model/design_prep.il", file=f) + print(f"sim -hdlname -summary {trace_name}.json -append {append} -r {trace_name}.yw {' '.join(formats)}", file=f) + + def exit_callback(retval): + + if task.design: + task.precise_prop_status = True + + assertion_types = set() + + with open(f"{task.workdir}/engine_{engine_idx}/{trace_name}.json") as summary: + summary = json.load(summary) + for assertion in summary["assertions"]: + assertion["path"] = tuple(assertion["path"]) + + first_appended = summary["steps"] + 1 - append + + printed_assumption_warning = False + + task.summary.add_event(engine_idx=engine_idx, trace=trace_name, path=tracefile) + + for assertion in summary["assertions"]: + if task.design: + prop = task.design.properties_by_path[tuple(assertion["path"])] + else: + prop = None + + hdlname = pretty_path((summary['top'], *assertion['path'])).rstrip() + task.summary.add_event( + engine_idx=engine_idx, + trace=trace_name, path=tracefile, hdlname=hdlname, + type=assertion["type"], src=assertion.get("src"), step=assertion["step"], + prop=prop) + + assertion_types.add(assertion["type"]) + + if assertion["type"] == '$assume': + if assertion["step"] < first_appended: + task.error(f"produced trace {error_tracefile!r} violates assumptions during simulation") + elif not printed_assumption_warning: + sim_log(f"Warning: trace {error_tracefile!r} violates assumptions during simulation of the appended time steps.") + if not task.opt_append_assume: + sim_log("For supported engines, the option 'append_assume on' can be used to find inputs that uphold assumptions during appended time steps.") + printed_assumption_warning = True + + proc = SbyProc( + task, + f"{prefix}.{trace_name}", + deps, + f"""cd {task.workdir}/engine_{engine_idx}; {task.exe_paths["yosys"]} -ql {trace_name}.log {trace_name}.ys""", + ) + proc.noprintregex = re.compile(r"Warning: Assert .* failed.*") + proc.register_exit_callback(exit_callback) + return proc diff --git a/tests/keepgoing/keepgoing_multi_step.py b/tests/keepgoing/keepgoing_multi_step.py index c724c66..548f9d2 100644 --- a/tests/keepgoing/keepgoing_multi_step.py +++ b/tests/keepgoing/keepgoing_multi_step.py @@ -11,7 +11,7 @@ step_5 = line_ref(workdir, src, "step 5") step_7 = line_ref(workdir, src, "step 7") log = open(workdir + "/logfile.txt").read() -log_per_trace = log.split("Writing trace to VCD file")[:-1] +log_per_trace = log.split("Writing trace to Yosys witness file")[:-1] assert len(log_per_trace) == 4 @@ -27,5 +27,5 @@ assert re.search(r"Assert failed in test: %s \(.*\)$" % step_5, log_per_trace[2] assert re.search(r"Assert failed in test: %s \(.*\) \[failed before\]$" % step_3_7, log_per_trace[3], re.M) assert re.search(r"Assert failed in test: %s \(.*\)$" % step_7, log_per_trace[3], re.M) -pattern = f"Property ASSERT in test at {assert_0} failed. Trace file: engine_0/trace0.vcd" +pattern = f"Property ASSERT in test at {assert_0} failed. Trace file: engine_0/trace0.(vcd|fst)" assert re.search(pattern, open(f"{workdir}/{workdir}.xml").read()) diff --git a/tests/keepgoing/keepgoing_same_step.py b/tests/keepgoing/keepgoing_same_step.py index e273916..206d1b3 100644 --- a/tests/keepgoing/keepgoing_same_step.py +++ b/tests/keepgoing/keepgoing_same_step.py @@ -9,7 +9,7 @@ assert_not_a = line_ref(workdir, src, "assert(!a)") assert_0 = line_ref(workdir, src, "assert(0)") log = open(workdir + "/logfile.txt").read() -log_per_trace = log.split("Writing trace to VCD file")[:-1] +log_per_trace = log.split("Writing trace to Yosys witness file")[:-1] assert len(log_per_trace) == 2 diff --git a/tests/keepgoing/keepgoing_smtc.py b/tests/keepgoing/keepgoing_smtc.py index e0fd27d..b41a798 100644 --- a/tests/keepgoing/keepgoing_smtc.py +++ b/tests/keepgoing/keepgoing_smtc.py @@ -12,7 +12,7 @@ assert_false = line_ref(workdir, "extra.smtc", "assert false") assert_distinct = line_ref(workdir, "extra.smtc", "assert (distinct") log = open(workdir + "/logfile.txt").read() -log_per_trace = log.split("Writing trace to VCD file")[:-1] +log_per_trace = log.split("Writing trace to Yosys witness file")[:-1] assert len(log_per_trace) == 4 diff --git a/tests/unsorted/btor_meminit.sby b/tests/unsorted/btor_meminit.sby new file mode 100644 index 0000000..ca584a5 --- /dev/null +++ b/tests/unsorted/btor_meminit.sby @@ -0,0 +1,48 @@ +[tasks] +btormc +#pono +smtbmc + +[options] +mode bmc +expect fail + +[engines] +btormc: btor btormc +# pono: btor pono +smtbmc: smtbmc + +[script] +read -formal top.sv +prep -top top -flatten + +[file top.sv] + +module top(input clk); + + inner inner(clk); + +endmodule + +module inner(input clk); + reg [7:0] counter = 0; + + reg [1:0] mem [0:255]; + + initial begin + mem[0] = 0; + mem[1] = 1; + mem[2] = 2; + mem[3] = 2; + mem[4] = 0; + mem[7] = 0; + end + + always @(posedge clk) begin + counter <= counter + 1; + foo: assert (mem[counter] < 3); + bar: assume (counter < 7); + + mem[counter] <= 0; + end +endmodule diff --git a/tests/unsorted/cover_unreachable.sby b/tests/unsorted/cover_unreachable.sby new file mode 100644 index 0000000..63ebcc7 --- /dev/null +++ b/tests/unsorted/cover_unreachable.sby @@ -0,0 +1,34 @@ +[tasks] +btormc +smtbmc + +[options] +mode cover +expect fail + +[engines] +btormc: btor btormc +smtbmc: smtbmc + +[script] +read -formal top.sv +prep -top top -flatten + +[file top.sv] + +module top(input clk); + + inner inner(clk); + +endmodule + +module inner(input clk); + reg [7:0] counter = 0; + + always @(posedge clk) begin + counter <= counter == 4 ? 0 : counter + 1; + + reachable: cover (counter == 3); + unreachable: cover (counter == 5); + end +endmodule From 06c36d5bb0d8eb35db60ba44798477c3867e4644 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 10 Jan 2023 16:17:49 +0100 Subject: [PATCH 2/4] Support "fifo:" make jobserver auth --- sbysrc/sby_jobserver.py | 25 +++++++++++++++++-------- 1 file changed, 17 insertions(+), 8 deletions(-) diff --git a/sbysrc/sby_jobserver.py b/sbysrc/sby_jobserver.py index b760007..a350133 100644 --- a/sbysrc/sby_jobserver.py +++ b/sbysrc/sby_jobserver.py @@ -58,15 +58,24 @@ def process_jobserver_environment(): elif flag.startswith("--jobserver-auth=") or flag.startswith("--jobserver-fds="): inherited_jobserver_auth_present = True if os.name == "posix": - arg = flag.split("=", 1)[1].split(",") - try: - jobserver_fds = int(arg[0]), int(arg[1]) - for fd in jobserver_fds: - fcntl.fcntl(fd, fcntl.F_GETFD) - except (ValueError, OSError): - pass + arg = flag.split("=", 1)[1] + if arg.startswith("fifo:"): + try: + fd = os.open(arg[5:], os.O_RDWR) + except FileNotFoundError: + pass + else: + inherited_jobserver_auth = fd, fd else: - inherited_jobserver_auth = jobserver_fds + arg = arg.split(",") + try: + jobserver_fds = int(arg[0]), int(arg[1]) + for fd in jobserver_fds: + fcntl.fcntl(fd, fcntl.F_GETFD) + except (ValueError, OSError): + pass + else: + inherited_jobserver_auth = jobserver_fds def jobserver_helper(jobserver_read_fd, jobserver_write_fd, request_fd, response_fd): From 6398938e6ad67080c978b680377a0a9647045317 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 11 Jan 2023 18:02:45 +0100 Subject: [PATCH 3/4] Enable yosys sim support for clock signals in hierarchical designs --- sbysrc/sby_core.py | 5 ++++- sbysrc/sby_sim.py | 5 ++++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index c91561f..f0fcf29 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -989,7 +989,7 @@ class SbyTask(SbyConfig): print("async2sync", file=f) print("chformal -assume -early", file=f) print("opt_clean", file=f) - print("formalff -setundef -clk2ff -ff2anyinit", file=f) + print("formalff -setundef -clk2ff -ff2anyinit -hierarchy", file=f) if self.opt_mode in ["bmc", "prove"]: print("chformal -live -fair -cover -remove", file=f) if self.opt_mode == "cover": @@ -1051,6 +1051,7 @@ class SbyTask(SbyConfig): print(f"# running in {self.workdir}/model/", file=f) print(f"""read_ilang design_prep.il""", file=f) print("hierarchy -smtcheck", file=f) + print("formalff -assume", file=f) if "_nomem" in model_name: print("memory_map -formal", file=f) print("formalff -setundef -clk2ff -ff2anyinit", file=f) @@ -1083,6 +1084,7 @@ class SbyTask(SbyConfig): print(f"# running in {self.workdir}/model/", file=f) print(f"""read_ilang design_prep.il""", file=f) print("hierarchy -simcheck", file=f) + print("formalff -assume", file=f) if "_nomem" in model_name: print("memory_map -formal", file=f) print("formalff -setundef -clk2ff -ff2anyinit", file=f) @@ -1117,6 +1119,7 @@ class SbyTask(SbyConfig): print(f"# running in {self.workdir}/model/", file=f) print("read_ilang design_prep.il", file=f) print("hierarchy -simcheck", file=f) + print("formalff -assume", file=f) print("flatten", file=f) print("setundef -undriven -anyseq", file=f) print("setattr -unset keep", file=f) diff --git a/sbysrc/sby_sim.py b/sbysrc/sby_sim.py index dee99de..0025ed8 100644 --- a/sbysrc/sby_sim.py +++ b/sbysrc/sby_sim.py @@ -63,7 +63,10 @@ def sim_witness_trace(prefix, task, engine_idx, witness_file, *, append, deps=() for assertion in summary["assertions"]: if task.design: - prop = task.design.properties_by_path[tuple(assertion["path"])] + try: + prop = task.design.properties_by_path[tuple(assertion["path"])] + except KeyError: + prop = None else: prop = None From f14aaa57c4bb20c36b8e09252443948c2b3a56c1 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 11 Jan 2023 18:36:06 +0100 Subject: [PATCH 4/4] avy: Fold aiger model using abc to support assumptions --- sbysrc/sby_core.py | 12 ++++++++++++ sbysrc/sby_engine_aiger.py | 7 +++++-- 2 files changed, 17 insertions(+), 2 deletions(-) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index f0fcf29..ae28b6a 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -1146,6 +1146,18 @@ class SbyTask(SbyConfig): return [proc] + if model_name == "aig_fold": + proc = SbyProc( + self, + model_name, + self.model("aig"), + f"""cd {self.workdir}/model; {self.exe_paths["abc"]} -c 'read_aiger design_aiger.aig; fold; strash; write_aiger design_aiger_fold.aig'""", + logfile=open(f"{self.workdir}/model/design_aiger_fold.log", "w") + ) + proc.checkretcode = True + + return [proc] + self.error(f"Invalid model name: {model_name}") def model(self, model_name): diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index d6e14d8..d7a5a31 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/sbysrc/sby_engine_aiger.py @@ -31,6 +31,8 @@ def run(mode, task, engine_idx, engine): status_2 = "UNKNOWN" + model_variant = "" + if solver_args[0] == "suprove": if mode not in ["live", "prove"]: task.error("The aiger solver 'suprove' is only supported in live and prove modes.") @@ -39,6 +41,7 @@ def run(mode, task, engine_idx, engine): solver_cmd = " ".join([task.exe_paths["suprove"]] + solver_args[1:]) elif solver_args[0] == "avy": + model_variant = "_fold" if mode != "prove": task.error("The aiger solver 'avy' is only supported in prove mode.") solver_cmd = " ".join([task.exe_paths["avy"], "--cex", "-"] + solver_args[1:]) @@ -71,8 +74,8 @@ def run(mode, task, engine_idx, engine): proc = SbyProc( task, f"engine_{engine_idx}", - task.model("aig"), - f"cd {task.workdir}; {solver_cmd} model/design_aiger.aig", + task.model(f"aig{model_variant}"), + f"cd {task.workdir}; {solver_cmd} model/design_aiger{model_variant}.aig", logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w") ) if solver_args[0] not in ["avy"]: