mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-12 16:28:17 +00:00
Code Activity

Merge pull request #145 from nakengelhardt/fix_junit_tracefile

Browse source 
junit: handle multiple asserts failing with the same trace
This commit is contained in:
N. Engelhardt 2022-03-28 16:32:54 +02:00 committed by GitHub
parent 3d8f56b89a c7e4785a8a
commit 53abf14514
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 28 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
sbysrc/sby_engine_smtbmc.py
View file

@ -155,7 +155,7 @@ def run(mode, task, engine_idx, engine):
task.induction_procs.append(proc) task.induction_procs.append(proc)
proc_status = None proc_status = None
last_prop = None last_prop = []
def output_callback(line): def output_callback(line):
nonlocal proc_status nonlocal proc_status
@ -187,7 +187,7 @@ def run(mode, task, engine_idx, engine):
cell_name = match[3] cell_name = match[3]
prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans) prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
prop.status = "FAIL" prop.status = "FAIL"
last_prop = prop last_prop.append(prop)
return line 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)
@ -195,13 +195,14 @@ def run(mode, task, engine_idx, engine):
cell_name = match[2] cell_name = match[2]
prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans) prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
prop.status = "PASS" prop.status = "PASS"
last_prop = prop last_prop.append(prop)
return line return line
match = re.match(r"^## [0-9: ]+ Writing trace to VCD file: (\S+)", line) match = re.match(r"^## [0-9: ]+ Writing trace to VCD file: (\S+)", line)
if match and last_prop: if match and last_prop:
last_prop.tracefile = match[1] for p in last_prop:
last_prop = None p.tracefile = match[1]
last_prop = []
return line return line
match = re.match(r"^## [0-9: ]+ Unreached cover statement at (\S+) \((\S+)\).", line) match = re.match(r"^## [0-9: ]+ Unreached cover statement at (\S+) \((\S+)\).", line)

22
tests/2props1trace.sby Normal file
View file

@ -0,0 +1,22 @@
[options]
mode bmc
depth 1
expect fail
[engines]
smtbmc
[script]
read -sv top.sv
prep -top top
[file top.sv]
module top(
input foo,
input bar
);
always @(*) begin
assert (foo);
assert (bar);
end
endmodule