7cd7d0d5997a43421e1b30ce6fcb1554b5451d0d
2 # yosys -- Yosys Open SYnthesis Suite
4 # Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
6 # Permission to use, copy, modify, and/or distribute this software for any
7 # purpose with or without fee is hereby granted, provided that the above
8 # copyright notice and this permission notice appear in all copies.
10 # THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
11 # WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
12 # MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
13 # ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
14 # WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
15 # ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
16 # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
19 import sys
, subprocess
, re
, os
20 from copy
import deepcopy
21 from select
import select
26 "0": "0000", "1": "0001", "2": "0010", "3": "0011",
27 "4": "0100", "5": "0101", "6": "0110", "7": "0111",
28 "8": "1000", "9": "1001", "A": "1010", "B": "1011",
29 "C": "1100", "D": "1101", "E": "1110", "F": "1111",
30 "a": "1010", "b": "1011", "c": "1100", "d": "1101",
31 "e": "1110", "f": "1111"
39 self
.registers
= set()
40 self
.memories
= dict()
46 self
.anyconsts
= dict()
51 def __init__(self
, opts
=None):
58 self
.produce_models
= True
59 self
.smt2cache
= [list()]
64 self
.logic
= opts
.logic
65 self
.solver
= opts
.solver
66 self
.solver_opts
= opts
.solver_opts
67 self
.debug_print
= opts
.debug_print
68 self
.debug_file
= opts
.debug_file
69 self
.dummy_file
= opts
.dummy_file
70 self
.timeinfo
= opts
.timeinfo
71 self
.unroll
= opts
.unroll
72 self
.noincr
= opts
.noincr
73 self
.info_stmts
= opts
.info_stmts
74 self
.nocomments
= opts
.nocomments
78 self
.solver_opts
= list()
79 self
.debug_print
= False
80 self
.debug_file
= None
81 self
.dummy_file
= None
82 self
.timeinfo
= os
.name
!= "nt"
85 self
.info_stmts
= list()
86 self
.nocomments
= False
88 self
.start_time
= time()
93 self
.setup_done
= False
96 assert not self
.setup_done
98 if self
.solver
== "yices":
99 self
.popen_vargs
= ['yices-smt2', '--incremental'] + self
.solver_opts
101 if self
.solver
== "z3":
102 self
.popen_vargs
= ['z3', '-smt2', '-in'] + self
.solver_opts
104 if self
.solver
== "cvc4":
105 self
.popen_vargs
= ['cvc4', '--incremental', '--lang', 'smt2.6' if self
.logic_dt
else 'smt2'] + self
.solver_opts
107 if self
.solver
== "mathsat":
108 self
.popen_vargs
= ['mathsat'] + self
.solver_opts
110 if self
.solver
== "boolector":
111 self
.popen_vargs
= ['boolector', '--smt2', '-i'] + self
.solver_opts
114 if self
.solver
== "abc":
115 if len(self
.solver_opts
) > 0:
116 self
.popen_vargs
= ['yosys-abc', '-S', '; '.join(self
.solver_opts
)]
118 self
.popen_vargs
= ['yosys-abc', '-S', '%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000']
119 self
.logic_ax
= False
123 if self
.solver
== "dummy":
124 assert self
.dummy_file
is not None
125 self
.dummy_fd
= open(self
.dummy_file
, "r")
127 if self
.dummy_file
is not None:
128 self
.dummy_fd
= open(self
.dummy_file
, "w")
130 self
.p
= subprocess
.Popen(self
.popen_vargs
, stdin
=subprocess
.PIPE
, stdout
=subprocess
.PIPE
, stderr
=subprocess
.STDOUT
)
133 self
.logic_uf
= False
134 self
.unroll_idcnt
= 0
135 self
.unroll_buffer
= ""
136 self
.unroll_sorts
= set()
137 self
.unroll_objs
= set()
138 self
.unroll_decls
= dict()
139 self
.unroll_cache
= dict()
140 self
.unroll_stack
= list()
142 if self
.logic
is None:
144 if self
.logic_qf
: self
.logic
+= "QF_"
145 if self
.logic_ax
: self
.logic
+= "A"
146 if self
.logic_uf
: self
.logic
+= "UF"
147 if self
.logic_bv
: self
.logic
+= "BV"
148 if self
.logic_dt
: self
.logic
= "ALL"
150 self
.setup_done
= True
152 if self
.produce_models
:
153 self
.write("(set-option :produce-models true)")
155 self
.write("(set-logic %s)" % self
.logic
)
157 for stmt
in self
.info_stmts
:
161 secs
= int(time() - self
.start_time
)
162 return "## %6d %3d:%02d:%02d " % (secs
, secs
// (60*60), (secs
// 60) % 60, secs
% 60)
164 def replace_in_stmt(self
, stmt
, pat
, repl
):
168 if isinstance(stmt
, list):
169 return [self
.replace_in_stmt(s
, pat
, repl
) for s
in stmt
]
173 def unroll_stmt(self
, stmt
):
174 if not isinstance(stmt
, list):
177 stmt
= [self
.unroll_stmt(s
) for s
in stmt
]
179 if len(stmt
) >= 2 and not isinstance(stmt
[0], list) and stmt
[0] in self
.unroll_decls
:
180 assert stmt
[1] in self
.unroll_objs
183 if key
not in self
.unroll_cache
:
184 decl
= deepcopy(self
.unroll_decls
[key
[0]])
186 self
.unroll_cache
[key
] = "|UNROLL#%d|" % self
.unroll_idcnt
187 decl
[1] = self
.unroll_cache
[key
]
188 self
.unroll_idcnt
+= 1
190 if decl
[0] == "declare-fun":
191 if isinstance(decl
[3], list) or decl
[3] not in self
.unroll_sorts
:
192 self
.unroll_objs
.add(decl
[1])
195 self
.unroll_objs
.add(decl
[1])
198 elif decl
[0] == "define-fun":
200 for arg_name
, arg_sort
in decl
[2]:
201 decl
[4] = self
.replace_in_stmt(decl
[4], arg_name
, key
[arg_index
])
206 decl
= self
.unroll_stmt(decl
)
207 self
.write(self
.unparse(decl
), unroll
=False)
209 return self
.unroll_cache
[key
]
213 def p_write(self
, data
):
214 # select_result = select([self.p.stdout], [self.p.stdin], [], 0.1):
215 wlen
= self
.p
.stdin
.write(data
)
216 assert wlen
== len(data
)
222 if len(self
.p_buffer
) == 0:
223 return self
.p
.stdout
.readline().decode("ascii")
226 def write(self
, stmt
, unroll
=True):
227 if stmt
.startswith(";"):
229 if not self
.setup_done
:
230 self
.info_stmts
.append(stmt
)
232 elif not self
.setup_done
:
237 if self
.nocomments
or self
.unroll
:
238 stmt
= re
.sub(r
" *;.*", "", stmt
)
239 if stmt
== "": return
241 if unroll
and self
.unroll
:
242 stmt
= self
.unroll_buffer
+ stmt
243 self
.unroll_buffer
= ""
245 s
= re
.sub(r
"\|[^|]*\|", "", stmt
)
246 if s
.count("(") != s
.count(")"):
247 self
.unroll_buffer
= stmt
+ " "
255 if len(s
) == 3 and s
[0] == "declare-sort" and s
[2] == "0":
256 self
.unroll_sorts
.add(s
[1])
259 elif len(s
) == 4 and s
[0] == "declare-fun" and s
[2] == [] and s
[3] in self
.unroll_sorts
:
260 self
.unroll_objs
.add(s
[1])
263 elif len(s
) >= 4 and s
[0] == "declare-fun":
264 for arg_sort
in s
[2]:
265 if arg_sort
in self
.unroll_sorts
:
266 self
.unroll_decls
[s
[1]] = s
269 elif len(s
) >= 4 and s
[0] == "define-fun":
270 for arg_name
, arg_sort
in s
[2]:
271 if arg_sort
in self
.unroll_sorts
:
272 self
.unroll_decls
[s
[1]] = s
275 stmt
= self
.unparse(self
.unroll_stmt(s
))
277 if stmt
== "(push 1)":
278 self
.unroll_stack
.append((
279 deepcopy(self
.unroll_sorts
),
280 deepcopy(self
.unroll_objs
),
281 deepcopy(self
.unroll_decls
),
282 deepcopy(self
.unroll_cache
),
285 if stmt
== "(pop 1)":
286 self
.unroll_sorts
, self
.unroll_objs
, self
.unroll_decls
, self
.unroll_cache
= self
.unroll_stack
.pop()
292 print(stmt
, file=self
.debug_file
)
293 self
.debug_file
.flush()
295 if self
.solver
!= "dummy":
297 if self
.p
is not None and not stmt
.startswith("(get-"):
301 if stmt
== "(push 1)":
302 self
.smt2cache
.append(list())
303 elif stmt
== "(pop 1)":
306 if self
.p
is not None:
307 self
.p_write(bytes(stmt
+ "\n", "ascii"))
309 self
.smt2cache
[-1].append(stmt
)
311 self
.p_write(bytes(stmt
+ "\n", "ascii"))
314 def info(self
, stmt
):
315 if not stmt
.startswith("; yosys-smt2-"):
318 fields
= stmt
.split()
320 if fields
[1] == "yosys-smt2-nomem":
321 if self
.logic
is None:
322 self
.logic_ax
= False
324 if fields
[1] == "yosys-smt2-nobv":
325 if self
.logic
is None:
326 self
.logic_bv
= False
328 if fields
[1] == "yosys-smt2-stdt":
329 if self
.logic
is None:
332 if fields
[1] == "yosys-smt2-module":
333 self
.curmod
= fields
[2]
334 self
.modinfo
[self
.curmod
] = SmtModInfo()
336 if fields
[1] == "yosys-smt2-cell":
337 self
.modinfo
[self
.curmod
].cells
[fields
[3]] = fields
[2]
339 if fields
[1] == "yosys-smt2-topmod":
340 self
.topmod
= fields
[2]
342 if fields
[1] == "yosys-smt2-input":
343 self
.modinfo
[self
.curmod
].inputs
.add(fields
[2])
344 self
.modinfo
[self
.curmod
].wsize
[fields
[2]] = int(fields
[3])
346 if fields
[1] == "yosys-smt2-output":
347 self
.modinfo
[self
.curmod
].outputs
.add(fields
[2])
348 self
.modinfo
[self
.curmod
].wsize
[fields
[2]] = int(fields
[3])
350 if fields
[1] == "yosys-smt2-register":
351 self
.modinfo
[self
.curmod
].registers
.add(fields
[2])
352 self
.modinfo
[self
.curmod
].wsize
[fields
[2]] = int(fields
[3])
354 if fields
[1] == "yosys-smt2-memory":
355 self
.modinfo
[self
.curmod
].memories
[fields
[2]] = (int(fields
[3]), int(fields
[4]), int(fields
[5]), int(fields
[6]))
357 if fields
[1] == "yosys-smt2-wire":
358 self
.modinfo
[self
.curmod
].wires
.add(fields
[2])
359 self
.modinfo
[self
.curmod
].wsize
[fields
[2]] = int(fields
[3])
361 if fields
[1] == "yosys-smt2-assert":
362 self
.modinfo
[self
.curmod
].asserts
["%s_a %s" % (self
.curmod
, fields
[2])] = fields
[3]
364 if fields
[1] == "yosys-smt2-cover":
365 self
.modinfo
[self
.curmod
].covers
["%s_c %s" % (self
.curmod
, fields
[2])] = fields
[3]
367 if fields
[1] == "yosys-smt2-anyconst":
368 self
.modinfo
[self
.curmod
].anyconsts
[fields
[2]] = (fields
[3], None if len(fields
) <= 4 else fields
[4])
370 if fields
[1] == "yosys-smt2-anyseq":
371 self
.modinfo
[self
.curmod
].anyseqs
[fields
[2]] = (fields
[3], None if len(fields
) <= 4 else fields
[4])
373 def hiernets(self
, top
, regs_only
=False):
374 def hiernets_worker(nets
, mod
, cursor
):
375 for netname
in sorted(self
.modinfo
[mod
].wsize
.keys()):
376 if not regs_only
or netname
in self
.modinfo
[mod
].registers
:
377 nets
.append(cursor
+ [netname
])
378 for cellname
, celltype
in sorted(self
.modinfo
[mod
].cells
.items()):
379 hiernets_worker(nets
, celltype
, cursor
+ [cellname
])
382 hiernets_worker(nets
, top
, [])
385 def hieranyconsts(self
, top
):
386 def worker(results
, mod
, cursor
):
387 for name
, value
in sorted(self
.modinfo
[mod
].anyconsts
.items()):
388 results
.append((cursor
, name
, value
[0], value
[1]))
389 for cellname
, celltype
in sorted(self
.modinfo
[mod
].cells
.items()):
390 worker(results
, celltype
, cursor
+ [cellname
])
393 worker(results
, top
, [])
396 def hieranyseqs(self
, top
):
397 def worker(results
, mod
, cursor
):
398 for name
, value
in sorted(self
.modinfo
[mod
].anyseqs
.items()):
399 results
.append((cursor
, name
, value
[0], value
[1]))
400 for cellname
, celltype
in sorted(self
.modinfo
[mod
].cells
.items()):
401 worker(results
, celltype
, cursor
+ [cellname
])
404 worker(results
, top
, [])
407 def hiermems(self
, top
):
408 def hiermems_worker(mems
, mod
, cursor
):
409 for memname
in sorted(self
.modinfo
[mod
].memories
.keys()):
410 mems
.append(cursor
+ [memname
])
411 for cellname
, celltype
in sorted(self
.modinfo
[mod
].cells
.items()):
412 hiermems_worker(mems
, celltype
, cursor
+ [cellname
])
415 hiermems_worker(mems
, top
, [])
423 if self
.solver
== "dummy":
424 line
= self
.dummy_fd
.readline().strip()
426 line
= self
.p_read().strip()
427 if self
.dummy_file
is not None:
428 self
.dummy_fd
.write(line
+ "\n")
430 count_brackets
+= line
.count("(")
431 count_brackets
-= line
.count(")")
436 if count_brackets
== 0:
438 if self
.solver
!= "dummy" and self
.p
.poll():
439 print("SMT Solver terminated unexpectedly: %s" % "".join(stmt
))
443 if stmt
.startswith("(error"):
444 print("SMT Solver Error: %s" % stmt
, file=sys
.stderr
)
451 print("> (check-sat)")
452 if self
.debug_file
and not self
.nocomments
:
453 print("; running check-sat..", file=self
.debug_file
)
454 self
.debug_file
.flush()
456 if self
.solver
!= "dummy":
458 if self
.p
is not None:
462 self
.p
= subprocess
.Popen(self
.popen_vargs
, stdin
=subprocess
.PIPE
, stdout
=subprocess
.PIPE
, stderr
=subprocess
.STDOUT
)
463 for cache_ctx
in self
.smt2cache
:
464 for cache_stmt
in cache_ctx
:
465 self
.p_write(bytes(cache_stmt
+ "\n", "ascii"))
467 self
.p_write(bytes("(check-sat)\n", "ascii"))
476 while select([self
.p
.stdout
], [], [], 0.1) == ([], [], []):
482 if count
% 10 == 0 or count
== 25:
486 m
= "(%d seconds)" % secs
488 m
= "(%d seconds -- %d:%02d)" % (secs
, secs
// 60, secs
% 60)
490 m
= "(%d seconds -- %d:%02d:%02d)" % (secs
, secs
// (60*60), (secs
// 60) % 60, secs
% 60)
492 print("%s %s %c" % ("\b \b" * num_bs
, m
, s
[i
]), end
="", file=sys
.stderr
)
496 print("\b" + s
[i
], end
="", file=sys
.stderr
)
502 print("\b \b" * num_bs
, end
="", file=sys
.stderr
)
507 print("(set-info :status %s)" % result
, file=self
.debug_file
)
508 print("(check-sat)", file=self
.debug_file
)
509 self
.debug_file
.flush()
512 def parse(self
, stmt
):
517 while stmt
[cursor
] != ')':
518 el
, le
= worker(stmt
[cursor
:])
521 return expr
, cursor
+1
526 while stmt
[cursor
] != '|':
530 return expr
, cursor
+1
532 if stmt
[0] in [" ", "\t", "\r", "\n"]:
533 el
, le
= worker(stmt
[1:])
538 while stmt
[cursor
] not in ["(", ")", "|", " ", "\t", "\r", "\n"]:
542 return worker(stmt
)[0]
544 def unparse(self
, stmt
):
545 if isinstance(stmt
, list):
546 return "(" + " ".join([self
.unparse(s
) for s
in stmt
]) + ")"
554 if len(v
) > 0 and v
[-1] == "1": d
+= 1
555 if len(v
) > 1 and v
[-2] == "1": d
+= 2
556 if len(v
) > 2 and v
[-3] == "1": d
+= 4
557 if len(v
) > 3 and v
[-4] == "1": d
+= 8
564 if v
== "true": return "1"
565 if v
== "false": return "0"
566 if v
.startswith("#b"):
568 if v
.startswith("#x"):
569 return "".join(hex_dict
.get(x
) for x
in v
[2:])
573 return int(self
.bv2bin(v
), 2)
576 self
.write("(get-value (%s))" % (expr
))
577 return self
.parse(self
.read())[0][1]
579 def get_list(self
, expr_list
):
580 if len(expr_list
) == 0:
582 self
.write("(get-value (%s))" % " ".join(expr_list
))
583 return [n
[1] for n
in self
.parse(self
.read())]
585 def get_path(self
, mod
, path
):
586 assert mod
in self
.modinfo
587 path
= path
.split(".")
589 for i
in range(len(path
)-1):
590 first
= ".".join(path
[0:i
+1])
591 second
= ".".join(path
[i
+1:])
593 if first
in self
.modinfo
[mod
].cells
:
594 nextmod
= self
.modinfo
[mod
].cells
[first
]
595 return [first
] + self
.get_path(nextmod
, second
)
597 return [".".join(path
)]
599 def net_expr(self
, mod
, base
, path
):
604 assert mod
in self
.modinfo
607 if path
[0] in self
.modinfo
[mod
].cells
:
608 return "(|%s_h %s| %s)" % (mod
, path
[0], base
)
609 if path
[0] in self
.modinfo
[mod
].wsize
:
610 return "(|%s_n %s| %s)" % (mod
, path
[0], base
)
611 if path
[0] in self
.modinfo
[mod
].memories
:
612 return "(|%s_m %s| %s)" % (mod
, path
[0], base
)
615 assert mod
in self
.modinfo
616 assert path
[0] in self
.modinfo
[mod
].cells
618 nextmod
= self
.modinfo
[mod
].cells
[path
[0]]
619 nextbase
= "(|%s_h %s| %s)" % (mod
, path
[0], base
)
620 return self
.net_expr(nextmod
, nextbase
, path
[1:])
622 def net_width(self
, mod
, net_path
):
623 for i
in range(len(net_path
)-1):
624 assert mod
in self
.modinfo
625 assert net_path
[i
] in self
.modinfo
[mod
].cells
626 mod
= self
.modinfo
[mod
].cells
[net_path
[i
]]
628 assert mod
in self
.modinfo
629 assert net_path
[-1] in self
.modinfo
[mod
].wsize
630 return self
.modinfo
[mod
].wsize
[net_path
[-1]]
632 def net_exists(self
, mod
, net_path
):
633 for i
in range(len(net_path
)-1):
634 if mod
not in self
.modinfo
: return False
635 if net_path
[i
] not in self
.modinfo
[mod
].cells
: return False
636 mod
= self
.modinfo
[mod
].cells
[net_path
[i
]]
638 if mod
not in self
.modinfo
: return False
639 if net_path
[-1] not in self
.modinfo
[mod
].wsize
: return False
642 def mem_exists(self
, mod
, mem_path
):
643 for i
in range(len(mem_path
)-1):
644 if mod
not in self
.modinfo
: return False
645 if mem_path
[i
] not in self
.modinfo
[mod
].cells
: return False
646 mod
= self
.modinfo
[mod
].cells
[mem_path
[i
]]
648 if mod
not in self
.modinfo
: return False
649 if mem_path
[-1] not in self
.modinfo
[mod
].memories
: return False
652 def mem_expr(self
, mod
, base
, path
, port
=None, infomode
=False):
654 assert mod
in self
.modinfo
655 assert path
[0] in self
.modinfo
[mod
].memories
657 return self
.modinfo
[mod
].memories
[path
[0]]
658 return "(|%s_m%s %s| %s)" % (mod
, "" if port
is None else ":%s" % port
, path
[0], base
)
660 assert mod
in self
.modinfo
661 assert path
[0] in self
.modinfo
[mod
].cells
663 nextmod
= self
.modinfo
[mod
].cells
[path
[0]]
664 nextbase
= "(|%s_h %s| %s)" % (mod
, path
[0], base
)
665 return self
.mem_expr(nextmod
, nextbase
, path
[1:], port
=port
, infomode
=infomode
)
667 def mem_info(self
, mod
, path
):
668 return self
.mem_expr(mod
, "", path
, infomode
=True)
670 def get_net(self
, mod_name
, net_path
, state_name
):
671 return self
.get(self
.net_expr(mod_name
, state_name
, net_path
))
673 def get_net_list(self
, mod_name
, net_path_list
, state_name
):
674 return self
.get_list([self
.net_expr(mod_name
, state_name
, n
) for n
in net_path_list
])
676 def get_net_hex(self
, mod_name
, net_path
, state_name
):
677 return self
.bv2hex(self
.get_net(mod_name
, net_path
, state_name
))
679 def get_net_hex_list(self
, mod_name
, net_path_list
, state_name
):
680 return [self
.bv2hex(v
) for v
in self
.get_net_list(mod_name
, net_path_list
, state_name
)]
682 def get_net_bin(self
, mod_name
, net_path
, state_name
):
683 return self
.bv2bin(self
.get_net(mod_name
, net_path
, state_name
))
685 def get_net_bin_list(self
, mod_name
, net_path_list
, state_name
):
686 return [self
.bv2bin(v
) for v
in self
.get_net_list(mod_name
, net_path_list
, state_name
)]
689 if self
.p
is not None:
695 self
.shortopts
= "s:S:v"
696 self
.longopts
= ["unroll", "noincr", "noprogress", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"]
697 self
.solver
= "yices"
698 self
.solver_opts
= list()
699 self
.debug_print
= False
700 self
.debug_file
= None
701 self
.dummy_file
= None
704 self
.timeinfo
= os
.name
!= "nt"
706 self
.info_stmts
= list()
707 self
.nocomments
= False
709 def handle(self
, o
, a
):
713 self
.solver_opts
.append(a
)
715 self
.debug_print
= True
716 elif o
== "--unroll":
718 elif o
== "--noincr":
720 elif o
== "--noprogress":
721 self
.timeinfo
= False
722 elif o
== "--dump-smt2":
723 self
.debug_file
= open(a
, "w")
729 self
.info_stmts
.append(a
)
730 elif o
== "--nocomments":
731 self
.nocomments
= True
739 set SMT solver: z3, yices, boolector, cvc4, mathsat, dummy
743 pass <opt> as command line argument to the solver
746 use the specified SMT2 logic (e.g. QF_AUFBV)
749 if solver is "dummy", read solver output from that file
750 otherwise: write solver output to that file
756 unroll uninterpreted functions
759 don't use incremental solving, instead restart solver for
760 each (check-sat). This also avoids (push) and (pop).
763 disable timer display during solving
764 (this option is set implicitly on Windows)
766 --dump-smt2 <filename>
767 write smt2 statements to file
769 --info <smt2-info-stmt>
770 include the specified smt2 info statement in the smt2 output
773 strip all comments from the generated smt2 code
778 def __init__(self
, f
):
783 def add_net(self
, path
, width
):
786 key
= "n%d" % len(self
.nets
)
787 self
.nets
[path
] = (key
, width
)
789 def set_net(self
, path
, bits
):
792 assert path
in self
.nets
793 print("b%s %s" % (bits
, self
.nets
[path
][0]), file=self
.f
)
795 def set_time(self
, t
):
799 print("$var integer 32 t smt_step $end", file=self
.f
)
800 print("$var event 1 ! smt_clock $end", file=self
.f
)
802 for path
in sorted(self
.nets
):
803 while len(scope
)+1 > len(path
) or (len(scope
) > 0 and scope
[-1] != path
[len(scope
)-1]):
804 print("$upscope $end", file=self
.f
)
806 while len(scope
)+1 < len(path
):
807 print("$scope module %s $end" % path
[len(scope
)], file=self
.f
)
808 scope
.append(path
[len(scope
)-1])
809 key
, width
= self
.nets
[path
]
810 print("$var wire %d %s %s $end" % (width
, key
, path
[-1]), file=self
.f
)
811 for i
in range(len(scope
)):
812 print("$upscope $end", file=self
.f
)
813 print("$enddefinitions $end", file=self
.f
)
816 print("#%d" % (10 * self
.t
), file=self
.f
)
817 print("1!", file=self
.f
)
818 print("b%s t" % format(self
.t
, "032b"), file=self
.f
)