Merge pull request #7 from YosysHQ/master

Syncing with official repo

1 files changed, 43 insertions, 14 deletions

diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 1a8d2484c..bac68ac70 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -17,7 +17,9 @@
 #
 
 import sys, re, os, signal
-import resource, subprocess
+import subprocess
+if os.name == "posix":
+    import resource
 from copy import deepcopy
 from select import select
 from time import time
@@ -27,12 +29,25 @@ from threading import Thread
 
 # This is needed so that the recursive SMT2 S-expression parser
 # does not run out of stack frames when parsing large expressions
-smtio_reclimit = 64 * 1024
-smtio_stacksize = 128 * 1024 * 1024
-if sys.getrecursionlimit() < smtio_reclimit:
-    sys.setrecursionlimit(smtio_reclimit)
-if resource.getrlimit(resource.RLIMIT_STACK)[0] < smtio_stacksize:
-    resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, -1))
+if os.name == "posix":
+    smtio_reclimit = 64 * 1024
+    if sys.getrecursionlimit() < smtio_reclimit:
+        sys.setrecursionlimit(smtio_reclimit)
+
+    current_rlimit_stack = resource.getrlimit(resource.RLIMIT_STACK)
+    if current_rlimit_stack[0] != resource.RLIM_INFINITY:
+        smtio_stacksize = 128 * 1024 * 1024
+        if os.uname().sysname == "Darwin":
+            # MacOS has rather conservative stack limits
+            smtio_stacksize = 16 * 1024 * 1024
+        if current_rlimit_stack[1] != resource.RLIM_INFINITY:
+            smtio_stacksize = min(smtio_stacksize, current_rlimit_stack[1])
+        if current_rlimit_stack[0] < smtio_stacksize:
+            try:
+                resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, current_rlimit_stack[1]))
+            except ValueError:
+                # couldn't get more stack, just run with what we have
+                pass
 
 
 # currently running solvers (so we can kill them)
@@ -51,8 +66,9 @@ def force_shutdown(signum, frame):
             os.kill(p.pid, signal.SIGTERM)
     sys.exit(1)
 
+if os.name == "posix":
+    signal.signal(signal.SIGHUP, force_shutdown)
 signal.signal(signal.SIGINT, force_shutdown)
-signal.signal(signal.SIGHUP, force_shutdown)
 signal.signal(signal.SIGTERM, force_shutdown)
 
 def except_hook(exctype, value, traceback):
@@ -154,19 +170,28 @@ class SmtIo:
             self.unroll = False
 
         if self.solver == "yices":
-            self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
+            if self.noincr:
+                self.popen_vargs = ['yices-smt2'] + self.solver_opts
+            else:
+                self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
 
         if self.solver == "z3":
             self.popen_vargs = ['z3', '-smt2', '-in'] + self.solver_opts
 
         if self.solver == "cvc4":
-            self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
+            if self.noincr:
+                self.popen_vargs = ['cvc4', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
+            else:
+                self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
 
         if self.solver == "mathsat":
             self.popen_vargs = ['mathsat'] + self.solver_opts
 
         if self.solver == "boolector":
-            self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts
+            if self.noincr:
+                self.popen_vargs = ['boolector', '--smt2'] + self.solver_opts
+            else:
+                self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts
             self.unroll = True
 
         if self.solver == "abc":
@@ -763,7 +788,7 @@ class SmtIo:
 
     def get_path(self, mod, path):
         assert mod in self.modinfo
-        path = path.split(".")
+        path = path.replace("\\", "/").split(".")
 
         for i in range(len(path)-1):
             first = ".".join(path[0:i+1])
@@ -1002,6 +1027,8 @@ class MkVcd:
         assert t >= self.t
         if t != self.t:
             if self.t == -1:
+                print("$version Generated by Yosys-SMTBMC $end", file=self.f)
+                print("$timescale 1ns $end", file=self.f)
                 print("$var integer 32 t smt_step $end", file=self.f)
                 print("$var event 1 ! smt_clock $end", file=self.f)
 
@@ -1020,7 +1047,10 @@ class MkVcd:
                         scope = scope[:-1]
 
                     while uipath[:-1] != scope:
-                        print("$scope module %s $end" % uipath[len(scope)], file=self.f)
+                        scopename = uipath[len(scope)]
+                        if scopename.startswith("$"):
+                            scopename = "\\" + scopename
+                        print("$scope module %s $end" % scopename, file=self.f)
                         scope.append(uipath[len(scope)])
 
                     if path in self.clocks and self.clocks[path][1] == "event":
@@ -1053,4 +1083,3 @@ class MkVcd:
                     print("b0 %s" % self.nets[path][0], file=self.f)
                 else:
                     print("b1 %s" % self.nets[path][0], file=self.f)
-