Merge pull request #148 from nakengelhardt/docs_updates

documentation updates

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index e1ee51c363f38b37175bfd4e71243745feea8faf..b78ef8531d24547d0c022319fa6f8ec6d784dbe4 100644 (file)
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -503,7 +503,7 @@ class SbyTask:
                 print("abc -g AND -fast", file=f)
                 print("opt_clean", file=f)
                 print("stat", file=f)
-                print("write_aiger -I -B -zinit -map design_aiger.aim design_aiger.aig", file=f)
+                print("write_aiger -I -B -zinit -no-startoffset -map design_aiger.aim design_aiger.aig", file=f)
 
             proc = SbyProc(
                 self,

diff --git a/sbysrc/sby_design.py b/sbysrc/sby_design.py
index 98a57f132b16c1c733c1234ace39b1e1f450d312..6dfbaecb9dd9dab6dee8975ceb9bd7e85ccb2666 100644 (file)
--- a/sbysrc/sby_design.py
+++ b/sbysrc/sby_design.py
@@ -91,11 +91,13 @@ class SbyModule:
             raise KeyError(f"Could not find assert at {location} in properties list!")
         return prop
 
-    def find_property_by_cellname(self, cell_name):
+    def find_property_by_cellname(self, cell_name, trans_dict=dict()):
+        # backends may need to mangle names irreversibly, so allow applying
+        # the same transformation here
         for prop in self:
-            if prop.name == cell_name:
+            if cell_name == prop.name.translate(str.maketrans(trans_dict)):
                 return prop
-        raise KeyError(f"No such property: {cell_name}")
+        raise KeyError(f"No such property: {smt2_name}")
 
 def design_hierarchy(filename):
     design_json = json.load(filename)

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 492e2a57f01a248c97ec39cb698bfc1b334c4de5..a9c5c804226ea14f084c79d4de605d031b4e2ab4 100644 (file)
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -155,11 +155,12 @@ def run(mode, task, engine_idx, engine):
         task.induction_procs.append(proc)
 
     proc_status = None
-    last_prop = None
+    last_prop = []
 
     def output_callback(line):
         nonlocal proc_status
         nonlocal last_prop
+        smt2_trans = {'\\':'/', '|':'/'}
 
         match = re.match(r"^## [0-9: ]+ Status: FAILED", line)
         if match:
@@ -184,29 +185,30 @@ def run(mode, task, engine_idx, engine):
         match = re.match(r"^## [0-9: ]+ Assert failed in (\S+): (\S+) \((\S+)\)", line)
         if match:
             cell_name = match[3]
-            prop = task.design_hierarchy.find_property_by_cellname(cell_name)
+            prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
             prop.status = "FAIL"
-            last_prop = prop
+            last_prop.append(prop)
             return line
 
         match = re.match(r"^## [0-9: ]+ Reached cover statement at (\S+) \((\S+)\) in step \d+.", line)
         if match:
             cell_name = match[2]
-            prop = task.design_hierarchy.find_property_by_cellname(cell_name)
+            prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
             prop.status = "PASS"
-            last_prop = prop
+            last_prop.append(prop)
             return line
 
         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
+            for p in last_prop:
+                p.tracefile = match[1]
+            last_prop = []
             return line
 
         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)
+            prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
             prop.status = "FAIL"
 
         return line

diff --git a/tests/.gitignore b/tests/.gitignore
index 212f4ddbe1f3e25fcc3abb967ed421e5905ef440..120675bec4354855a2ba9fe51cff81368d3f05b8 100644 (file)
--- a/tests/.gitignore
+++ b/tests/.gitignore
@@ -10,3 +10,4 @@
 /junit_*/
 /submod_props*/
 /multi_assert*/
+/aim_vs_smt2_nonzero_start_offset*/

diff --git a/tests/2props1trace.sby b/tests/2props1trace.sby
new file mode 100644 (file)
index 0000000..8f51fde
--- /dev/null
+++ b/tests/2props1trace.sby
@@ -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

diff --git a/tests/aim_vs_smt2_nonzero_start_offset.sby b/tests/aim_vs_smt2_nonzero_start_offset.sby
new file mode 100644 (file)
index 0000000..4309551
--- /dev/null
+++ b/tests/aim_vs_smt2_nonzero_start_offset.sby
@@ -0,0 +1,33 @@
+[tasks]
+bmc
+prove
+
+[options]
+bmc: mode bmc
+prove: mode prove
+expect fail
+wait on
+
+[engines]
+bmc: abc bmc3
+bmc: abc sim3
+prove: aiger avy
+prove: aiger suprove
+prove: abc pdr
+
+[script]
+read -sv test.sv
+prep -top test
+
+[file test.sv]
+module test (
+    input clk,
+    input [8:1] nonzero_offset
+);
+    reg [7:0] counter = 0;
+
+    always @(posedge clk) begin
+        if (counter == 3) assert(nonzero_offset[1]);
+        counter <= counter + 1;
+    end
+endmodule

diff --git a/tests/submod_props.sby b/tests/submod_props.sby
index 93abc9c139d18ca8d8fe07d943e7f63acec99fec..99336767d86772ce4b8452ec1df50935e55950c6 100644 (file)
--- a/tests/submod_props.sby
+++ b/tests/submod_props.sby
@@ -1,10 +1,12 @@
 [tasks]
 bmc
 cover
+flatten
 
 [options]
 bmc: mode bmc
 cover: mode cover
+flatten: mode bmc
 
 expect fail
 
@@ -14,6 +16,7 @@ smtbmc boolector
 [script]
 read -sv test.sv
 prep -top top
+flatten: flatten
 
 [file test.sv]
 module test(input foo);