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
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
|
public class ChipDesign {
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("))");
}
}
|
