ChipDesign: added generator

1 files changed, 132 insertions, 0 deletions

diff --git a/chip_design/generate-chipdesign.py b/chip_design/generate-chipdesign.py
new file mode 100755
index 0000000..d231c8d
--- /dev/null
+++ b/chip_design/generate-chipdesign.py
@@ -0,0 +1,132 @@
+#!/usr/bin/env python
+# Run with: $0 | z3 -smt -in
+
+# Power components
+powers = [
+    (4, 3),
+    (4, 3),
+]
+
+# Regular components
+regulars = [
+    (4, 5),
+    (4, 6),
+    (5, 20),
+    (6, 9),
+    (6, 10),
+    (6, 11),
+    (7, 8),
+    (7, 12),
+    (10, 10),
+    (10, 20),
+]
+
+# Chip dimensions
+chip_w, chip_h = (30, 30)
+
+# Minimum distance between centers
+power_distance = 17
+
+
+all_components = powers + regulars
+
+def fillin(cases, template_vars):
+    if type(cases) == str:
+        return cases.format(**template_vars)
+    return [template.format(**template_vars) for template in cases]
+
+
+literals = []
+preds = []
+# Add X and Y coordinate for each component,
+# and also the width/height
+for i, (w, h) in enumerate(all_components):
+    var_x = 'x%d' % i
+    var_y = 'y%d' % i
+    var_w = 'w%d' % i
+    var_h = 'h%d' % i
+    literals += [
+        var_x,
+        var_y,
+        var_w,
+        var_h,
+    ]
+    # Ensure each component stays in chip area
+    newpreds = [
+        '(>= {var_x} 0)',
+        '(>= {var_y} 0)',
+        '(<= {var_x} {chip_w})',
+        '(<= {var_y} {chip_h})',
+    ]
+    # Dimensions are restricted:
+    # either width and height are w, h; or they are rotated.
+    newpreds += [
+        '(or'
+        ' (and (= {var_w} {w}) (= {var_h} {h}))'
+        ' (and (= {var_w} {h}) (= {var_h} {w}))'
+        ')',
+    ]
+    # Fill in template with vars
+    preds += fillin(newpreds, vars())
+
+# Avoid overlap between any pair, so any other component must be outside the
+# current pivot.
+for i in range(len(all_components)):
+    for j in range(len(all_components)):
+        if i == j:
+            continue
+        # other (j) must be below, on the left of pivot (i).
+        # or above or on the right (mind the width/height!).
+        altpreds = [
+            '(<= y{j} y{i})',
+            '(<= x{j} x{i})',
+            '(>= y{j} (+ y{i} h{i}))',
+            '(>= x{j} (+ x{i} x{i}))',
+        ]
+        preds += ['(or %s)' % ' '.join(fillin(altpreds, vars()))]
+
+# require minimum distance between power components
+for i in range(len(powers)):
+    for j in range(len(powers)):
+        if i == j:
+            continue
+        # need center_i >= center_j + distance (for center from {X,Y}, repeat
+        # for i and j swapped in case j occurs after i)
+        # center = x + w / 2
+        center_x_i = fillin('(+ x{i} (/ w{i} 2))', vars())
+        center_y_i = fillin('(+ y{i} (/ h{i} 2))', vars())
+        center_x_j = fillin('(+ x{j} (/ w{j} 2))', vars())
+        center_y_j = fillin('(+ y{j} (/ h{j} 2))', vars())
+        altpreds = [
+            '(>= {center_x_i} (+ {center_x_j} {power_distance}))',
+            '(>= {center_x_j} (+ {center_x_i} {power_distance}))',
+            '(>= {center_y_i} (+ {center_y_j} {power_distance}))',
+            '(>= {center_y_j} (+ {center_y_i} {power_distance}))',
+        ]
+        preds += ['(or %s)' % ' '.join(fillin(altpreds, vars()))]
+
+# Begin generator
+s = """(benchmark test.smt
+:logic QF_UFLRA
+:extrafuns
+(
+"""
+s += "\n".join("(%s Real)" % x for x in literals)
+s += """
+)
+:formula
+(and
+"""
+s += "\n".join(preds)
+s += """
+))
+"""
+
+try:
+    import sys
+    print(s)
+    # Hack to avoid printing a ugly error in case stdin of next pipe is closed.
+    sys.stdout.flush()
+    sys.stdout.close()
+except BrokenPipeError:
+    pass