From: N. Engelhardt <nak@yosyshq.com>
Date: Mon, 7 Feb 2022 21:01:52 +0000 (+0100)
Subject: fix induction
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7ee357fcc8aa13b7015049f1c89380c5cc074107;p=SymbiYosys.git

fix induction
---

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 7535d71..ede1a8d 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -773,7 +773,7 @@ class SbyTask:
             junit_skipped = 0
         print(f'<?xml version="1.0" encoding="UTF-8"?>', file=f)
         print(f'<testsuites>', file=f)
-        print(f'<testsuite timestamp="{junit_time}" hostname="{platform.node()}" package="{junit_ts_name}" id="1" name="{junit_tc_name}" tests="{junit_tests}" errors="{junit_errors}" failures="{junit_failures}" time="{self.total_time}" skipped="{junit_skipped}">', file=f)
+        print(f'<testsuite timestamp="{junit_time}" hostname="{platform.node()}" package="{junit_ts_name}" id="0" name="{junit_tc_name}" tests="{junit_tests}" errors="{junit_errors}" failures="{junit_failures}" time="{self.total_time}" skipped="{junit_skipped}">', file=f)
         print(f'<properties>', file=f)
         print(f'<property name="os" value="{platform.system()}"/>', file=f)
         print(f'</properties>', file=f)
diff --git a/sbysrc/sby_design.py b/sbysrc/sby_design.py
index c0fdb8b..98a57f1 100644
--- a/sbysrc/sby_design.py
+++ b/sbysrc/sby_design.py
@@ -51,7 +51,7 @@ class SbyProperty:
     tracefile: str = field(default="")
 
     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} at {self.location}: status={self.status}, tracefile=\"{self.tracefile}\">"
 
 @dataclass
 class SbyModule:
@@ -105,14 +105,15 @@ def design_hierarchy(filename):
 
         cells = design_json["modules"][module_name]["cells"]
         for cell_name, cell in cells.items():
+            sub_hierarchy=f"{hierarchy}/{instance_name}" if hierarchy else instance_name
             if cell["type"][0] != '$':
-                mod.submodules[cell_name] = make_mod_hier(cell_name, cell["type"], hierarchy=f"{hierarchy}/{instance_name}")
+                mod.submodules[cell_name] = make_mod_hier(cell_name, cell["type"], hierarchy=sub_hierarchy)
             if cell["type"] in ["$assume", "$assert", "$cover", "$live"]:
                 try:
                     location = cell["attributes"]["src"]
                 except KeyError:
                     location = ""
-                p = SbyProperty(name=cell_name, type=SbyProperty.Type.from_cell(cell["type"]), location=location, hierarchy=f"{hierarchy}/{instance_name}")
+                p = SbyProperty(name=cell_name, type=SbyProperty.Type.from_cell(cell["type"]), location=location, hierarchy=sub_hierarchy)
                 mod.properties.append(p)
         return mod
 
diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 0bf887d..492e2a5 100644
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -273,6 +273,9 @@ 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()
diff --git a/tests/both_ex.sby b/tests/both_ex.sby
index f83f2b1..8177374 100644
--- a/tests/both_ex.sby
+++ b/tests/both_ex.sby
@@ -15,7 +15,7 @@ pono: btor pono
 cover: btor btormc
 
 [script]
-read_verilog -sv both_ex.v
+read -sv both_ex.v
 prep -top test
 
 [files]
diff --git a/tests/cover_fail.sby b/tests/cover_fail.sby
index f75a911..8031e20 100644
--- a/tests/cover_fail.sby
+++ b/tests/cover_fail.sby
@@ -7,7 +7,7 @@ expect fail
 smtbmc boolector
 
 [script]
-read_verilog -sv test.v
+read -sv test.v
 prep -top test
 
 [file test.v]
diff --git a/tests/multi_assert.sby b/tests/multi_assert.sby
index 818195f..883181a 100644
--- a/tests/multi_assert.sby
+++ b/tests/multi_assert.sby
@@ -12,7 +12,7 @@ btormc: btor btormc
 pono: btor pono
 
 [script]
-read_verilog -sv multi_assert.v
+read -sv multi_assert.v
 prep -top test
 
 [file multi_assert.v]
diff --git a/tests/preunsat.sby b/tests/preunsat.sby
index 6694a6c..98255c6 100644
--- a/tests/preunsat.sby
+++ b/tests/preunsat.sby
@@ -12,7 +12,7 @@ btormc: btor btormc
 yices: smtbmc yices
 
 [script]
-read_verilog -sv test.sv
+read -sv test.sv
 prep -top test
 
 [file test.sv]
diff --git a/tests/redxor.sby b/tests/redxor.sby
index 6e6e9f8..0746861 100644
--- a/tests/redxor.sby
+++ b/tests/redxor.sby
@@ -6,7 +6,7 @@ expect pass
 btor btormc
 
 [script]
-read_verilog -formal redxor.v
+read -formal redxor.v
 prep -top test
 
 [files]
diff --git a/tests/stopfirst.sby b/tests/stopfirst.sby
index 35ed539..782f791 100644
--- a/tests/stopfirst.sby
+++ b/tests/stopfirst.sby
@@ -6,7 +6,7 @@ expect fail
 btor btormc
 
 [script]
-read_verilog -sv test.sv
+read -sv test.sv
 prep -top test
 
 [file test.sv]
diff --git a/tests/submod_props.sby b/tests/submod_props.sby
index 33a3a00..93abc9c 100644
--- a/tests/submod_props.sby
+++ b/tests/submod_props.sby
@@ -12,7 +12,7 @@ expect fail
 smtbmc boolector
 
 [script]
-read_verilog -sv test.sv
+read -sv test.sv
 prep -top top
 
 [file test.sv]