-
Notifications
You must be signed in to change notification settings - Fork 7
/
simple_main.py
48 lines (38 loc) · 1.58 KB
/
simple_main.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
import ConfigParser
import os
import tempfile
import Netlist_to_Z3_latency_nor2
def main():
# Read configuration parameters
config = ConfigParser.ConfigParser()
config.readfp(open('simple_conf.cfg'))
input_path = config.get('input_output', 'input_path')
input_format = config.get('input_output', 'input_format')
abc_dir_path = config.get('abc', 'abc_dir_path')
Z3_path = config.get('Z3', 'Z3_path')
output_path = config.get('input_output', 'output_path')
abc_exe_path = os.path.join(abc_dir_path, "abc")
abc_rc_path = os.path.join(abc_dir_path, "abc.rc")
# Create abc script
abc_script = file('abc_script_template.abc', 'rb').read()
abc_script = abc_script.replace('abc_rc_path', abc_rc_path)
abc_script = abc_script.replace('input.blif', input_path)
if input_format == 'verilog':
abc_script = abc_script.replace('read_blif', 'read_verilog')
abc_script = abc_script.replace('lib.genlib', 'mcnc1_nor2.genlib')
abc_output_path = tempfile.mktemp()
abc_script = abc_script.replace('output.v', abc_output_path)
# Run abc script
abc_script_path = tempfile.mktemp()
file(abc_script_path, "wb").write(abc_script)
os.system('%s -f "%s"' % (abc_exe_path, abc_script_path))
# Create constraints file (smt2 format)
Z3_input = Netlist_to_Z3_latency_nor2.netlist_to_z3(abc_output_path)
# Run Z3
os.system('%s -smt2 %s > %s' % (Z3_path, Z3_input, output_path))
# Clean files
os.remove(abc_script_path)
os.remove(abc_output_path)
os.remove(Z3_input)
if __name__ == "__main__":
main()