mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-06-24 14:53:42 +00:00
Code Activity

Add "yosys-smtbmc --btorwit" skeleton

Browse source 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-12-08 06:59:27 +01:00
parent ed3c57fad3
commit 47a5dfdaa4
1 changed files with 19 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

20
backends/smt2/smtbmc.py
View file

@ -32,6 +32,8 @@ cexfile = None
aimfile = None aimfile = None
aiwfile = None aiwfile = None
aigheader = True aigheader = True
btorfile = None
witfile = None
vlogtbfile = None vlogtbfile = None
vlogtbtop = None vlogtbtop = None
inconstr = list() inconstr = list()
@ -92,6 +94,10 @@ yosys-smtbmc [options] <yosys_smt2_output>
the AIGER witness file does not include the status and the AIGER witness file does not include the status and
properties lines. properties lines.
--btorwit <prefix>
--btorwit <btor_filename>:<witness_filename>
read a BTOR file and a BTOR witness for that BTOR file.
--noinfo --noinfo
only run the core proof, do not collect and print any only run the core proof, do not collect and print any
additional information (e.g. which assert failed) additional information (e.g. which assert failed)
@ -152,7 +158,7 @@ yosys-smtbmc [options] <yosys_smt2_output>
try: try:
opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts + opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "presat", ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "btorwit=", "presat",
"dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=", "dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
"smtc-init", "smtc-top=", "noinit"]) "smtc-init", "smtc-top=", "noinit"])
except: except:
@ -189,6 +195,12 @@ for o, a in opts:
aiwfile = a + ".aiw" aiwfile = a + ".aiw"
elif o == "--aig-noheader": elif o == "--aig-noheader":
aigheader = False aigheader = False
elif o == "--btorwit":
if ":" in a:
btorfile, witfile = a.split(":")
else:
btorfile = a + ".btor"
witfile = a + ".wit"
elif o == "--dump-vcd": elif o == "--dump-vcd":
vcdfile = a vcdfile = a
elif o == "--dump-vlogtb": elif o == "--dump-vlogtb":
@ -575,6 +587,12 @@ if aimfile is not None:
num_steps = max(num_steps, step+1) num_steps = max(num_steps, step+1)
step += 1 step += 1
if btorfile is not None:
print("The --btorwit feature is not implemented yet")
smt.write("(exit)")
smt.wait()
sys.exit(1)
def write_vcd_trace(steps_start, steps_stop, index): def write_vcd_trace(steps_start, steps_stop, index):
filename = vcdfile.replace("%", index) filename = vcdfile.replace("%", index)
print_msg("Writing trace to VCD file: %s" % (filename)) print_msg("Writing trace to VCD file: %s" % (filename))