aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2/smtio.py
diff options
context:
space:
mode:
Diffstat (limited to 'backends/smt2/smtio.py')
-rw-r--r--backends/smt2/smtio.py13
1 files changed, 11 insertions, 2 deletions
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index ab20a4af2..bac68ac70 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -43,7 +43,11 @@ if os.name == "posix":
if current_rlimit_stack[1] != resource.RLIM_INFINITY:
smtio_stacksize = min(smtio_stacksize, current_rlimit_stack[1])
if current_rlimit_stack[0] < smtio_stacksize:
- resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, current_rlimit_stack[1]))
+ 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)
@@ -1023,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)
@@ -1041,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":