mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-27 23:45:50 +00:00
Code Activity

parse solver location output for assert failures (cover not functional yet)

Browse source
This commit is contained in:
N. Engelhardt 2022-01-27 13:41:07 +01:00
parent a9d1972c47
commit 1cf27e7c31
5 changed files with 91 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

2
sbysrc/sby.py
View file

@ -478,7 +478,7 @@ def run_task(taskname):
print(f'</properties>', file=f)
if solver_gives_line:
for check in checks:
print(f'<testcase classname="{junit_tc_name}" name="" time="{task.total_time}">', file=f) # name required
print(f'<testcase classname="{junit_tc_name}" name="Property {check.type} in {check.hierarchy} at {check.location}" time="{task.total_time}">', file=f) # name required
if check.status == "UNKNOWN":
print(f'<skipped />', file=f)
elif check.status == "FAIL":

14
sbysrc/sby_core.py
View file

@ -222,8 +222,9 @@ class SbyTask:
self.reusedir = reusedir
self.status = "UNKNOWN"
self.total_time = 0
self.expect = []
self.expect = list()
self.design_hierarchy = None
self.precise_prop_status = False
yosys_program_prefix = "" ##yosys-program-prefix##
self.exe_paths = {
@ -371,6 +372,9 @@ class SbyTask:
print(f"# running in {self.workdir}/src/", file=f)
for cmd in self.script:
print(cmd, file=f)
# assumptions at this point: hierarchy has been run and a top module has been designated
print("hierarchy -simcheck", file=f)
print(f"""write_json ../model/design.json""", file=f)
if model_name == "base":
print("memory_nordff", file=f)
else:
@ -392,8 +396,6 @@ class SbyTask:
print("opt -keepdc -fast", file=f)
print("check", file=f)
print("hierarchy -simcheck", file=f)
# FIXME: can using design and design_nomem in the same task happen?
print(f"""write_json ../model/design{"" if model_name == "base" else "_nomem"}.json""", file=f)
print(f"""write_ilang ../model/design{"" if model_name == "base" else "_nomem"}.il""", file=f)
proc = SbyProc(
@ -407,9 +409,9 @@ class SbyTask:
def instance_hierarchy_callback(retcode):
assert retcode == 0
assert self.design_hierarchy == None # verify this assumption
with open(f"""{self.workdir}/model/design{"" if model_name == "base" else "_nomem"}.json""") as f:
self.design_hierarchy = design_hierarchy(f)
if self.design_hierarchy == None:
with open(f"""{self.workdir}/model/design{"" if model_name == "base" else "_nomem"}.json""") as f:
self.design_hierarchy = design_hierarchy(f)
proc.exit_callback = instance_hierarchy_callback

29
sbysrc/sby_design.py
View file

@ -28,7 +28,7 @@ class SbyProperty:
COVER = auto()
LIVE = auto()
def __repr__(self):
def __str__(self):
return self.name
@classmethod
@ -50,6 +50,9 @@ class SbyProperty:
status: str = field(default="UNKNOWN")
tracefile: str = field(default="")
def __repr__(self):
return f"SbyProperty<{self.type} {self.name} at {self.location}: status={self.status}, tracefile=\"{self.tracefile}\""
@dataclass
class SbyModule:
name: str
@ -57,13 +60,35 @@ class SbyModule:
submodules: dict = field(default_factory=dict)
properties: list = field(default_factory=list)
def __repr__(self):
return f"SbyModule<{self.name} : {self.type}, submodules={self.submodules}, properties={self.properties}>"
def get_property_list(self):
l = list()
l.extend(self.properties)
for submod in self.submodules:
for submod in self.submodules.values():
l.extend(submod.get_property_list())
return l
def find_property(self, hierarchy, location):
# FIXME: use that RE that works with escaped paths from https://stackoverflow.com/questions/46207665/regex-pattern-to-split-verilog-path-in-different-instances-using-python
path = hierarchy.split('.')
mod = path.pop(0)
if self.name != mod:
raise ValueError(f"{self.name} is not the first module in hierarchical path {hierarchy}.")
try:
mod_hier = self
while path:
mod = path.pop(0)
mod_hier = mod_hier.submodules[mod]
except KeyError:
raise KeyError(f"Could not find {hierarchy} in design hierarchy!")
try:
prop = next(p for p in mod_hier.properties if location in p.location)
except StopIteration:
raise KeyError(f"Could not find assert at {location} in properties list!")
return prop
def design_hierarchy(filename):
design_json = json.load(filename)
def make_mod_hier(instance_name, module_name, hierarchy=""):

25
sbysrc/sby_engine_smtbmc.py
View file

@ -32,6 +32,7 @@ def run(mode, task, engine_idx, engine):
basecase_only = False
induction_only = False
random_seed = None
task.precise_prop_status = True
opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "stdt", "presat",
"nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", "induction", "seed="])
@ -154,9 +155,11 @@ def run(mode, task, engine_idx, engine):
task.induction_procs.append(proc)
proc_status = None
last_prop = None
def output_callback(line):
nonlocal proc_status
nonlocal last_prop
match = re.match(r"^## [0-9: ]+ Status: FAILED", line)
if match:
@ -178,6 +181,28 @@ def run(mode, task, engine_idx, engine):
proc_status = "ERROR"
return line
match = re.match(r"^## [0-9: ]+ Assert failed in (([a-z_][a-z0-9$_]*|\\\S*|\.)+): (\S*).*", line)
if match:
module_path = match[1]
location = match[3]
try:
prop = task.design_hierarchy.find_property(module_path, location)
except KeyError as e:
task.precise_prop_status = False
return line + f" (Warning: {str(e)})"
prop.status = "FAIL"
last_prop = prop
return line
match = re.match(r"^## [0-9: ]+ Reached cover statement at (\S+) in step \d+.", line)
if match:
location = match[1]
match = re.match(r"^## [0-9: ]+ Writing trace to VCD file: (\S+)", line)
if match and last_prop:
last_prop.tracefile = match[1]
last_prop = None
return line
def exit_callback(retcode):

30
tests/submod_props.sby Normal file
View file

@ -0,0 +1,30 @@
[tasks]
bmc
cover
[options]
bmc: mode bmc
cover: mode cover
expect fail
[engines]
smtbmc boolector
[script]
read_verilog -sv test.sv
prep -top top
[file test.sv]
module test(input foo);
always @* assert(foo);
always @* assert(!foo);
always @* cover(foo);
always @* cover(!foo);
endmodule
module top();
test test_i (
.foo(1'b1)
);
endmodule