Skeleton for Chip design

1 files changed, 67 insertions, 2 deletions

diff --git a/chip_design/ChipDesign.java b/chip_design/ChipDesign.java
index 2ec87e7..b7b986a 100644
--- a/chip_design/ChipDesign.java
+++ b/chip_design/ChipDesign.java
@@ -1,6 +1,71 @@
 public class ChipDesign {
-	
-	public static void main(String... args) {
 
+    private static final int CHIP_HEIGHT = 30;
+    private static final int CHIP_WIDTH = 30;
+
+    private static final int NR_OF_COMPONENTS = 10;
+
+    private static final int X = 0;
+    private static final int Y = 1;
+
+    private static final int NR_OF_POWER_COMPONENTS = 4;
+    private static final int[] POWER_COMPONENT = {4, 3};
+
+    private static final int[][] COMPONENTS = {
+            {4, 5},
+            {4, 6},
+            {5, 20},
+            {6, 9},
+            {6, 10},
+            {6, 11},
+            {7, 8},
+            {7, 12},
+            {10, 10},
+            {10, 20}
+    };
+
+    private static void print_predicates() {
+        for(int i = 0; i < NR_OF_COMPONENTS; i++) {
+            System.out.println("(Cx" + i + " Int) (Cy" + i + " Int)");
+            System.out.println("(Cr" + i + ")");
+        }
+        for(int i = 0; i < NR_OF_POWER_COMPONENTS; i++) {
+            System.out.println("(PCx" + i + " Int) (PCy" + i + " Int)");
+            System.out.println("(PCr" + i + ")");
+        }
+    }
+
+    private static void print_formula() {
+        for(int i = 0; i < NR_OF_COMPONENTS; i++) {
+            System.out.println("(>= Cx" + i + " 0) (>= Cy" + i + " 0)");
+            System.out.println("(<= (+ Cx" + i + " (ite (Cr" + i + ") " + COMPONENTS[i][Y] + " " + COMPONENTS[i][X] + ")) " + CHIP_WIDTH + ") (<= (+ Cy" + i + " (ite (Cr" + i + ") " + COMPONENTS[i][X] + " " + COMPONENTS[i][Y] + ")) " + CHIP_HEIGHT + ")");
+        }
+        for(int i = 0; i < NR_OF_POWER_COMPONENTS; i++) {
+            System.out.println("(>= PCx" + i + " 0) (>= PCy" + i + " 0)");
+            System.out.println("(<= (+ PCx" + i + " (ite (PCr" + i + ") " + COMPONENTS[i][Y] + " " + COMPONENTS[i][X] + ")) " + CHIP_WIDTH + ") (<= (+ PCy" + i + " (ite (PCr" + i + ") " + COMPONENTS[i][X] + " " + COMPONENTS[i][Y] + ")) " + CHIP_HEIGHT + ")");
+        }
+
+        /* Non-overlap constraint? It is not in the pdf, but it'd be weird if overlap was allowed */
+
+        /* Power requirement (connected edge) */
+
+        /* Heat production limit */
+        for(int i = 0; i < NR_OF_POWER_COMPONENTS; i++) {
+            for(int j = i + 1; j < NR_OF_POWER_COMPONENTS; j++) {
+                if(i == j) continue;
+                System.out.println("(or (> (- PCx" + i + " PCx" + j + ") 17) (> (- PCy" + i + " PCy" + j + ") 17) (> (- PCx" + j + " PCx" + i + ") 17) (> (- PCy" + j + " PCy" + i + ") 17))");
+            }
+        }
+    }
+
+	public static void main(String... args) {
+		System.out.println("(benchmark chip_design.smt");
+		System.out.println(":logic QF_UFLIA");
+		System.out.println(":extrafuns (");
+		print_predicates();
+		System.out.println(")");
+		System.out.println(":formula (and ");
+		print_formula();
+		System.out.println("))");
 	}
 }