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
, re
, os
, signal
20 import resource
, subprocess
21 from copy
import deepcopy
22 from select
import select
24 from queue
import Queue
, Empty
25 from threading
import Thread
28 # This is needed so that the recursive SMT2 S-expression parser
29 # does not run out of stack frames when parsing large expressions
30 smtio_reclimit
= 64 * 1024
31 smtio_stacksize
= 128 * 1024 * 1024
32 if sys
.getrecursionlimit() < smtio_reclimit
:
33 sys
.setrecursionlimit(smtio_reclimit
)
34 if resource
.getrlimit(resource
.RLIMIT_STACK
)[0] < smtio_stacksize
:
35 resource
.setrlimit(resource
.RLIMIT_STACK
, (smtio_stacksize
, -1))
38 # currently running solvers (so we can kill them)
39 running_solvers
= dict()
40 got_term_signal
= False
43 def sig_handler(signum
, frame
):
44 global got_term_signal
45 if not got_term_signal
:
46 print("<%s>" % signal
.Signals(signum
).name
)
47 got_term_signal
= True
48 for p
in running_solvers
.values():
49 os
.killpg(os
.getpgid(p
.pid
), signal
.SIGTERM
)
52 signal
.signal(signal
.SIGINT
, sig_handler
)
53 signal
.signal(signal
.SIGHUP
, sig_handler
)
54 signal
.signal(signal
.SIGTERM
, sig_handler
)
58 "0": "0000", "1": "0001", "2": "0010", "3": "0011",
59 "4": "0100", "5": "0101", "6": "0110", "7": "0111",
60 "8": "1000", "9": "1001", "A": "1010", "B": "1011",
61 "C": "1100", "D": "1101", "E": "1110", "F": "1111",
62 "a": "1010", "b": "1011", "c": "1100", "d": "1101",
63 "e": "1110", "f": "1111"
71 self
.registers
= set()
72 self
.memories
= dict()
79 self
.anyconsts
= dict()
81 self
.allconsts
= dict()
87 def __init__(self
, opts
=None):
97 self
.produce_models
= True
98 self
.smt2cache
= [list()]
100 self
.p_index
= solvers_index
104 self
.logic
= opts
.logic
105 self
.solver
= opts
.solver
106 self
.solver_opts
= opts
.solver_opts
107 self
.debug_print
= opts
.debug_print
108 self
.debug_file
= opts
.debug_file
109 self
.dummy_file
= opts
.dummy_file
110 self
.timeinfo
= opts
.timeinfo
111 self
.unroll
= opts
.unroll
112 self
.noincr
= opts
.noincr
113 self
.info_stmts
= opts
.info_stmts
114 self
.nocomments
= opts
.nocomments
117 self
.solver
= "yices"
118 self
.solver_opts
= list()
119 self
.debug_print
= False
120 self
.debug_file
= None
121 self
.dummy_file
= None
122 self
.timeinfo
= os
.name
!= "nt"
125 self
.info_stmts
= list()
126 self
.nocomments
= False
128 self
.start_time
= time()
130 self
.modinfo
= dict()
133 self
.setup_done
= False
136 if self
.p
is not None:
137 os
.killpg(os
.getpgid(self
.p
.pid
), signal
.SIGTERM
)
138 if running_solvers
is not None:
139 del running_solvers
[self
.p_index
]
142 assert not self
.setup_done
147 if self
.solver
== "yices":
148 self
.popen_vargs
= ['yices-smt2', '--incremental'] + self
.solver_opts
150 if self
.solver
== "z3":
151 self
.popen_vargs
= ['z3', '-smt2', '-in'] + self
.solver_opts
153 if self
.solver
== "cvc4":
154 self
.popen_vargs
= ['cvc4', '--incremental', '--lang', 'smt2.6' if self
.logic_dt
else 'smt2'] + self
.solver_opts
156 if self
.solver
== "mathsat":
157 self
.popen_vargs
= ['mathsat'] + self
.solver_opts
159 if self
.solver
== "boolector":
160 self
.popen_vargs
= ['boolector', '--smt2', '-i'] + self
.solver_opts
163 if self
.solver
== "abc":
164 if len(self
.solver_opts
) > 0:
165 self
.popen_vargs
= ['yosys-abc', '-S', '; '.join(self
.solver_opts
)]
167 self
.popen_vargs
= ['yosys-abc', '-S', '%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000']
168 self
.logic_ax
= False
172 if self
.solver
== "dummy":
173 assert self
.dummy_file
is not None
174 self
.dummy_fd
= open(self
.dummy_file
, "r")
176 if self
.dummy_file
is not None:
177 self
.dummy_fd
= open(self
.dummy_file
, "w")
182 assert not self
.forall
183 self
.logic_uf
= False
184 self
.unroll_idcnt
= 0
185 self
.unroll_buffer
= ""
186 self
.unroll_sorts
= set()
187 self
.unroll_objs
= set()
188 self
.unroll_decls
= dict()
189 self
.unroll_cache
= dict()
190 self
.unroll_stack
= list()
192 if self
.logic
is None:
194 if self
.logic_qf
: self
.logic
+= "QF_"
195 if self
.logic_ax
: self
.logic
+= "A"
196 if self
.logic_uf
: self
.logic
+= "UF"
197 if self
.logic_bv
: self
.logic
+= "BV"
198 if self
.logic_dt
: self
.logic
= "ALL"
200 self
.setup_done
= True
202 for stmt
in self
.info_stmts
:
205 if self
.produce_models
:
206 self
.write("(set-option :produce-models true)")
208 self
.write("(set-logic %s)" % self
.logic
)
211 secs
= int(time() - self
.start_time
)
212 return "## %6d %3d:%02d:%02d " % (secs
, secs
// (60*60), (secs
// 60) % 60, secs
% 60)
214 def replace_in_stmt(self
, stmt
, pat
, repl
):
218 if isinstance(stmt
, list):
219 return [self
.replace_in_stmt(s
, pat
, repl
) for s
in stmt
]
223 def unroll_stmt(self
, stmt
):
224 if not isinstance(stmt
, list):
227 stmt
= [self
.unroll_stmt(s
) for s
in stmt
]
229 if len(stmt
) >= 2 and not isinstance(stmt
[0], list) and stmt
[0] in self
.unroll_decls
:
230 assert stmt
[1] in self
.unroll_objs
233 if key
not in self
.unroll_cache
:
234 decl
= deepcopy(self
.unroll_decls
[key
[0]])
236 self
.unroll_cache
[key
] = "|UNROLL#%d|" % self
.unroll_idcnt
237 decl
[1] = self
.unroll_cache
[key
]
238 self
.unroll_idcnt
+= 1
240 if decl
[0] == "declare-fun":
241 if isinstance(decl
[3], list) or decl
[3] not in self
.unroll_sorts
:
242 self
.unroll_objs
.add(decl
[1])
245 self
.unroll_objs
.add(decl
[1])
248 elif decl
[0] == "define-fun":
250 for arg_name
, arg_sort
in decl
[2]:
251 decl
[4] = self
.replace_in_stmt(decl
[4], arg_name
, key
[arg_index
])
256 decl
= self
.unroll_stmt(decl
)
257 self
.write(self
.unparse(decl
), unroll
=False)
259 return self
.unroll_cache
[key
]
263 def p_thread_main(self
):
265 data
= self
.p
.stdout
.readline().decode("ascii")
267 self
.p_queue
.put(data
)
269 self
.p_running
= False
272 assert self
.p
is None
273 self
.p
= subprocess
.Popen(self
.popen_vargs
, stdin
=subprocess
.PIPE
, stdout
=subprocess
.PIPE
, stderr
=subprocess
.STDOUT
)
274 running_solvers
[self
.p_index
] = self
.p
275 self
.p_running
= True
277 self
.p_queue
= Queue()
278 self
.p_thread
= Thread(target
=self
.p_thread_main
)
279 self
.p_thread
.start()
281 def p_write(self
, data
, flush
):
282 assert self
.p
is not None
283 self
.p
.stdin
.write(bytes(data
, "ascii"))
284 if flush
: self
.p
.stdin
.flush()
287 assert self
.p
is not None
288 assert self
.p_running
289 if self
.p_next
is not None:
293 return self
.p_queue
.get()
296 assert self
.p
is not None
297 assert self
.p_running
298 if self
.p_next
is not None:
301 self
.p_next
= self
.p_queue
.get(True, 0.1)
307 assert self
.p
is not None
310 assert not self
.p_running
311 del running_solvers
[self
.p_index
]
317 def write(self
, stmt
, unroll
=True):
318 if stmt
.startswith(";"):
320 if not self
.setup_done
:
321 self
.info_stmts
.append(stmt
)
323 elif not self
.setup_done
:
328 if self
.nocomments
or self
.unroll
:
329 stmt
= re
.sub(r
" *;.*", "", stmt
)
330 if stmt
== "": return
332 if unroll
and self
.unroll
:
333 stmt
= self
.unroll_buffer
+ stmt
334 self
.unroll_buffer
= ""
336 s
= re
.sub(r
"\|[^|]*\|", "", stmt
)
337 if s
.count("(") != s
.count(")"):
338 self
.unroll_buffer
= stmt
+ " "
346 if len(s
) == 3 and s
[0] == "declare-sort" and s
[2] == "0":
347 self
.unroll_sorts
.add(s
[1])
350 elif len(s
) == 4 and s
[0] == "declare-fun" and s
[2] == [] and s
[3] in self
.unroll_sorts
:
351 self
.unroll_objs
.add(s
[1])
354 elif len(s
) >= 4 and s
[0] == "declare-fun":
355 for arg_sort
in s
[2]:
356 if arg_sort
in self
.unroll_sorts
:
357 self
.unroll_decls
[s
[1]] = s
360 elif len(s
) >= 4 and s
[0] == "define-fun":
361 for arg_name
, arg_sort
in s
[2]:
362 if arg_sort
in self
.unroll_sorts
:
363 self
.unroll_decls
[s
[1]] = s
366 stmt
= self
.unparse(self
.unroll_stmt(s
))
368 if stmt
== "(push 1)":
369 self
.unroll_stack
.append((
370 deepcopy(self
.unroll_sorts
),
371 deepcopy(self
.unroll_objs
),
372 deepcopy(self
.unroll_decls
),
373 deepcopy(self
.unroll_cache
),
376 if stmt
== "(pop 1)":
377 self
.unroll_sorts
, self
.unroll_objs
, self
.unroll_decls
, self
.unroll_cache
= self
.unroll_stack
.pop()
383 print(stmt
, file=self
.debug_file
)
384 self
.debug_file
.flush()
386 if self
.solver
!= "dummy":
388 if self
.p
is not None and not stmt
.startswith("(get-"):
390 if stmt
== "(push 1)":
391 self
.smt2cache
.append(list())
392 elif stmt
== "(pop 1)":
395 if self
.p
is not None:
396 self
.p_write(stmt
+ "\n", True)
397 self
.smt2cache
[-1].append(stmt
)
399 self
.p_write(stmt
+ "\n", True)
401 def info(self
, stmt
):
402 if not stmt
.startswith("; yosys-smt2-"):
405 fields
= stmt
.split()
407 if fields
[1] == "yosys-smt2-nomem":
408 if self
.logic
is None:
409 self
.logic_ax
= False
411 if fields
[1] == "yosys-smt2-nobv":
412 if self
.logic
is None:
413 self
.logic_bv
= False
415 if fields
[1] == "yosys-smt2-stdt":
416 if self
.logic
is None:
419 if fields
[1] == "yosys-smt2-forall":
420 if self
.logic
is None:
421 self
.logic_qf
= False
424 if fields
[1] == "yosys-smt2-module":
425 self
.curmod
= fields
[2]
426 self
.modinfo
[self
.curmod
] = SmtModInfo()
428 if fields
[1] == "yosys-smt2-cell":
429 self
.modinfo
[self
.curmod
].cells
[fields
[3]] = fields
[2]
431 if fields
[1] == "yosys-smt2-topmod":
432 self
.topmod
= fields
[2]
434 if fields
[1] == "yosys-smt2-input":
435 self
.modinfo
[self
.curmod
].inputs
.add(fields
[2])
436 self
.modinfo
[self
.curmod
].wsize
[fields
[2]] = int(fields
[3])
438 if fields
[1] == "yosys-smt2-output":
439 self
.modinfo
[self
.curmod
].outputs
.add(fields
[2])
440 self
.modinfo
[self
.curmod
].wsize
[fields
[2]] = int(fields
[3])
442 if fields
[1] == "yosys-smt2-register":
443 self
.modinfo
[self
.curmod
].registers
.add(fields
[2])
444 self
.modinfo
[self
.curmod
].wsize
[fields
[2]] = int(fields
[3])
446 if fields
[1] == "yosys-smt2-memory":
447 self
.modinfo
[self
.curmod
].memories
[fields
[2]] = (int(fields
[3]), int(fields
[4]), int(fields
[5]), int(fields
[6]), fields
[7] == "async")
449 if fields
[1] == "yosys-smt2-wire":
450 self
.modinfo
[self
.curmod
].wires
.add(fields
[2])
451 self
.modinfo
[self
.curmod
].wsize
[fields
[2]] = int(fields
[3])
453 if fields
[1] == "yosys-smt2-clock":
454 for edge
in fields
[3:]:
455 if fields
[2] not in self
.modinfo
[self
.curmod
].clocks
:
456 self
.modinfo
[self
.curmod
].clocks
[fields
[2]] = edge
457 elif self
.modinfo
[self
.curmod
].clocks
[fields
[2]] != edge
:
458 self
.modinfo
[self
.curmod
].clocks
[fields
[2]] = "event"
460 if fields
[1] == "yosys-smt2-assert":
461 self
.modinfo
[self
.curmod
].asserts
["%s_a %s" % (self
.curmod
, fields
[2])] = fields
[3]
463 if fields
[1] == "yosys-smt2-cover":
464 self
.modinfo
[self
.curmod
].covers
["%s_c %s" % (self
.curmod
, fields
[2])] = fields
[3]
466 if fields
[1] == "yosys-smt2-anyconst":
467 self
.modinfo
[self
.curmod
].anyconsts
[fields
[2]] = (fields
[4], None if len(fields
) <= 5 else fields
[5])
468 self
.modinfo
[self
.curmod
].asize
[fields
[2]] = int(fields
[3])
470 if fields
[1] == "yosys-smt2-anyseq":
471 self
.modinfo
[self
.curmod
].anyseqs
[fields
[2]] = (fields
[4], None if len(fields
) <= 5 else fields
[5])
472 self
.modinfo
[self
.curmod
].asize
[fields
[2]] = int(fields
[3])
474 if fields
[1] == "yosys-smt2-allconst":
475 self
.modinfo
[self
.curmod
].allconsts
[fields
[2]] = (fields
[4], None if len(fields
) <= 5 else fields
[5])
476 self
.modinfo
[self
.curmod
].asize
[fields
[2]] = int(fields
[3])
478 if fields
[1] == "yosys-smt2-allseq":
479 self
.modinfo
[self
.curmod
].allseqs
[fields
[2]] = (fields
[4], None if len(fields
) <= 5 else fields
[5])
480 self
.modinfo
[self
.curmod
].asize
[fields
[2]] = int(fields
[3])
482 def hiernets(self
, top
, regs_only
=False):
483 def hiernets_worker(nets
, mod
, cursor
):
484 for netname
in sorted(self
.modinfo
[mod
].wsize
.keys()):
485 if not regs_only
or netname
in self
.modinfo
[mod
].registers
:
486 nets
.append(cursor
+ [netname
])
487 for cellname
, celltype
in sorted(self
.modinfo
[mod
].cells
.items()):
488 hiernets_worker(nets
, celltype
, cursor
+ [cellname
])
491 hiernets_worker(nets
, top
, [])
494 def hieranyconsts(self
, top
):
495 def worker(results
, mod
, cursor
):
496 for name
, value
in sorted(self
.modinfo
[mod
].anyconsts
.items()):
497 width
= self
.modinfo
[mod
].asize
[name
]
498 results
.append((cursor
, name
, value
[0], value
[1], width
))
499 for cellname
, celltype
in sorted(self
.modinfo
[mod
].cells
.items()):
500 worker(results
, celltype
, cursor
+ [cellname
])
503 worker(results
, top
, [])
506 def hieranyseqs(self
, top
):
507 def worker(results
, mod
, cursor
):
508 for name
, value
in sorted(self
.modinfo
[mod
].anyseqs
.items()):
509 width
= self
.modinfo
[mod
].asize
[name
]
510 results
.append((cursor
, name
, value
[0], value
[1], width
))
511 for cellname
, celltype
in sorted(self
.modinfo
[mod
].cells
.items()):
512 worker(results
, celltype
, cursor
+ [cellname
])
515 worker(results
, top
, [])
518 def hierallconsts(self
, top
):
519 def worker(results
, mod
, cursor
):
520 for name
, value
in sorted(self
.modinfo
[mod
].allconsts
.items()):
521 width
= self
.modinfo
[mod
].asize
[name
]
522 results
.append((cursor
, name
, value
[0], value
[1], width
))
523 for cellname
, celltype
in sorted(self
.modinfo
[mod
].cells
.items()):
524 worker(results
, celltype
, cursor
+ [cellname
])
527 worker(results
, top
, [])
530 def hierallseqs(self
, top
):
531 def worker(results
, mod
, cursor
):
532 for name
, value
in sorted(self
.modinfo
[mod
].allseqs
.items()):
533 width
= self
.modinfo
[mod
].asize
[name
]
534 results
.append((cursor
, name
, value
[0], value
[1], width
))
535 for cellname
, celltype
in sorted(self
.modinfo
[mod
].cells
.items()):
536 worker(results
, celltype
, cursor
+ [cellname
])
539 worker(results
, top
, [])
542 def hiermems(self
, top
):
543 def hiermems_worker(mems
, mod
, cursor
):
544 for memname
in sorted(self
.modinfo
[mod
].memories
.keys()):
545 mems
.append(cursor
+ [memname
])
546 for cellname
, celltype
in sorted(self
.modinfo
[mod
].cells
.items()):
547 hiermems_worker(mems
, celltype
, cursor
+ [cellname
])
550 hiermems_worker(mems
, top
, [])
558 if self
.solver
== "dummy":
559 line
= self
.dummy_fd
.readline().strip()
561 line
= self
.p_read().strip()
562 if self
.dummy_file
is not None:
563 self
.dummy_fd
.write(line
+ "\n")
565 count_brackets
+= line
.count("(")
566 count_brackets
-= line
.count(")")
571 if count_brackets
== 0:
573 if self
.solver
!= "dummy" and self
.p
.poll():
574 print("SMT Solver terminated unexpectedly: %s" % "".join(stmt
), flush
=True)
578 if stmt
.startswith("(error"):
579 print("SMT Solver Error: %s" % stmt
, file=sys
.stderr
, flush
=True)
580 if self
.solver
!= "dummy":
588 print("> (check-sat)")
589 if self
.debug_file
and not self
.nocomments
:
590 print("; running check-sat..", file=self
.debug_file
)
591 self
.debug_file
.flush()
593 if self
.solver
!= "dummy":
595 if self
.p
is not None:
598 for cache_ctx
in self
.smt2cache
:
599 for cache_stmt
in cache_ctx
:
600 self
.p_write(cache_stmt
+ "\n", False)
602 self
.p_write("(check-sat)\n", True)
616 if count
% 10 == 0 or count
== 25:
620 m
= "(%d seconds)" % secs
622 m
= "(%d seconds -- %d:%02d)" % (secs
, secs
// 60, secs
% 60)
624 m
= "(%d seconds -- %d:%02d:%02d)" % (secs
, secs
// (60*60), (secs
// 60) % 60, secs
% 60)
626 print("%s %s %c" % ("\b \b" * num_bs
, m
, s
[i
]), end
="", file=sys
.stderr
)
630 print("\b" + s
[i
], end
="", file=sys
.stderr
)
636 print("\b \b" * num_bs
, end
="", file=sys
.stderr
)
641 print("(set-info :status %s)" % result
, file=self
.debug_file
)
642 print("(check-sat)", file=self
.debug_file
)
643 self
.debug_file
.flush()
646 def parse(self
, stmt
):
651 while stmt
[cursor
] != ')':
652 el
, le
= worker(stmt
[cursor
:])
655 return expr
, cursor
+1
660 while stmt
[cursor
] != '|':
664 return expr
, cursor
+1
666 if stmt
[0] in [" ", "\t", "\r", "\n"]:
667 el
, le
= worker(stmt
[1:])
672 while stmt
[cursor
] not in ["(", ")", "|", " ", "\t", "\r", "\n"]:
676 return worker(stmt
)[0]
678 def unparse(self
, stmt
):
679 if isinstance(stmt
, list):
680 return "(" + " ".join([self
.unparse(s
) for s
in stmt
]) + ")"
688 if len(v
) > 0 and v
[-1] == "1": d
+= 1
689 if len(v
) > 1 and v
[-2] == "1": d
+= 2
690 if len(v
) > 2 and v
[-3] == "1": d
+= 4
691 if len(v
) > 3 and v
[-4] == "1": d
+= 8
698 if v
== "true": return "1"
699 if v
== "false": return "0"
700 if v
.startswith("#b"):
702 if v
.startswith("#x"):
703 return "".join(hex_dict
.get(x
) for x
in v
[2:])
707 return int(self
.bv2bin(v
), 2)
710 self
.write("(get-value (%s))" % (expr
))
711 return self
.parse(self
.read())[0][1]
713 def get_list(self
, expr_list
):
714 if len(expr_list
) == 0:
716 self
.write("(get-value (%s))" % " ".join(expr_list
))
717 return [n
[1] for n
in self
.parse(self
.read())]
719 def get_path(self
, mod
, path
):
720 assert mod
in self
.modinfo
721 path
= path
.split(".")
723 for i
in range(len(path
)-1):
724 first
= ".".join(path
[0:i
+1])
725 second
= ".".join(path
[i
+1:])
727 if first
in self
.modinfo
[mod
].cells
:
728 nextmod
= self
.modinfo
[mod
].cells
[first
]
729 return [first
] + self
.get_path(nextmod
, second
)
731 return [".".join(path
)]
733 def net_expr(self
, mod
, base
, path
):
738 assert mod
in self
.modinfo
741 if path
[0] in self
.modinfo
[mod
].cells
:
742 return "(|%s_h %s| %s)" % (mod
, path
[0], base
)
743 if path
[0] in self
.modinfo
[mod
].wsize
:
744 return "(|%s_n %s| %s)" % (mod
, path
[0], base
)
745 if path
[0] in self
.modinfo
[mod
].memories
:
746 return "(|%s_m %s| %s)" % (mod
, path
[0], base
)
749 assert mod
in self
.modinfo
750 assert path
[0] in self
.modinfo
[mod
].cells
752 nextmod
= self
.modinfo
[mod
].cells
[path
[0]]
753 nextbase
= "(|%s_h %s| %s)" % (mod
, path
[0], base
)
754 return self
.net_expr(nextmod
, nextbase
, path
[1:])
756 def net_width(self
, mod
, net_path
):
757 for i
in range(len(net_path
)-1):
758 assert mod
in self
.modinfo
759 assert net_path
[i
] in self
.modinfo
[mod
].cells
760 mod
= self
.modinfo
[mod
].cells
[net_path
[i
]]
762 assert mod
in self
.modinfo
763 assert net_path
[-1] in self
.modinfo
[mod
].wsize
764 return self
.modinfo
[mod
].wsize
[net_path
[-1]]
766 def net_clock(self
, mod
, net_path
):
767 for i
in range(len(net_path
)-1):
768 assert mod
in self
.modinfo
769 assert net_path
[i
] in self
.modinfo
[mod
].cells
770 mod
= self
.modinfo
[mod
].cells
[net_path
[i
]]
772 assert mod
in self
.modinfo
773 if net_path
[-1] not in self
.modinfo
[mod
].clocks
:
775 return self
.modinfo
[mod
].clocks
[net_path
[-1]]
777 def net_exists(self
, mod
, net_path
):
778 for i
in range(len(net_path
)-1):
779 if mod
not in self
.modinfo
: return False
780 if net_path
[i
] not in self
.modinfo
[mod
].cells
: return False
781 mod
= self
.modinfo
[mod
].cells
[net_path
[i
]]
783 if mod
not in self
.modinfo
: return False
784 if net_path
[-1] not in self
.modinfo
[mod
].wsize
: return False
787 def mem_exists(self
, mod
, mem_path
):
788 for i
in range(len(mem_path
)-1):
789 if mod
not in self
.modinfo
: return False
790 if mem_path
[i
] not in self
.modinfo
[mod
].cells
: return False
791 mod
= self
.modinfo
[mod
].cells
[mem_path
[i
]]
793 if mod
not in self
.modinfo
: return False
794 if mem_path
[-1] not in self
.modinfo
[mod
].memories
: return False
797 def mem_expr(self
, mod
, base
, path
, port
=None, infomode
=False):
799 assert mod
in self
.modinfo
800 assert path
[0] in self
.modinfo
[mod
].memories
802 return self
.modinfo
[mod
].memories
[path
[0]]
803 return "(|%s_m%s %s| %s)" % (mod
, "" if port
is None else ":%s" % port
, path
[0], base
)
805 assert mod
in self
.modinfo
806 assert path
[0] in self
.modinfo
[mod
].cells
808 nextmod
= self
.modinfo
[mod
].cells
[path
[0]]
809 nextbase
= "(|%s_h %s| %s)" % (mod
, path
[0], base
)
810 return self
.mem_expr(nextmod
, nextbase
, path
[1:], port
=port
, infomode
=infomode
)
812 def mem_info(self
, mod
, path
):
813 return self
.mem_expr(mod
, "", path
, infomode
=True)
815 def get_net(self
, mod_name
, net_path
, state_name
):
816 return self
.get(self
.net_expr(mod_name
, state_name
, net_path
))
818 def get_net_list(self
, mod_name
, net_path_list
, state_name
):
819 return self
.get_list([self
.net_expr(mod_name
, state_name
, n
) for n
in net_path_list
])
821 def get_net_hex(self
, mod_name
, net_path
, state_name
):
822 return self
.bv2hex(self
.get_net(mod_name
, net_path
, state_name
))
824 def get_net_hex_list(self
, mod_name
, net_path_list
, state_name
):
825 return [self
.bv2hex(v
) for v
in self
.get_net_list(mod_name
, net_path_list
, state_name
)]
827 def get_net_bin(self
, mod_name
, net_path
, state_name
):
828 return self
.bv2bin(self
.get_net(mod_name
, net_path
, state_name
))
830 def get_net_bin_list(self
, mod_name
, net_path_list
, state_name
):
831 return [self
.bv2bin(v
) for v
in self
.get_net_list(mod_name
, net_path_list
, state_name
)]
834 if self
.p
is not None:
841 self
.shortopts
= "s:S:v"
842 self
.longopts
= ["unroll", "noincr", "noprogress", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"]
843 self
.solver
= "yices"
844 self
.solver_opts
= list()
845 self
.debug_print
= False
846 self
.debug_file
= None
847 self
.dummy_file
= None
850 self
.timeinfo
= os
.name
!= "nt"
852 self
.info_stmts
= list()
853 self
.nocomments
= False
855 def handle(self
, o
, a
):
859 self
.solver_opts
.append(a
)
861 self
.debug_print
= True
862 elif o
== "--unroll":
864 elif o
== "--noincr":
866 elif o
== "--noprogress":
867 self
.timeinfo
= False
868 elif o
== "--dump-smt2":
869 self
.debug_file
= open(a
, "w")
875 self
.info_stmts
.append(a
)
876 elif o
== "--nocomments":
877 self
.nocomments
= True
885 set SMT solver: z3, yices, boolector, cvc4, mathsat, dummy
889 pass <opt> as command line argument to the solver
892 use the specified SMT2 logic (e.g. QF_AUFBV)
895 if solver is "dummy", read solver output from that file
896 otherwise: write solver output to that file
902 unroll uninterpreted functions
905 don't use incremental solving, instead restart solver for
906 each (check-sat). This also avoids (push) and (pop).
909 disable timer display during solving
910 (this option is set implicitly on Windows)
912 --dump-smt2 <filename>
913 write smt2 statements to file
915 --info <smt2-info-stmt>
916 include the specified smt2 info statement in the smt2 output
919 strip all comments from the generated smt2 code
924 def __init__(self
, f
):
930 def add_net(self
, path
, width
):
933 key
= "n%d" % len(self
.nets
)
934 self
.nets
[path
] = (key
, width
)
936 def add_clock(self
, path
, edge
):
939 key
= "n%d" % len(self
.nets
)
940 self
.nets
[path
] = (key
, 1)
941 self
.clocks
[path
] = (key
, edge
)
943 def set_net(self
, path
, bits
):
946 assert path
in self
.nets
947 if path
not in self
.clocks
:
948 print("b%s %s" % (bits
, self
.nets
[path
][0]), file=self
.f
)
950 def escape_name(self
, name
):
951 name
= re
.sub(r
"\[([a-zA-Z_][0-9a-zA-Z_]*)\]", r
".\1", name
)
952 if re
.match("[\[\]]", name
) and name
[0] != "\\":
956 def set_time(self
, t
):
960 print("$var integer 32 t smt_step $end", file=self
.f
)
961 print("$var event 1 ! smt_clock $end", file=self
.f
)
963 for path
in sorted(self
.nets
):
964 while len(scope
)+1 > len(path
) or (len(scope
) > 0 and scope
[-1] != path
[len(scope
)-1]):
965 print("$upscope $end", file=self
.f
)
967 while len(scope
)+1 < len(path
):
968 print("$scope module %s $end" % path
[len(scope
)], file=self
.f
)
969 scope
.append(path
[len(scope
)-1])
970 key
, width
= self
.nets
[path
]
971 if path
in self
.clocks
and self
.clocks
[path
][1] == "event":
972 print("$var event 1 %s %s $end" % (key
, self
.escape_name(path
[-1])), file=self
.f
)
974 print("$var wire %d %s %s $end" % (width
, key
, self
.escape_name(path
[-1])), file=self
.f
)
975 for i
in range(len(scope
)):
976 print("$upscope $end", file=self
.f
)
977 print("$enddefinitions $end", file=self
.f
)
983 print("#%d" % (10 * self
.t
- 5), file=self
.f
)
984 for path
in sorted(self
.clocks
.keys()):
985 if self
.clocks
[path
][1] == "posedge":
986 print("b0 %s" % self
.nets
[path
][0], file=self
.f
)
987 elif self
.clocks
[path
][1] == "negedge":
988 print("b1 %s" % self
.nets
[path
][0], file=self
.f
)
990 print("#%d" % (10 * self
.t
), file=self
.f
)
991 print("1!", file=self
.f
)
992 print("b%s t" % format(self
.t
, "032b"), file=self
.f
)
994 for path
in sorted(self
.clocks
.keys()):
995 if self
.clocks
[path
][1] == "negedge":
996 print("b0 %s" % self
.nets
[path
][0], file=self
.f
)
998 print("b1 %s" % self
.nets
[path
][0], file=self
.f
)