From 94163b31d8b7359f2d677eae8c6db3da63502b01 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 4 Sep 2017 14:47:05 -0400 Subject: Add display files (temporary, kind-of) --- etc/compile-by-zinc/femulData0.dot | 189 ++++ etc/compile-by-zinc/femulData0.png | Bin 0 -> 648863 bytes etc/compile-by-zinc/femulData0.svg | 1339 +++++++++++++++++++++++++++++ etc/compile-by-zinc/femulData0_1.png | Bin 0 -> 452548 bytes etc/compile-by-zinc/femulData0_1.svg | 1118 ++++++++++++++++++++++++ etc/compile-by-zinc/femulDisplayReg_0.mzn | 145 ++++ etc/compile-by-zinc/femulDisplayReg_1.mzn | 147 ++++ etc/compile-by-zinc/femulDisplayReg_2.mzn | 66 ++ etc/compile-by-zinc/femulDisplayReg_3.mzn | 66 ++ etc/compile-by-zinc/femulDisplay_0.mzn | 164 ++++ etc/compile-by-zinc/femulDisplay_1.mzn | 92 ++ 11 files changed, 3326 insertions(+) create mode 100644 etc/compile-by-zinc/femulData0.dot create mode 100644 etc/compile-by-zinc/femulData0.png create mode 100644 etc/compile-by-zinc/femulData0.svg create mode 100644 etc/compile-by-zinc/femulData0_1.png create mode 100644 etc/compile-by-zinc/femulData0_1.svg create mode 100644 etc/compile-by-zinc/femulDisplayReg_0.mzn create mode 100644 etc/compile-by-zinc/femulDisplayReg_1.mzn create mode 100644 etc/compile-by-zinc/femulDisplayReg_2.mzn create mode 100644 etc/compile-by-zinc/femulDisplayReg_3.mzn create mode 100644 etc/compile-by-zinc/femulDisplay_0.mzn create mode 100644 etc/compile-by-zinc/femulDisplay_1.mzn (limited to 'etc') diff --git a/etc/compile-by-zinc/femulData0.dot b/etc/compile-by-zinc/femulData0.dot new file mode 100644 index 000000000..e4caf9720 --- /dev/null +++ b/etc/compile-by-zinc/femulData0.dot @@ -0,0 +1,189 @@ +digraph G { + x90 [label="x90 (r13)",fillcolor="gold"]; + x75 [label="x75 (r8)",fillcolor="brown"]; + x58_128 [label="x58_128 (RSP:r13)",fillcolor="blueviolet"]; + x69 [label="x69 (RBP)",fillcolor="blue"]; + x68_128 [label="x68_128 (r9:r14)",fillcolor="cadetblue"]; + x44_128 [label="x44_128 (r12:r15)",fillcolor="red"]; + x42_128 [label="x42_128 (r12:r15)",fillcolor="red"]; + x40_128 [label="x40_128 (r12:r15)",fillcolor="red"]; + x60_128 [label="x60_128 (RSP:r13)",fillcolor="blueviolet"]; + x62_128 [label="x62_128 (RSP:r13)",fillcolor="blueviolet"]; + x64_128 [label="x64_128 (r8:r10)",fillcolor="brown"]; + x66_128 [label="x66_128 (r8:r10)",fillcolor="brown"]; + x29_128 [label="x29_128 (r9:r14)",fillcolor="cadetblue"]; + x28_128 [label="x28_128 (r8:r10)",fillcolor="brown"]; + x24_128 [label="x24_128 (r8:r10)",fillcolor="brown"]; + x26_128 [label="x26_128 (r8:r10)",fillcolor="brown"]; + x21_128 [label="x21_128 (RSP:r13)",fillcolor="blueviolet"]; + x20_128 [label="x20_128 (RBP:r11)",fillcolor="blue"]; + x23_128 [label="x23_128 (RSP:r13)",fillcolor="blueviolet"]; + x83 [label="x83 (r12)",fillcolor="red"]; + x82 [label="x82 (r15)",fillcolor="darkorange"]; + x81 [label="x81 (r12)",fillcolor="red"]; + x80_128 [label="x80_128 (r12:r15)",fillcolor="red"]; + x87 [label="x87 (r12)",fillcolor="red"]; + x86 [label="x86 (r11)",fillcolor="cyan"]; + x85 [label="x85 (r12)",fillcolor="red"]; + x84 [label="x84 (r11)",fillcolor="cyan"]; + x89 [label="x89 (r12)",fillcolor="red"]; + x88 [label="x88 (r13)",fillcolor="gold"]; + x50_128 [label="x50_128 (RBP:r11)",fillcolor="blue"]; + x5 [label="x5 (r12)",fillcolor="red"]; + x54_128 [label="x54_128 (RBP:r11)",fillcolor="blue"]; + x33_128 [label="x33_128 (r9:r14)",fillcolor="cadetblue"]; + x56_128 [label="x56_128 (RBP:r11)",fillcolor="blue"]; + x31_128 [label="x31_128 (r9:r14)",fillcolor="cadetblue"]; + x36_128 [label="x36_128 (r12:r15)",fillcolor="red"]; + x52_128 [label="x52_128 (RBP:r11)",fillcolor="blue"]; + x78 [label="x78 (r9)",fillcolor="cadetblue"]; + x79 [label="x79 (r14)",fillcolor="deeppink"]; + x76 [label="x76 (r10)",fillcolor="chartreuse"]; + x77_128 [label="x77_128 (r9:r14)",fillcolor="cadetblue"]; + x38_128 [label="x38_128 (r12:r15)",fillcolor="red"]; + x35_128 [label="x35_128 (r9:r14)",fillcolor="cadetblue"]; + x72 [label="x72 (RSP)",fillcolor="blueviolet"]; + x73 [label="x73 (r13)",fillcolor="gold"]; + x70 [label="x70 (r11)",fillcolor="cyan"]; + x71_128 [label="x71_128 (RSP:r13)",fillcolor="blueviolet"]; + x18 [label="x18 (r15)",fillcolor="darkorange"]; + x74_128 [label="x74_128 (r8:r10)",fillcolor="brown"]; + in -> x10 ; + in -> x11 ; + in -> x9 ; + in -> x7 ; + in -> x5 ; + in -> x18 ; + in -> x19 ; + in -> x17 ; + in -> x15 ; + in -> x13 ; + x82 -> out ; + x79 -> out ; + x90 -> out ; + x89 -> out ; + x86 -> out ; + x13 -> x20_128 ; + x5 -> x20_128 ; + x15 -> x21_128 ; + x5 -> x21_128 ; + x13 -> x22_128 ; + x7 -> x22_128 ; + x21_128 -> x23_128 ; + x22_128 -> x23_128 ; + x17 -> x24_128 ; + x5 -> x24_128 ; + x13 -> x25_128 ; + x9 -> x25_128 ; + x24_128 -> x26_128 ; + x25_128 -> x26_128 ; + x15 -> x27_128 ; + x7 -> x27_128 ; + x26_128 -> x28_128 ; + x27_128 -> x28_128 ; + x19 -> x29_128 ; + x5 -> x29_128 ; + x11 -> x30_128 ; + x13 -> x30_128 ; + x29_128 -> x31_128 ; + x30_128 -> x31_128 ; + x17 -> x32_128 ; + x7 -> x32_128 ; + x31_128 -> x33_128 ; + x32_128 -> x33_128 ; + x15 -> x34_128 ; + x9 -> x34_128 ; + x33_128 -> x35_128 ; + x34_128 -> x35_128 ; + x18 -> x36_128 ; + x5 -> x36_128 ; + x10 -> x37_128 ; + x13 -> x37_128 ; + x36_128 -> x38_128 ; + x37_128 -> x38_128 ; + x11 -> x39_128 ; + x15 -> x39_128 ; + x38_128 -> x40_128 ; + x39_128 -> x40_128 ; + x19 -> x41_128 ; + x7 -> x41_128 ; + x40_128 -> x42_128 ; + x41_128 -> x42_128 ; + x17 -> x43_128 ; + x9 -> x43_128 ; + x42_128 -> x44_128 ; + x43_128 -> x44_128 ; + x10 -> x45 ; + x7 -> x46 ; + x9 -> x47 ; + x11 -> x48 ; + x15 -> x49_128 ; + x45 -> x49_128 ; + x20_128 -> x50_128 ; + x49_128 -> x50_128 ; + x18 -> x51_128 ; + x46 -> x51_128 ; + x50_128 -> x52_128 ; + x51_128 -> x52_128 ; + x19 -> x53_128 ; + x47 -> x53_128 ; + x52_128 -> x54_128 ; + x53_128 -> x54_128 ; + x17 -> x55_128 ; + x48 -> x55_128 ; + x54_128 -> x56_128 ; + x55_128 -> x56_128 ; + x17 -> x57_128 ; + x45 -> x57_128 ; + x23_128 -> x58_128 ; + x57_128 -> x58_128 ; + x18 -> x59_128 ; + x47 -> x59_128 ; + x58_128 -> x60_128 ; + x59_128 -> x60_128 ; + x19 -> x61_128 ; + x48 -> x61_128 ; + x60_128 -> x62_128 ; + x61_128 -> x62_128 ; + x19 -> x63_128 ; + x45 -> x63_128 ; + x28_128 -> x64_128 ; + x63_128 -> x64_128 ; + x18 -> x65_128 ; + x48 -> x65_128 ; + x64_128 -> x66_128 ; + x65_128 -> x66_128 ; + x18 -> x67_128 ; + x45 -> x67_128 ; + x35_128 -> x68_128 ; + x67_128 -> x68_128 ; + x56_128 -> x69 ; + x56_128 -> x70 ; + x62_128 -> x71_128 ; + x69 -> x71_128 ; + x71_128 -> x72 ; + x71_128 -> x73 ; + x66_128 -> x74_128 ; + x72 -> x74_128 ; + x74_128 -> x75 ; + x74_128 -> x76 ; + x68_128 -> x77_128 ; + x75 -> x77_128 ; + x77_128 -> x78 ; + x77_128 -> x79 ; + x44_128 -> x80_128 ; + x78 -> x80_128 ; + x80_128 -> x81 ; + x80_128 -> x82 ; + x81 -> x83 ; + x70 -> x84 ; + x83 -> x84 ; + x84 -> x85 ; + x84 -> x86 ; + x73 -> x87 ; + x85 -> x87 ; + x87 -> x88 ; + x87 -> x89 ; + x76 -> x90 ; + x88 -> x90 ; +} diff --git a/etc/compile-by-zinc/femulData0.png b/etc/compile-by-zinc/femulData0.png new file mode 100644 index 000000000..0cd951607 Binary files /dev/null and b/etc/compile-by-zinc/femulData0.png differ diff --git a/etc/compile-by-zinc/femulData0.svg b/etc/compile-by-zinc/femulData0.svg new file mode 100644 index 000000000..827da12e7 --- /dev/null +++ b/etc/compile-by-zinc/femulData0.svg @@ -0,0 +1,1339 @@ + + + + + + +G + + + +x90 + +x90 (r13) + + + +out + +out + + + +x90->out + + + + + +x75 + +x75 (r8) + + + +x77_128 + +x77_128 (r9:r14) + + + +x75->x77_128 + + + + + +x58_128 + +x58_128 (RSP:r13) + + + +x60_128 + +x60_128 (RSP:r13) + + + +x58_128->x60_128 + + + + + +x69 + +x69 (RBP) + + + +x71_128 + +x71_128 (RSP:r13) + + + +x69->x71_128 + + + + + +x68_128 + +x68_128 (r9:r14) + + + +x68_128->x77_128 + + + + + +x44_128 + +x44_128 (r12:r15) + + + +x80_128 + +x80_128 (r12:r15) + + + +x44_128->x80_128 + + + + + +x42_128 + +x42_128 (r12:r15) + + + +x42_128->x44_128 + + + + + +x40_128 + +x40_128 (r12:r15) + + + +x40_128->x42_128 + + + + + +x62_128 + +x62_128 (RSP:r13) + + + +x60_128->x62_128 + + + + + +x62_128->x71_128 + + + + + +x64_128 + +x64_128 (r8:r10) + + + +x66_128 + +x66_128 (r8:r10) + + + +x64_128->x66_128 + + + + + +x74_128 + +x74_128 (r8:r10) + + + +x66_128->x74_128 + + + + + +x29_128 + +x29_128 (r9:r14) + + + +x31_128 + +x31_128 (r9:r14) + + + +x29_128->x31_128 + + + + + +x28_128 + +x28_128 (r8:r10) + + + +x28_128->x64_128 + + + + + +x24_128 + +x24_128 (r8:r10) + + + +x26_128 + +x26_128 (r8:r10) + + + +x24_128->x26_128 + + + + + +x26_128->x28_128 + + + + + +x21_128 + +x21_128 (RSP:r13) + + + +x23_128 + +x23_128 (RSP:r13) + + + +x21_128->x23_128 + + + + + +x20_128 + +x20_128 (RBP:r11) + + + +x50_128 + +x50_128 (RBP:r11) + + + +x20_128->x50_128 + + + + + +x23_128->x58_128 + + + + + +x83 + +x83 (r12) + + + +x84 + +x84 (r11) + + + +x83->x84 + + + + + +x82 + +x82 (r15) + + + +x82->out + + + + + +x81 + +x81 (r12) + + + +x81->x83 + + + + + +x80_128->x82 + + + + + +x80_128->x81 + + + + + +x87 + +x87 (r12) + + + +x89 + +x89 (r12) + + + +x87->x89 + + + + + +x88 + +x88 (r13) + + + +x87->x88 + + + + + +x86 + +x86 (r11) + + + +x86->out + + + + + +x85 + +x85 (r12) + + + +x85->x87 + + + + + +x84->x86 + + + + + +x84->x85 + + + + + +x89->out + + + + + +x88->x90 + + + + + +x52_128 + +x52_128 (RBP:r11) + + + +x50_128->x52_128 + + + + + +x5 + +x5 (r12) + + + +x5->x29_128 + + + + + +x5->x24_128 + + + + + +x5->x21_128 + + + + + +x5->x20_128 + + + + + +x36_128 + +x36_128 (r12:r15) + + + +x5->x36_128 + + + + + +x54_128 + +x54_128 (RBP:r11) + + + +x56_128 + +x56_128 (RBP:r11) + + + +x54_128->x56_128 + + + + + +x33_128 + +x33_128 (r9:r14) + + + +x35_128 + +x35_128 (r9:r14) + + + +x33_128->x35_128 + + + + + +x56_128->x69 + + + + + +x70 + +x70 (r11) + + + +x56_128->x70 + + + + + +x31_128->x33_128 + + + + + +x38_128 + +x38_128 (r12:r15) + + + +x36_128->x38_128 + + + + + +x52_128->x54_128 + + + + + +x78 + +x78 (r9) + + + +x78->x80_128 + + + + + +x79 + +x79 (r14) + + + +x79->out + + + + + +x76 + +x76 (r10) + + + +x76->x90 + + + + + +x77_128->x78 + + + + + +x77_128->x79 + + + + + +x38_128->x40_128 + + + + + +x35_128->x68_128 + + + + + +x72 + +x72 (RSP) + + + +x72->x74_128 + + + + + +x73 + +x73 (r13) + + + +x73->x87 + + + + + +x70->x84 + + + + + +x71_128->x72 + + + + + +x71_128->x73 + + + + + +x18 + +x18 (r15) + + + +x18->x36_128 + + + + + +x51_128 + +x51_128 + + + +x18->x51_128 + + + + + +x59_128 + +x59_128 + + + +x18->x59_128 + + + + + +x65_128 + +x65_128 + + + +x18->x65_128 + + + + + +x67_128 + +x67_128 + + + +x18->x67_128 + + + + + +x74_128->x75 + + + + + +x74_128->x76 + + + + + +in + +in + + + +in->x5 + + + + + +in->x18 + + + + + +x10 + +x10 + + + +in->x10 + + + + + +x11 + +x11 + + + +in->x11 + + + + + +x9 + +x9 + + + +in->x9 + + + + + +x7 + +x7 + + + +in->x7 + + + + + +x19 + +x19 + + + +in->x19 + + + + + +x17 + +x17 + + + +in->x17 + + + + + +x15 + +x15 + + + +in->x15 + + + + + +x13 + +x13 + + + +in->x13 + + + + + +x37_128 + +x37_128 + + + +x10->x37_128 + + + + + +x45 + +x45 + + + +x10->x45 + + + + + +x30_128 + +x30_128 + + + +x11->x30_128 + + + + + +x39_128 + +x39_128 + + + +x11->x39_128 + + + + + +x48 + +x48 + + + +x11->x48 + + + + + +x25_128 + +x25_128 + + + +x9->x25_128 + + + + + +x34_128 + +x34_128 + + + +x9->x34_128 + + + + + +x43_128 + +x43_128 + + + +x9->x43_128 + + + + + +x47 + +x47 + + + +x9->x47 + + + + + +x22_128 + +x22_128 + + + +x7->x22_128 + + + + + +x27_128 + +x27_128 + + + +x7->x27_128 + + + + + +x32_128 + +x32_128 + + + +x7->x32_128 + + + + + +x41_128 + +x41_128 + + + +x7->x41_128 + + + + + +x46 + +x46 + + + +x7->x46 + + + + + +x19->x29_128 + + + + + +x19->x41_128 + + + + + +x53_128 + +x53_128 + + + +x19->x53_128 + + + + + +x61_128 + +x61_128 + + + +x19->x61_128 + + + + + +x63_128 + +x63_128 + + + +x19->x63_128 + + + + + +x17->x24_128 + + + + + +x17->x32_128 + + + + + +x17->x43_128 + + + + + +x55_128 + +x55_128 + + + +x17->x55_128 + + + + + +x57_128 + +x57_128 + + + +x17->x57_128 + + + + + +x15->x21_128 + + + + + +x15->x27_128 + + + + + +x15->x34_128 + + + + + +x15->x39_128 + + + + + +x49_128 + +x49_128 + + + +x15->x49_128 + + + + + +x13->x20_128 + + + + + +x13->x22_128 + + + + + +x13->x25_128 + + + + + +x13->x30_128 + + + + + +x13->x37_128 + + + + + +x22_128->x23_128 + + + + + +x25_128->x26_128 + + + + + +x27_128->x28_128 + + + + + +x30_128->x31_128 + + + + + +x32_128->x33_128 + + + + + +x34_128->x35_128 + + + + + +x37_128->x38_128 + + + + + +x39_128->x40_128 + + + + + +x41_128->x42_128 + + + + + +x43_128->x44_128 + + + + + +x45->x49_128 + + + + + +x45->x57_128 + + + + + +x45->x63_128 + + + + + +x45->x67_128 + + + + + +x46->x51_128 + + + + + +x47->x53_128 + + + + + +x47->x59_128 + + + + + +x48->x55_128 + + + + + +x48->x61_128 + + + + + +x48->x65_128 + + + + + +x49_128->x50_128 + + + + + +x51_128->x52_128 + + + + + +x53_128->x54_128 + + + + + +x55_128->x56_128 + + + + + +x57_128->x58_128 + + + + + +x59_128->x60_128 + + + + + +x61_128->x62_128 + + + + + +x63_128->x64_128 + + + + + +x65_128->x66_128 + + + + + +x67_128->x68_128 + + + + + diff --git a/etc/compile-by-zinc/femulData0_1.png b/etc/compile-by-zinc/femulData0_1.png new file mode 100644 index 000000000..2012013ee Binary files /dev/null and b/etc/compile-by-zinc/femulData0_1.png differ diff --git a/etc/compile-by-zinc/femulData0_1.svg b/etc/compile-by-zinc/femulData0_1.svg new file mode 100644 index 000000000..469b4eab8 --- /dev/null +++ b/etc/compile-by-zinc/femulData0_1.svg @@ -0,0 +1,1118 @@ + + + + + + +G + + +in + +in + + +x10 + +x10 + + +in->x10 + + + + +x11 + +x11 + + +in->x11 + + + + +x9 + +x9 + + +in->x9 + + + + +x7 + +x7 + + +in->x7 + + + + +x5 + +x5 + + +in->x5 + + + + +x18 + +x18 + + +in->x18 + + + + +x19 + +x19 + + +in->x19 + + + + +x17 + +x17 + + +in->x17 + + + + +x15 + +x15 + + +in->x15 + + + + +x13 + +x13 + + +in->x13 + + + + +x37 + +x37 + + +x10->x37 + + + + +x45 + +x45 + + +x10->x45 + + + + +x30 + +x30 + + +x11->x30 + + + + +x39 + +x39 + + +x11->x39 + + + + +x48 + +x48 + + +x11->x48 + + + + +x25 + +x25 + + +x9->x25 + + + + +x34 + +x34 + + +x9->x34 + + + + +x43 + +x43 + + +x9->x43 + + + + +x47 + +x47 + + +x9->x47 + + + + +x22 + +x22 + + +x7->x22 + + + + +x27 + +x27 + + +x7->x27 + + + + +x32 + +x32 + + +x7->x32 + + + + +x41 + +x41 + + +x7->x41 + + + + +x46 + +x46 + + +x7->x46 + + + + +x20 + +x20 + + +x5->x20 + + + + +x21 + +x21 + + +x5->x21 + + + + +x24 + +x24 + + +x5->x24 + + + + +x29 + +x29 + + +x5->x29 + + + + +x36 + +x36 + + +x5->x36 + + + + +x18->x36 + + + + +x51 + +x51 + + +x18->x51 + + + + +x59 + +x59 + + +x18->x59 + + + + +x65 + +x65 + + +x18->x65 + + + + +x67 + +x67 + + +x18->x67 + + + + +x19->x29 + + + + +x19->x41 + + + + +x53 + +x53 + + +x19->x53 + + + + +x61 + +x61 + + +x19->x61 + + + + +x63 + +x63 + + +x19->x63 + + + + +x17->x24 + + + + +x17->x32 + + + + +x17->x43 + + + + +x55 + +x55 + + +x17->x55 + + + + +x57 + +x57 + + +x17->x57 + + + + +x15->x21 + + + + +x15->x27 + + + + +x15->x34 + + + + +x15->x39 + + + + +x49 + +x49 + + +x15->x49 + + + + +x13->x20 + + + + +x13->x22 + + + + +x13->x25 + + + + +x13->x30 + + + + +x13->x37 + + + + +x82 + +x82 (r12) + + +out + +out + + +x82->out + + + + +x79 + +x79 + + +x79->out + + + + +x90 + +x90 (r15) + + +x90->out + + + + +x89 + +x89 (r14) + + +x89->out + + + + +x86 + +x86 (r13) + + +x86->out + + + + +x50 + +x50 + + +x20->x50 + + + + +x23 + +x23 + + +x21->x23 + + + + +x22->x23 + + + + +x58 + +x58 + + +x23->x58 + + + + +x26 + +x26 + + +x24->x26 + + + + +x25->x26 + + + + +x28 + +x28 + + +x26->x28 + + + + +x27->x28 + + + + +x64 + +x64 + + +x28->x64 + + + + +x31 + +x31 + + +x29->x31 + + + + +x30->x31 + + + + +x33 + +x33 + + +x31->x33 + + + + +x32->x33 + + + + +x35 + +x35 + + +x33->x35 + + + + +x34->x35 + + + + +x68 + +x68 + + +x35->x68 + + + + +x38 + +x38 + + +x36->x38 + + + + +x37->x38 + + + + +x40 + +x40 + + +x38->x40 + + + + +x39->x40 + + + + +x42 + +x42 + + +x40->x42 + + + + +x41->x42 + + + + +x44 + +x44 + + +x42->x44 + + + + +x43->x44 + + + + +x80 + +x80 + + +x44->x80 + + + + +x45->x49 + + + + +x45->x57 + + + + +x45->x63 + + + + +x45->x67 + + + + +x46->x51 + + + + +x47->x53 + + + + +x47->x59 + + + + +x48->x55 + + + + +x48->x61 + + + + +x48->x65 + + + + +x49->x50 + + + + +x52 + +x52 + + +x50->x52 + + + + +x51->x52 + + + + +x54 + +x54 + + +x52->x54 + + + + +x53->x54 + + + + +x56 + +x56 + + +x54->x56 + + + + +x55->x56 + + + + +x69 + +x69 + + +x56->x69 + + + + +x70 + +x70 + + +x56->x70 + + + + +x57->x58 + + + + +x60 + +x60 + + +x58->x60 + + + + +x59->x60 + + + + +x62 + +x62 + + +x60->x62 + + + + +x61->x62 + + + + +x71 + +x71 + + +x62->x71 + + + + +x63->x64 + + + + +x66 + +x66 + + +x64->x66 + + + + +x65->x66 + + + + +x74 + +x74 + + +x66->x74 + + + + +x67->x68 + + + + +x77 + +x77 + + +x68->x77 + + + + +x69->x71 + + + + +x84 + +x84 + + +x70->x84 + + + + +x72 + +x72 + + +x71->x72 + + + + +x73 + +x73 + + +x71->x73 + + + + +x72->x74 + + + + +x87 + +x87 (r14) + + +x73->x87 + + + + +x75 + +x75 + + +x74->x75 + + + + +x76 + +x76 (r11) + + +x74->x76 + + + + +x75->x77 + + + + +x76->x90 + + + + +x77->x79 + + + + +x78 + +x78 + + +x77->x78 + + + + +x78->x80 + + + + +x80->x82 + + + + +x81 + +x81 + + +x80->x81 + + + + +x83 + +x83 + + +x81->x83 + + + + +x83->x84 + + + + +x84->x86 + + + + +x85 + +x85 + + +x84->x85 + + + + +x85->x87 + + + + +x87->x89 + + + + +x88 + +x88 (r15) + + +x87->x88 + + + + +x88->x90 + + + + + diff --git a/etc/compile-by-zinc/femulDisplayReg_0.mzn b/etc/compile-by-zinc/femulDisplayReg_0.mzn new file mode 100644 index 000000000..dc5cb140e --- /dev/null +++ b/etc/compile-by-zinc/femulDisplayReg_0.mzn @@ -0,0 +1,145 @@ +include "alldifferent.mzn"; +include "cumulative.mzn"; +%uint128_t x20 = x5 * x13; +%uint128_t x21 = x5 * x15; +%uint128_t x22 = x7 * x13; +%uint128_t x23 = x21 + x22; +%uint128_t x24 = x5 * x17; +%uint128_t x25 = x9 * x13; +%uint128_t x26 = x24 + x25; +%uint128_t x27 = x7 * x15; +%uint128_t x28 = x26 + x27; +%uint128_t x29 = x5 * x19; +%uint128_t x30 = x11 * x13; +%uint128_t x31 = x29 + x30; +%uint128_t x32 = x7 * x17; +%uint128_t x33 = x31 + x32; +%uint128_t x34 = x9 * x15; +%uint128_t x35 = x33 + x34; +%uint128_t x36 = x5 * x18; +%uint128_t x37 = x10 * x13; +%uint128_t x38 = x36 + x37; +%uint128_t x39 = x11 * x15; +%uint128_t x40 = x38 + x39; +%uint128_t x41 = x7 * x19; +%uint128_t x42 = x40 + x41; +%uint128_t x43 = x9 * x17; +%uint128_t x44 = x42 + x43; +%uint64_t x45 = x10 * 0x13; +%uint64_t x46 = x7 * 0x13; +%uint64_t x47 = x9 * 0x13; +%uint64_t x48 = x11 * 0x13; +%uint128_t x49 = x45 * x15; +set of int: INSTRUCTIONS = 1..40; +INSTRUCTIONS: x10 = 1; INSTRUCTIONS: x11 = 2; INSTRUCTIONS: x9 = 3; INSTRUCTIONS: x7 = 4; INSTRUCTIONS: x5 = 5; INSTRUCTIONS: x18 = 6; INSTRUCTIONS: x19 = 7; INSTRUCTIONS: x17 = 8; INSTRUCTIONS: x15 = 9; INSTRUCTIONS: x13 = 10; INSTRUCTIONS: x20 = 11; INSTRUCTIONS: x21 = 12; INSTRUCTIONS: x22 = 13; INSTRUCTIONS: x23 = 14; INSTRUCTIONS: x24 = 15; INSTRUCTIONS: x25 = 16; INSTRUCTIONS: x26 = 17; INSTRUCTIONS: x27 = 18; INSTRUCTIONS: x28 = 19; INSTRUCTIONS: x29 = 20; INSTRUCTIONS: x30 = 21; INSTRUCTIONS: x31 = 22; INSTRUCTIONS: x32 = 23; INSTRUCTIONS: x33 = 24; INSTRUCTIONS: x34 = 25; INSTRUCTIONS: x35 = 26; INSTRUCTIONS: x36 = 27; INSTRUCTIONS: x37 = 28; INSTRUCTIONS: x38 = 29; INSTRUCTIONS: x39 = 30; INSTRUCTIONS: x40 = 31; INSTRUCTIONS: x41 = 32; INSTRUCTIONS: x42 = 33; INSTRUCTIONS: x43 = 34; INSTRUCTIONS: x44 = 35; INSTRUCTIONS: x45 = 36; INSTRUCTIONS: x46 = 37; INSTRUCTIONS: x47 = 38; INSTRUCTIONS: x48 = 39; INSTRUCTIONS: x49 = 40; array[INSTRUCTIONS] of string: INSTRUCTIONS_NAMES = ["x10", "x11", "x9", "x7", "x5", "x18", "x19", "x17", "x15", "x13", "x20", "x21", "x22", "x23", "x24", "x25", "x26", "x27", "x28", "x29", "x30", "x31", "x32", "x33", "x34", "x35", "x36", "x37", "x38", "x39", "x40", "x41", "x42", "x43", "x44", "x45", "x46", "x47", "x48", "x49"]; + +int: MAX_LOC = 144; + +set of int: LOCATIONS = 1..MAX_LOC; +array[INSTRUCTIONS] of var LOCATIONS: output_locations; +array[INSTRUCTIONS] of var LOCATIONS: live_duration; +array[INSTRUCTIONS] of int: output_register_count = [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 2]; +var LOCATIONS: RET_loc; +constraint cumulative(output_locations, live_duration, output_register_count, 16); + + +constraint alldifferent(output_locations); + +constraint output_locations[x45] + live_duration[x45] == max([output_locations[x49]]); +constraint output_locations[x43] + live_duration[x43] == max([output_locations[x44]]); +constraint output_locations[x42] + live_duration[x42] == max([output_locations[x44]]); +constraint output_locations[x41] + live_duration[x41] == max([output_locations[x42]]); +constraint output_locations[x40] + live_duration[x40] == max([output_locations[x42]]); +constraint output_locations[x29] + live_duration[x29] == max([output_locations[x31]]); +constraint output_locations[x25] + live_duration[x25] == max([output_locations[x26]]); +constraint output_locations[x24] + live_duration[x24] == max([output_locations[x26]]); +constraint output_locations[x27] + live_duration[x27] == max([output_locations[x28]]); +constraint output_locations[x26] + live_duration[x26] == max([output_locations[x28]]); +constraint output_locations[x21] + live_duration[x21] == max([output_locations[x23]]); +constraint output_locations[x22] + live_duration[x22] == max([output_locations[x23]]); +constraint output_locations[x9] + live_duration[x9] == max([output_locations[x25], output_locations[x34], output_locations[x43], output_locations[x47]]); +constraint output_locations[x7] + live_duration[x7] == max([output_locations[x22], output_locations[x27], output_locations[x32], output_locations[x41], output_locations[x46]]); +constraint output_locations[x5] + live_duration[x5] == max([output_locations[x20], output_locations[x21], output_locations[x24], output_locations[x29], output_locations[x36]]); +constraint output_locations[x32] + live_duration[x32] == max([output_locations[x33]]); +constraint output_locations[x33] + live_duration[x33] == max([output_locations[x35]]); +constraint output_locations[x30] + live_duration[x30] == max([output_locations[x31]]); +constraint output_locations[x31] + live_duration[x31] == max([output_locations[x33]]); +constraint output_locations[x36] + live_duration[x36] == max([output_locations[x38]]); +constraint output_locations[x37] + live_duration[x37] == max([output_locations[x38]]); +constraint output_locations[x34] + live_duration[x34] == max([output_locations[x35]]); +constraint output_locations[x38] + live_duration[x38] == max([output_locations[x40]]); +constraint output_locations[x39] + live_duration[x39] == max([output_locations[x40]]); +constraint output_locations[x18] + live_duration[x18] == max([output_locations[x36]]); +constraint output_locations[x19] + live_duration[x19] == max([output_locations[x29], output_locations[x41]]); +constraint output_locations[x10] + live_duration[x10] == max([output_locations[x37], output_locations[x45]]); +constraint output_locations[x11] + live_duration[x11] == max([output_locations[x30], output_locations[x39], output_locations[x48]]); +constraint output_locations[x13] + live_duration[x13] == max([output_locations[x20], output_locations[x22], output_locations[x25], output_locations[x30], output_locations[x37]]); +constraint output_locations[x15] + live_duration[x15] == max([output_locations[x21], output_locations[x27], output_locations[x34], output_locations[x39], output_locations[x49]]); +constraint output_locations[x17] + live_duration[x17] == max([output_locations[x24], output_locations[x32], output_locations[x43]]); + + +constraint output_locations[x5] + 1 <= output_locations[x20]; +constraint output_locations[x13] + 1 <= output_locations[x20]; +constraint output_locations[x5] + 1 <= output_locations[x21]; +constraint output_locations[x15] + 1 <= output_locations[x21]; +constraint output_locations[x7] + 1 <= output_locations[x22]; +constraint output_locations[x13] + 1 <= output_locations[x22]; +constraint output_locations[x21] + 1 <= output_locations[x23]; +constraint output_locations[x22] + 1 <= output_locations[x23]; +constraint output_locations[x5] + 1 <= output_locations[x24]; +constraint output_locations[x17] + 1 <= output_locations[x24]; +constraint output_locations[x9] + 1 <= output_locations[x25]; +constraint output_locations[x13] + 1 <= output_locations[x25]; +constraint output_locations[x24] + 1 <= output_locations[x26]; +constraint output_locations[x25] + 1 <= output_locations[x26]; +constraint output_locations[x7] + 1 <= output_locations[x27]; +constraint output_locations[x15] + 1 <= output_locations[x27]; +constraint output_locations[x26] + 1 <= output_locations[x28]; +constraint output_locations[x27] + 1 <= output_locations[x28]; +constraint output_locations[x5] + 1 <= output_locations[x29]; +constraint output_locations[x19] + 1 <= output_locations[x29]; +constraint output_locations[x11] + 1 <= output_locations[x30]; +constraint output_locations[x13] + 1 <= output_locations[x30]; +constraint output_locations[x29] + 1 <= output_locations[x31]; +constraint output_locations[x30] + 1 <= output_locations[x31]; +constraint output_locations[x7] + 1 <= output_locations[x32]; +constraint output_locations[x17] + 1 <= output_locations[x32]; +constraint output_locations[x31] + 1 <= output_locations[x33]; +constraint output_locations[x32] + 1 <= output_locations[x33]; +constraint output_locations[x9] + 1 <= output_locations[x34]; +constraint output_locations[x15] + 1 <= output_locations[x34]; +constraint output_locations[x33] + 1 <= output_locations[x35]; +constraint output_locations[x34] + 1 <= output_locations[x35]; +constraint output_locations[x5] + 1 <= output_locations[x36]; +constraint output_locations[x18] + 1 <= output_locations[x36]; +constraint output_locations[x10] + 1 <= output_locations[x37]; +constraint output_locations[x13] + 1 <= output_locations[x37]; +constraint output_locations[x36] + 1 <= output_locations[x38]; +constraint output_locations[x37] + 1 <= output_locations[x38]; +constraint output_locations[x11] + 1 <= output_locations[x39]; +constraint output_locations[x15] + 1 <= output_locations[x39]; +constraint output_locations[x38] + 1 <= output_locations[x40]; +constraint output_locations[x39] + 1 <= output_locations[x40]; +constraint output_locations[x7] + 1 <= output_locations[x41]; +constraint output_locations[x19] + 1 <= output_locations[x41]; +constraint output_locations[x40] + 1 <= output_locations[x42]; +constraint output_locations[x41] + 1 <= output_locations[x42]; +constraint output_locations[x9] + 1 <= output_locations[x43]; +constraint output_locations[x17] + 1 <= output_locations[x43]; +constraint output_locations[x42] + 1 <= output_locations[x44]; +constraint output_locations[x43] + 1 <= output_locations[x44]; +constraint output_locations[x10] + 1 <= output_locations[x45]; +constraint output_locations[x7] + 1 <= output_locations[x46]; +constraint output_locations[x9] + 1 <= output_locations[x47]; +constraint output_locations[x11] + 1 <= output_locations[x48]; +constraint output_locations[x45] + 1 <= output_locations[x49]; +constraint output_locations[x15] + 1 <= output_locations[x49]; + +constraint max([ output_locations[i] + 1 | i in INSTRUCTIONS ]) <= RET_loc; + + +solve minimize RET_loc; + +output [ "(" ++ show(INSTRUCTIONS_NAMES[i]) ++ ", " ++ show(output_locations[i]) ++ ", " ++ show(live_duration[i]) ++ ") ,\n" + | i in INSTRUCTIONS ]; +output [ "RET_loc: " ++ show(RET_loc) ]; diff --git a/etc/compile-by-zinc/femulDisplayReg_1.mzn b/etc/compile-by-zinc/femulDisplayReg_1.mzn new file mode 100644 index 000000000..222156642 --- /dev/null +++ b/etc/compile-by-zinc/femulDisplayReg_1.mzn @@ -0,0 +1,147 @@ +include "alldifferent.mzn"; +include "cumulative.mzn"; +%uint128_t x50 = x20 + x49; +%uint128_t x51 = x46 * x18; +%uint128_t x52 = x50 + x51; +%uint128_t x53 = x47 * x19; +%uint128_t x54 = x52 + x53; +%uint128_t x55 = x48 * x17; +%uint128_t x56 = x54 + x55; +%uint128_t x57 = x45 * x17; +%uint128_t x58 = x23 + x57; +%uint128_t x59 = x47 * x18; +%uint128_t x60 = x58 + x59; +%uint128_t x61 = x48 * x19; +%uint128_t x62 = x60 + x61; +%uint128_t x63 = x45 * x19; +%uint128_t x64 = x28 + x63; +%uint128_t x65 = x48 * x18; +%uint128_t x66 = x64 + x65; +%uint128_t x67 = x45 * x18; +%uint128_t x68 = x35 + x67; +%uint64_t x69 = x56 >> 0x33; +%uint64_t x70 = x56 & 0x7ffffffffffff; +%uint128_t x71 = x69 + x62; +%uint64_t x72 = x71 >> 0x33; +%uint64_t x73 = x71 & 0x7ffffffffffff; +%uint128_t x74 = x72 + x66; +%uint64_t x75 = x74 >> 0x33; +%uint64_t x76 = x74 & 0x7ffffffffffff; +%uint128_t x77 = x75 + x68; +%uint64_t x78 = x77 >> 0x33; +%uint64_t x79 = x77 & 0x7ffffffffffff; +set of int: INSTRUCTIONS = 1..40; +INSTRUCTIONS: x10 = 1; INSTRUCTIONS: x11 = 2; INSTRUCTIONS: x9 = 3; INSTRUCTIONS: x7 = 4; INSTRUCTIONS: x5 = 5; INSTRUCTIONS: x18 = 6; INSTRUCTIONS: x19 = 7; INSTRUCTIONS: x17 = 8; INSTRUCTIONS: x15 = 9; INSTRUCTIONS: x13 = 10; INSTRUCTIONS: x50 = 11; INSTRUCTIONS: x51 = 12; INSTRUCTIONS: x52 = 13; INSTRUCTIONS: x53 = 14; INSTRUCTIONS: x54 = 15; INSTRUCTIONS: x55 = 16; INSTRUCTIONS: x56 = 17; INSTRUCTIONS: x57 = 18; INSTRUCTIONS: x58 = 19; INSTRUCTIONS: x59 = 20; INSTRUCTIONS: x60 = 21; INSTRUCTIONS: x61 = 22; INSTRUCTIONS: x62 = 23; INSTRUCTIONS: x63 = 24; INSTRUCTIONS: x64 = 25; INSTRUCTIONS: x65 = 26; INSTRUCTIONS: x66 = 27; INSTRUCTIONS: x67 = 28; INSTRUCTIONS: x68 = 29; INSTRUCTIONS: x69 = 30; INSTRUCTIONS: x70 = 31; INSTRUCTIONS: x71 = 32; INSTRUCTIONS: x72 = 33; INSTRUCTIONS: x73 = 34; INSTRUCTIONS: x74 = 35; INSTRUCTIONS: x75 = 36; INSTRUCTIONS: x76 = 37; INSTRUCTIONS: x77 = 38; INSTRUCTIONS: x78 = 39; INSTRUCTIONS: x79 = 40; array[INSTRUCTIONS] of string: INSTRUCTIONS_NAMES = ["x10", "x11", "x9", "x7", "x5", "x18", "x19", "x17", "x15", "x13", "x50", "x51", "x52", "x53", "x54", "x55", "x56", "x57", "x58", "x59", "x60", "x61", "x62", "x63", "x64", "x65", "x66", "x67", "x68", "x69", "x70", "x71", "x72", "x73", "x74", "x75", "x76", "x77", "x78", "x79"]; + +int: MAX_LOC = 144; + +set of int: LOCATIONS = 1..MAX_LOC; +array[INSTRUCTIONS] of var LOCATIONS: output_locations; +array[INSTRUCTIONS] of var LOCATIONS: live_duration; +array[INSTRUCTIONS] of int: output_register_count = [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 2, 1, 1, 2, 1, 1, 2, 1, 1]; +var LOCATIONS: RET_loc; +constraint cumulative(output_locations, live_duration, output_register_count, 16); + + +constraint alldifferent(output_locations); + +constraint output_locations[x75] + live_duration[x75] == max([output_locations[x77]]); +constraint output_locations[x72] + live_duration[x72] == max([output_locations[x74]]); +constraint output_locations[x67] + live_duration[x67] == max([output_locations[x68]]); +constraint output_locations[x66] + live_duration[x66] == max([output_locations[x74]]); +constraint output_locations[x47] + live_duration[x47] == max([output_locations[x53], output_locations[x59]]); +constraint output_locations[x46] + live_duration[x46] == max([output_locations[x51]]); +constraint output_locations[x45] + live_duration[x45] == max([output_locations[x57], output_locations[x63], output_locations[x67]]); +constraint output_locations[x61] + live_duration[x61] == max([output_locations[x62]]); +constraint output_locations[x60] + live_duration[x60] == max([output_locations[x62]]); +constraint output_locations[x63] + live_duration[x63] == max([output_locations[x64]]); +constraint output_locations[x62] + live_duration[x62] == max([output_locations[x71]]); +constraint output_locations[x65] + live_duration[x65] == max([output_locations[x66]]); +constraint output_locations[x64] + live_duration[x64] == max([output_locations[x66]]); +constraint output_locations[x49] + live_duration[x49] == max([output_locations[x50]]); +constraint output_locations[x48] + live_duration[x48] == max([output_locations[x55], output_locations[x61], output_locations[x65]]); +constraint output_locations[x28] + live_duration[x28] == max([output_locations[x64]]); +constraint output_locations[x20] + live_duration[x20] == max([output_locations[x50]]); +constraint output_locations[x23] + live_duration[x23] == max([output_locations[x58]]); +constraint output_locations[x69] + live_duration[x69] == max([output_locations[x71]]); +constraint output_locations[x68] + live_duration[x68] == max([output_locations[x77]]); +constraint output_locations[x54] + live_duration[x54] == max([output_locations[x56]]); +constraint output_locations[x55] + live_duration[x55] == max([output_locations[x56]]); +constraint output_locations[x56] + live_duration[x56] == max([output_locations[x69], output_locations[x70]]); +constraint output_locations[x57] + live_duration[x57] == max([output_locations[x58]]); +constraint output_locations[x50] + live_duration[x50] == max([output_locations[x52]]); +constraint output_locations[x51] + live_duration[x51] == max([output_locations[x52]]); +constraint output_locations[x52] + live_duration[x52] == max([output_locations[x54]]); +constraint output_locations[x53] + live_duration[x53] == max([output_locations[x54]]); +constraint output_locations[x77] + live_duration[x77] == max([output_locations[x78], output_locations[x79]]); +constraint output_locations[x74] + live_duration[x74] == max([output_locations[x75], output_locations[x76]]); +constraint output_locations[x35] + live_duration[x35] == max([output_locations[x68]]); +constraint output_locations[x58] + live_duration[x58] == max([output_locations[x60]]); +constraint output_locations[x59] + live_duration[x59] == max([output_locations[x60]]); +constraint output_locations[x71] + live_duration[x71] == max([output_locations[x72], output_locations[x73]]); +constraint output_locations[x18] + live_duration[x18] == max([output_locations[x51], output_locations[x59], output_locations[x65], output_locations[x67]]); +constraint output_locations[x19] + live_duration[x19] == max([output_locations[x53], output_locations[x61], output_locations[x63]]); +constraint output_locations[x17] + live_duration[x17] == max([output_locations[x55], output_locations[x57]]); + + +constraint output_locations[x20] + 1 <= output_locations[x50]; +constraint output_locations[x49] + 1 <= output_locations[x50]; +constraint output_locations[x46] + 1 <= output_locations[x51]; +constraint output_locations[x18] + 1 <= output_locations[x51]; +constraint output_locations[x50] + 1 <= output_locations[x52]; +constraint output_locations[x51] + 1 <= output_locations[x52]; +constraint output_locations[x47] + 1 <= output_locations[x53]; +constraint output_locations[x19] + 1 <= output_locations[x53]; +constraint output_locations[x52] + 1 <= output_locations[x54]; +constraint output_locations[x53] + 1 <= output_locations[x54]; +constraint output_locations[x48] + 1 <= output_locations[x55]; +constraint output_locations[x17] + 1 <= output_locations[x55]; +constraint output_locations[x54] + 1 <= output_locations[x56]; +constraint output_locations[x55] + 1 <= output_locations[x56]; +constraint output_locations[x45] + 1 <= output_locations[x57]; +constraint output_locations[x17] + 1 <= output_locations[x57]; +constraint output_locations[x23] + 1 <= output_locations[x58]; +constraint output_locations[x57] + 1 <= output_locations[x58]; +constraint output_locations[x47] + 1 <= output_locations[x59]; +constraint output_locations[x18] + 1 <= output_locations[x59]; +constraint output_locations[x58] + 1 <= output_locations[x60]; +constraint output_locations[x59] + 1 <= output_locations[x60]; +constraint output_locations[x48] + 1 <= output_locations[x61]; +constraint output_locations[x19] + 1 <= output_locations[x61]; +constraint output_locations[x60] + 1 <= output_locations[x62]; +constraint output_locations[x61] + 1 <= output_locations[x62]; +constraint output_locations[x45] + 1 <= output_locations[x63]; +constraint output_locations[x19] + 1 <= output_locations[x63]; +constraint output_locations[x28] + 1 <= output_locations[x64]; +constraint output_locations[x63] + 1 <= output_locations[x64]; +constraint output_locations[x48] + 1 <= output_locations[x65]; +constraint output_locations[x18] + 1 <= output_locations[x65]; +constraint output_locations[x64] + 1 <= output_locations[x66]; +constraint output_locations[x65] + 1 <= output_locations[x66]; +constraint output_locations[x45] + 1 <= output_locations[x67]; +constraint output_locations[x18] + 1 <= output_locations[x67]; +constraint output_locations[x35] + 1 <= output_locations[x68]; +constraint output_locations[x67] + 1 <= output_locations[x68]; +constraint output_locations[x56] + 1 <= output_locations[x69]; +constraint output_locations[x56] + 1 <= output_locations[x70]; +constraint output_locations[x69] + 1 <= output_locations[x71]; +constraint output_locations[x62] + 1 <= output_locations[x71]; +constraint output_locations[x71] + 1 <= output_locations[x72]; +constraint output_locations[x71] + 1 <= output_locations[x73]; +constraint output_locations[x72] + 1 <= output_locations[x74]; +constraint output_locations[x66] + 1 <= output_locations[x74]; +constraint output_locations[x74] + 1 <= output_locations[x75]; +constraint output_locations[x74] + 1 <= output_locations[x76]; +constraint output_locations[x75] + 1 <= output_locations[x77]; +constraint output_locations[x68] + 1 <= output_locations[x77]; +constraint output_locations[x77] + 1 <= output_locations[x78]; +constraint output_locations[x77] + 1 <= output_locations[x79]; + +constraint max([ output_locations[i] + 1 | i in INSTRUCTIONS ]) <= RET_loc; + + +solve minimize RET_loc; + +output [ "(" ++ show(INSTRUCTIONS_NAMES[i]) ++ ", " ++ show(output_locations[i]) ++ ", " ++ show(live_duration[i]) ++ ") ,\n" + | i in INSTRUCTIONS ]; +output [ "RET_loc: " ++ show(RET_loc) ]; diff --git a/etc/compile-by-zinc/femulDisplayReg_2.mzn b/etc/compile-by-zinc/femulDisplayReg_2.mzn new file mode 100644 index 000000000..0d2bd382f --- /dev/null +++ b/etc/compile-by-zinc/femulDisplayReg_2.mzn @@ -0,0 +1,66 @@ +include "alldifferent.mzn"; +include "cumulative.mzn"; +%uint128_t x80 = x78 + x44; +%uint64_t x81 = x80 >> 0x33; +%uint64_t x82 = x80 & 0x7ffffffffffff; +%uint64_t x83 = 0x13 * x81; +%uint64_t x84 = x70 + x83; +%uint64_t x85 = x84 >> 0x33; +%uint64_t x86 = x84 & 0x7ffffffffffff; +%uint64_t x87 = x85 + x73; +%uint64_t x88 = x87 >> 0x33; +%uint64_t x89 = x87 & 0x7ffffffffffff; +%uint64_t x90 = x88 + x76; +set of int: INSTRUCTIONS = 1..21; +INSTRUCTIONS: x10 = 1; INSTRUCTIONS: x11 = 2; INSTRUCTIONS: x9 = 3; INSTRUCTIONS: x7 = 4; INSTRUCTIONS: x5 = 5; INSTRUCTIONS: x18 = 6; INSTRUCTIONS: x19 = 7; INSTRUCTIONS: x17 = 8; INSTRUCTIONS: x15 = 9; INSTRUCTIONS: x13 = 10; INSTRUCTIONS: x80 = 11; INSTRUCTIONS: x81 = 12; INSTRUCTIONS: x82 = 13; INSTRUCTIONS: x83 = 14; INSTRUCTIONS: x84 = 15; INSTRUCTIONS: x85 = 16; INSTRUCTIONS: x86 = 17; INSTRUCTIONS: x87 = 18; INSTRUCTIONS: x88 = 19; INSTRUCTIONS: x89 = 20; INSTRUCTIONS: x90 = 21; array[INSTRUCTIONS] of string: INSTRUCTIONS_NAMES = ["x10", "x11", "x9", "x7", "x5", "x18", "x19", "x17", "x15", "x13", "x80", "x81", "x82", "x83", "x84", "x85", "x86", "x87", "x88", "x89", "x90"]; + +int: MAX_LOC = 87; + +set of int: LOCATIONS = 1..MAX_LOC; +array[INSTRUCTIONS] of var LOCATIONS: output_locations; +array[INSTRUCTIONS] of var LOCATIONS: live_duration; +array[INSTRUCTIONS] of int: output_register_count = [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]; +var LOCATIONS: RET_loc; +constraint cumulative(output_locations, live_duration, output_register_count, 16); + + +constraint alldifferent(output_locations); + +constraint output_locations[x83] + live_duration[x83] == max([output_locations[x84]]); +constraint output_locations[x81] + live_duration[x81] == max([output_locations[x83]]); +constraint output_locations[x44] + live_duration[x44] == max([output_locations[x80]]); +constraint output_locations[x87] + live_duration[x87] == max([output_locations[x88], output_locations[x89]]); +constraint output_locations[x85] + live_duration[x85] == max([output_locations[x87]]); +constraint output_locations[x78] + live_duration[x78] == max([output_locations[x80]]); +constraint output_locations[x84] + live_duration[x84] == max([output_locations[x85], output_locations[x86]]); +constraint output_locations[x76] + live_duration[x76] == max([output_locations[x90]]); +constraint output_locations[x88] + live_duration[x88] == max([output_locations[x90]]); +constraint output_locations[x73] + live_duration[x73] == max([output_locations[x87]]); +constraint output_locations[x70] + live_duration[x70] == max([output_locations[x84]]); +constraint output_locations[x80] + live_duration[x80] == max([output_locations[x81], output_locations[x82]]); + + +constraint output_locations[x78] + 1 <= output_locations[x80]; +constraint output_locations[x44] + 1 <= output_locations[x80]; +constraint output_locations[x80] + 1 <= output_locations[x81]; +constraint output_locations[x80] + 1 <= output_locations[x82]; +constraint output_locations[x81] + 1 <= output_locations[x83]; +constraint output_locations[x70] + 1 <= output_locations[x84]; +constraint output_locations[x83] + 1 <= output_locations[x84]; +constraint output_locations[x84] + 1 <= output_locations[x85]; +constraint output_locations[x84] + 1 <= output_locations[x86]; +constraint output_locations[x85] + 1 <= output_locations[x87]; +constraint output_locations[x73] + 1 <= output_locations[x87]; +constraint output_locations[x87] + 1 <= output_locations[x88]; +constraint output_locations[x87] + 1 <= output_locations[x89]; +constraint output_locations[x88] + 1 <= output_locations[x90]; +constraint output_locations[x76] + 1 <= output_locations[x90]; + +constraint max([ output_locations[i] + 1 | i in INSTRUCTIONS ]) <= RET_loc; + + +solve minimize RET_loc; + +output [ "(" ++ show(INSTRUCTIONS_NAMES[i]) ++ ", " ++ show(output_locations[i]) ++ ", " ++ show(live_duration[i]) ++ ") ,\n" + | i in INSTRUCTIONS ]; +output [ "RET_loc: " ++ show(RET_loc) ]; diff --git a/etc/compile-by-zinc/femulDisplayReg_3.mzn b/etc/compile-by-zinc/femulDisplayReg_3.mzn new file mode 100644 index 000000000..0d2bd382f --- /dev/null +++ b/etc/compile-by-zinc/femulDisplayReg_3.mzn @@ -0,0 +1,66 @@ +include "alldifferent.mzn"; +include "cumulative.mzn"; +%uint128_t x80 = x78 + x44; +%uint64_t x81 = x80 >> 0x33; +%uint64_t x82 = x80 & 0x7ffffffffffff; +%uint64_t x83 = 0x13 * x81; +%uint64_t x84 = x70 + x83; +%uint64_t x85 = x84 >> 0x33; +%uint64_t x86 = x84 & 0x7ffffffffffff; +%uint64_t x87 = x85 + x73; +%uint64_t x88 = x87 >> 0x33; +%uint64_t x89 = x87 & 0x7ffffffffffff; +%uint64_t x90 = x88 + x76; +set of int: INSTRUCTIONS = 1..21; +INSTRUCTIONS: x10 = 1; INSTRUCTIONS: x11 = 2; INSTRUCTIONS: x9 = 3; INSTRUCTIONS: x7 = 4; INSTRUCTIONS: x5 = 5; INSTRUCTIONS: x18 = 6; INSTRUCTIONS: x19 = 7; INSTRUCTIONS: x17 = 8; INSTRUCTIONS: x15 = 9; INSTRUCTIONS: x13 = 10; INSTRUCTIONS: x80 = 11; INSTRUCTIONS: x81 = 12; INSTRUCTIONS: x82 = 13; INSTRUCTIONS: x83 = 14; INSTRUCTIONS: x84 = 15; INSTRUCTIONS: x85 = 16; INSTRUCTIONS: x86 = 17; INSTRUCTIONS: x87 = 18; INSTRUCTIONS: x88 = 19; INSTRUCTIONS: x89 = 20; INSTRUCTIONS: x90 = 21; array[INSTRUCTIONS] of string: INSTRUCTIONS_NAMES = ["x10", "x11", "x9", "x7", "x5", "x18", "x19", "x17", "x15", "x13", "x80", "x81", "x82", "x83", "x84", "x85", "x86", "x87", "x88", "x89", "x90"]; + +int: MAX_LOC = 87; + +set of int: LOCATIONS = 1..MAX_LOC; +array[INSTRUCTIONS] of var LOCATIONS: output_locations; +array[INSTRUCTIONS] of var LOCATIONS: live_duration; +array[INSTRUCTIONS] of int: output_register_count = [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]; +var LOCATIONS: RET_loc; +constraint cumulative(output_locations, live_duration, output_register_count, 16); + + +constraint alldifferent(output_locations); + +constraint output_locations[x83] + live_duration[x83] == max([output_locations[x84]]); +constraint output_locations[x81] + live_duration[x81] == max([output_locations[x83]]); +constraint output_locations[x44] + live_duration[x44] == max([output_locations[x80]]); +constraint output_locations[x87] + live_duration[x87] == max([output_locations[x88], output_locations[x89]]); +constraint output_locations[x85] + live_duration[x85] == max([output_locations[x87]]); +constraint output_locations[x78] + live_duration[x78] == max([output_locations[x80]]); +constraint output_locations[x84] + live_duration[x84] == max([output_locations[x85], output_locations[x86]]); +constraint output_locations[x76] + live_duration[x76] == max([output_locations[x90]]); +constraint output_locations[x88] + live_duration[x88] == max([output_locations[x90]]); +constraint output_locations[x73] + live_duration[x73] == max([output_locations[x87]]); +constraint output_locations[x70] + live_duration[x70] == max([output_locations[x84]]); +constraint output_locations[x80] + live_duration[x80] == max([output_locations[x81], output_locations[x82]]); + + +constraint output_locations[x78] + 1 <= output_locations[x80]; +constraint output_locations[x44] + 1 <= output_locations[x80]; +constraint output_locations[x80] + 1 <= output_locations[x81]; +constraint output_locations[x80] + 1 <= output_locations[x82]; +constraint output_locations[x81] + 1 <= output_locations[x83]; +constraint output_locations[x70] + 1 <= output_locations[x84]; +constraint output_locations[x83] + 1 <= output_locations[x84]; +constraint output_locations[x84] + 1 <= output_locations[x85]; +constraint output_locations[x84] + 1 <= output_locations[x86]; +constraint output_locations[x85] + 1 <= output_locations[x87]; +constraint output_locations[x73] + 1 <= output_locations[x87]; +constraint output_locations[x87] + 1 <= output_locations[x88]; +constraint output_locations[x87] + 1 <= output_locations[x89]; +constraint output_locations[x88] + 1 <= output_locations[x90]; +constraint output_locations[x76] + 1 <= output_locations[x90]; + +constraint max([ output_locations[i] + 1 | i in INSTRUCTIONS ]) <= RET_loc; + + +solve minimize RET_loc; + +output [ "(" ++ show(INSTRUCTIONS_NAMES[i]) ++ ", " ++ show(output_locations[i]) ++ ", " ++ show(live_duration[i]) ++ ") ,\n" + | i in INSTRUCTIONS ]; +output [ "RET_loc: " ++ show(RET_loc) ]; diff --git a/etc/compile-by-zinc/femulDisplay_0.mzn b/etc/compile-by-zinc/femulDisplay_0.mzn new file mode 100644 index 000000000..fda3425b9 --- /dev/null +++ b/etc/compile-by-zinc/femulDisplay_0.mzn @@ -0,0 +1,164 @@ +include "alldifferent.mzn"; +include "cumulative.mzn"; +%uint128_t x20 = x5 * x13; +%uint128_t x21 = x5 * x15; +%uint128_t x22 = x7 * x13; +%uint128_t x23 = x21 + x22; +%uint128_t x24 = x5 * x17; +%uint128_t x25 = x9 * x13; +%uint128_t x26 = x24 + x25; +%uint128_t x27 = x7 * x15; +%uint128_t x28 = x26 + x27; +%uint128_t x29 = x5 * x19; +%uint128_t x30 = x11 * x13; +%uint128_t x31 = x29 + x30; +%uint128_t x32 = x7 * x17; +%uint128_t x33 = x31 + x32; +%uint128_t x34 = x9 * x15; +%uint128_t x35 = x33 + x34; +%uint128_t x36 = x5 * x18; +%uint128_t x37 = x10 * x13; +%uint128_t x38 = x36 + x37; +%uint128_t x39 = x11 * x15; +%uint128_t x40 = x38 + x39; +%uint128_t x41 = x7 * x19; +%uint128_t x42 = x40 + x41; +%uint128_t x43 = x9 * x17; +%uint128_t x44 = x42 + x43; +%uint64_t x45 = x10 * 0x13; +%uint64_t x46 = x7 * 0x13; +%uint64_t x47 = x9 * 0x13; +%uint64_t x48 = x11 * 0x13; +%uint128_t x49 = x45 * x15; +%uint128_t x50 = x20 + x49; +%uint128_t x51 = x46 * x18; +%uint128_t x52 = x50 + x51; +%uint128_t x53 = x47 * x19; +%uint128_t x54 = x52 + x53; +%uint128_t x55 = x48 * x17; +%uint128_t x56 = x54 + x55; +%uint128_t x57 = x45 * x17; +%uint128_t x58 = x23 + x57; +%uint128_t x59 = x47 * x18; +%uint128_t x60 = x58 + x59; +%uint128_t x61 = x48 * x19; +%uint128_t x62 = x60 + x61; +%uint128_t x63 = x45 * x19; +%uint128_t x64 = x28 + x63; +%uint128_t x65 = x48 * x18; +%uint128_t x66 = x64 + x65; +%uint128_t x67 = x45 * x18; +%uint128_t x68 = x35 + x67; +%uint64_t x69 = x56 >> 0x33; +%uint64_t x70 = x56 & 0x7ffffffffffff; +%uint128_t x71 = x69 + x62; +%uint64_t x72 = x71 >> 0x33; +set of int: CORE = 1..3; +CORE: ADD_MUL = 1; CORE: MUL_CORE = 2; CORE: LEA_BW = 3; array[CORE] of string: CORE_NAMES = ["ADD_MUL", "MUL_CORE", "LEA_BW"]; + +set of int: INSTRUCTIONS = 1..53; +INSTRUCTIONS: x20 = 1; INSTRUCTIONS: x21 = 2; INSTRUCTIONS: x22 = 3; INSTRUCTIONS: x23 = 4; INSTRUCTIONS: x24 = 5; INSTRUCTIONS: x25 = 6; INSTRUCTIONS: x26 = 7; INSTRUCTIONS: x27 = 8; INSTRUCTIONS: x28 = 9; INSTRUCTIONS: x29 = 10; INSTRUCTIONS: x30 = 11; INSTRUCTIONS: x31 = 12; INSTRUCTIONS: x32 = 13; INSTRUCTIONS: x33 = 14; INSTRUCTIONS: x34 = 15; INSTRUCTIONS: x35 = 16; INSTRUCTIONS: x36 = 17; INSTRUCTIONS: x37 = 18; INSTRUCTIONS: x38 = 19; INSTRUCTIONS: x39 = 20; INSTRUCTIONS: x40 = 21; INSTRUCTIONS: x41 = 22; INSTRUCTIONS: x42 = 23; INSTRUCTIONS: x43 = 24; INSTRUCTIONS: x44 = 25; INSTRUCTIONS: x45 = 26; INSTRUCTIONS: x46 = 27; INSTRUCTIONS: x47 = 28; INSTRUCTIONS: x48 = 29; INSTRUCTIONS: x49 = 30; INSTRUCTIONS: x50 = 31; INSTRUCTIONS: x51 = 32; INSTRUCTIONS: x52 = 33; INSTRUCTIONS: x53 = 34; INSTRUCTIONS: x54 = 35; INSTRUCTIONS: x55 = 36; INSTRUCTIONS: x56 = 37; INSTRUCTIONS: x57 = 38; INSTRUCTIONS: x58 = 39; INSTRUCTIONS: x59 = 40; INSTRUCTIONS: x60 = 41; INSTRUCTIONS: x61 = 42; INSTRUCTIONS: x62 = 43; INSTRUCTIONS: x63 = 44; INSTRUCTIONS: x64 = 45; INSTRUCTIONS: x65 = 46; INSTRUCTIONS: x66 = 47; INSTRUCTIONS: x67 = 48; INSTRUCTIONS: x68 = 49; INSTRUCTIONS: x69 = 50; INSTRUCTIONS: x70 = 51; INSTRUCTIONS: x71 = 52; INSTRUCTIONS: x72 = 53; array[INSTRUCTIONS] of string: INSTRUCTIONS_NAMES = ["x20", "x21", "x22", "x23", "x24", "x25", "x26", "x27", "x28", "x29", "x30", "x31", "x32", "x33", "x34", "x35", "x36", "x37", "x38", "x39", "x40", "x41", "x42", "x43", "x44", "x45", "x46", "x47", "x48", "x49", "x50", "x51", "x52", "x53", "x54", "x55", "x56", "x57", "x58", "x59", "x60", "x61", "x62", "x63", "x64", "x65", "x66", "x67", "x68", "x69", "x70", "x71", "x72"]; + +set of int: OPS = 1..6; +OPS: SHL = 1; OPS: AND = 2; OPS: ADD = 3; OPS: MUL = 4; OPS: OR = 5; OPS: SHR = 6; array[OPS] of string: OPS_NAMES = ["SHL", "AND", "ADD", "MUL", "OR", "SHR"]; + +int: MAX_LOC = 183; + +set of int: LOCATIONS = 1..MAX_LOC; +array[INSTRUCTIONS] of var LOCATIONS: output_locations; +array[INSTRUCTIONS] of var int: output_data_latency; +array[INSTRUCTIONS] of var int: output_core_latency; +array[INSTRUCTIONS] of var CORE: output_cores; +array[INSTRUCTIONS] of OPS: input_ops = [MUL, MUL, MUL, ADD, MUL, MUL, ADD, MUL, ADD, MUL, MUL, ADD, MUL, ADD, MUL, ADD, MUL, MUL, ADD, MUL, ADD, MUL, ADD, MUL, ADD, MUL, MUL, MUL, MUL, MUL, ADD, MUL, ADD, MUL, ADD, MUL, ADD, MUL, ADD, MUL, ADD, MUL, ADD, MUL, ADD, MUL, ADD, MUL, ADD, SHL, AND, ADD, SHL]; +array[INSTRUCTIONS] of var int: output_ADD_MUL_core_latency; +array[INSTRUCTIONS] of var 0..1: output_ADD_MUL_core_use; +constraint forall (i in INSTRUCTIONS) (0 <= output_ADD_MUL_core_latency[i]); +constraint forall (i in INSTRUCTIONS) (output_ADD_MUL_core_use[i] == 1 -> output_core_latency[i] == output_ADD_MUL_core_latency[i]); +array[INSTRUCTIONS] of var int: output_MUL_CORE_core_latency; +array[INSTRUCTIONS] of var 0..1: output_MUL_CORE_core_use; +constraint forall (i in INSTRUCTIONS) (0 <= output_MUL_CORE_core_latency[i]); +constraint forall (i in INSTRUCTIONS) (output_MUL_CORE_core_use[i] == 1 -> output_core_latency[i] == output_MUL_CORE_core_latency[i]); +array[INSTRUCTIONS] of var int: output_LEA_BW_core_latency; +array[INSTRUCTIONS] of var 0..1: output_LEA_BW_core_use; +constraint forall (i in INSTRUCTIONS) (0 <= output_LEA_BW_core_latency[i]); +constraint forall (i in INSTRUCTIONS) (output_LEA_BW_core_use[i] == 1 -> output_core_latency[i] == output_LEA_BW_core_latency[i]); +var LOCATIONS: RET_loc; + + +constraint alldifferent(output_locations); + +constraint output_locations[x21] + output_data_latency[x21] <= output_locations[x23]; +constraint output_locations[x22] + output_data_latency[x22] <= output_locations[x23]; +constraint output_locations[x24] + output_data_latency[x24] <= output_locations[x26]; +constraint output_locations[x25] + output_data_latency[x25] <= output_locations[x26]; +constraint output_locations[x26] + output_data_latency[x26] <= output_locations[x28]; +constraint output_locations[x27] + output_data_latency[x27] <= output_locations[x28]; +constraint output_locations[x29] + output_data_latency[x29] <= output_locations[x31]; +constraint output_locations[x30] + output_data_latency[x30] <= output_locations[x31]; +constraint output_locations[x31] + output_data_latency[x31] <= output_locations[x33]; +constraint output_locations[x32] + output_data_latency[x32] <= output_locations[x33]; +constraint output_locations[x33] + output_data_latency[x33] <= output_locations[x35]; +constraint output_locations[x34] + output_data_latency[x34] <= output_locations[x35]; +constraint output_locations[x36] + output_data_latency[x36] <= output_locations[x38]; +constraint output_locations[x37] + output_data_latency[x37] <= output_locations[x38]; +constraint output_locations[x38] + output_data_latency[x38] <= output_locations[x40]; +constraint output_locations[x39] + output_data_latency[x39] <= output_locations[x40]; +constraint output_locations[x40] + output_data_latency[x40] <= output_locations[x42]; +constraint output_locations[x41] + output_data_latency[x41] <= output_locations[x42]; +constraint output_locations[x42] + output_data_latency[x42] <= output_locations[x44]; +constraint output_locations[x43] + output_data_latency[x43] <= output_locations[x44]; +constraint output_locations[x45] + output_data_latency[x45] <= output_locations[x49]; +constraint output_locations[x20] + output_data_latency[x20] <= output_locations[x50]; +constraint output_locations[x49] + output_data_latency[x49] <= output_locations[x50]; +constraint output_locations[x46] + output_data_latency[x46] <= output_locations[x51]; +constraint output_locations[x50] + output_data_latency[x50] <= output_locations[x52]; +constraint output_locations[x51] + output_data_latency[x51] <= output_locations[x52]; +constraint output_locations[x47] + output_data_latency[x47] <= output_locations[x53]; +constraint output_locations[x52] + output_data_latency[x52] <= output_locations[x54]; +constraint output_locations[x53] + output_data_latency[x53] <= output_locations[x54]; +constraint output_locations[x48] + output_data_latency[x48] <= output_locations[x55]; +constraint output_locations[x54] + output_data_latency[x54] <= output_locations[x56]; +constraint output_locations[x55] + output_data_latency[x55] <= output_locations[x56]; +constraint output_locations[x45] + output_data_latency[x45] <= output_locations[x57]; +constraint output_locations[x23] + output_data_latency[x23] <= output_locations[x58]; +constraint output_locations[x57] + output_data_latency[x57] <= output_locations[x58]; +constraint output_locations[x47] + output_data_latency[x47] <= output_locations[x59]; +constraint output_locations[x58] + output_data_latency[x58] <= output_locations[x60]; +constraint output_locations[x59] + output_data_latency[x59] <= output_locations[x60]; +constraint output_locations[x48] + output_data_latency[x48] <= output_locations[x61]; +constraint output_locations[x60] + output_data_latency[x60] <= output_locations[x62]; +constraint output_locations[x61] + output_data_latency[x61] <= output_locations[x62]; +constraint output_locations[x45] + output_data_latency[x45] <= output_locations[x63]; +constraint output_locations[x28] + output_data_latency[x28] <= output_locations[x64]; +constraint output_locations[x63] + output_data_latency[x63] <= output_locations[x64]; +constraint output_locations[x48] + output_data_latency[x48] <= output_locations[x65]; +constraint output_locations[x64] + output_data_latency[x64] <= output_locations[x66]; +constraint output_locations[x65] + output_data_latency[x65] <= output_locations[x66]; +constraint output_locations[x45] + output_data_latency[x45] <= output_locations[x67]; +constraint output_locations[x35] + output_data_latency[x35] <= output_locations[x68]; +constraint output_locations[x67] + output_data_latency[x67] <= output_locations[x68]; +constraint output_locations[x56] + output_data_latency[x56] <= output_locations[x69]; +constraint output_locations[x56] + output_data_latency[x56] <= output_locations[x70]; +constraint output_locations[x69] + output_data_latency[x69] <= output_locations[x71]; +constraint output_locations[x62] + output_data_latency[x62] <= output_locations[x71]; +constraint output_locations[x71] + output_data_latency[x71] <= output_locations[x72]; + +constraint max([ output_locations[i] + output_data_latency[i] | i in INSTRUCTIONS ]) <= RET_loc; + + +constraint forall (i in INSTRUCTIONS) (input_ops[i] == SHL -> ((output_cores[i] == LEA_BW /\ output_LEA_BW_core_use[i] == 1 /\ output_LEA_BW_core_latency[i] == 4 /\ output_data_latency[i] == 4 /\ output_ADD_MUL_core_use[i] == 0 /\ output_ADD_MUL_core_latency[i] == 0 /\ output_MUL_CORE_core_use[i] == 0 /\ output_MUL_CORE_core_latency[i] == 0))); +constraint forall (i in INSTRUCTIONS) (input_ops[i] == AND -> ((output_cores[i] == LEA_BW /\ output_LEA_BW_core_use[i] == 1 /\ output_LEA_BW_core_latency[i] == 4 /\ output_data_latency[i] == 4 /\ output_ADD_MUL_core_use[i] == 0 /\ output_ADD_MUL_core_latency[i] == 0 /\ output_MUL_CORE_core_use[i] == 0 /\ output_MUL_CORE_core_latency[i] == 0))); +constraint forall (i in INSTRUCTIONS) (input_ops[i] == ADD -> ((output_cores[i] == ADD_MUL /\ output_ADD_MUL_core_use[i] == 1 /\ output_ADD_MUL_core_latency[i] == 4 /\ output_data_latency[i] == 4 /\ output_MUL_CORE_core_use[i] == 0 /\ output_MUL_CORE_core_latency[i] == 0 /\ output_LEA_BW_core_use[i] == 0 /\ output_LEA_BW_core_latency[i] == 0) \/ (output_cores[i] == LEA_BW /\ output_LEA_BW_core_use[i] == 1 /\ output_LEA_BW_core_latency[i] == 4 /\ output_data_latency[i] == 4 /\ output_ADD_MUL_core_use[i] == 0 /\ output_ADD_MUL_core_latency[i] == 0 /\ output_MUL_CORE_core_use[i] == 0 /\ output_MUL_CORE_core_latency[i] == 0))); +constraint forall (i in INSTRUCTIONS) (input_ops[i] == MUL -> ((output_cores[i] == ADD_MUL /\ output_ADD_MUL_core_use[i] == 1 /\ output_ADD_MUL_core_latency[i] == 4 /\ output_data_latency[i] == 12 /\ output_MUL_CORE_core_use[i] == 0 /\ output_MUL_CORE_core_latency[i] == 0 /\ output_LEA_BW_core_use[i] == 0 /\ output_LEA_BW_core_latency[i] == 0) \/ (output_cores[i] == MUL_CORE /\ output_MUL_CORE_core_use[i] == 1 /\ output_MUL_CORE_core_latency[i] == 4 /\ output_data_latency[i] == 12 /\ output_ADD_MUL_core_use[i] == 0 /\ output_ADD_MUL_core_latency[i] == 0 /\ output_LEA_BW_core_use[i] == 0 /\ output_LEA_BW_core_latency[i] == 0))); +constraint forall (i in INSTRUCTIONS) (input_ops[i] == OR -> ((output_cores[i] == LEA_BW /\ output_LEA_BW_core_use[i] == 1 /\ output_LEA_BW_core_latency[i] == 4 /\ output_data_latency[i] == 4 /\ output_ADD_MUL_core_use[i] == 0 /\ output_ADD_MUL_core_latency[i] == 0 /\ output_MUL_CORE_core_use[i] == 0 /\ output_MUL_CORE_core_latency[i] == 0))); +constraint forall (i in INSTRUCTIONS) (input_ops[i] == SHR -> ((output_cores[i] == LEA_BW /\ output_LEA_BW_core_use[i] == 1 /\ output_LEA_BW_core_latency[i] == 4 /\ output_data_latency[i] == 4 /\ output_ADD_MUL_core_use[i] == 0 /\ output_ADD_MUL_core_latency[i] == 0 /\ output_MUL_CORE_core_use[i] == 0 /\ output_MUL_CORE_core_latency[i] == 0))); + +constraint cumulative(output_locations, output_ADD_MUL_core_latency, output_ADD_MUL_core_use, 2); +constraint cumulative(output_locations, output_MUL_CORE_core_latency, output_MUL_CORE_core_use, 1); +constraint cumulative(output_locations, output_LEA_BW_core_latency, output_LEA_BW_core_use, 2); + +solve minimize RET_loc; + +output [ "(" ++ show(INSTRUCTIONS_NAMES[i]) ++ ", " ++ show(CORE_NAMES[fix(output_cores[i])]) ++ ", " ++ show(output_locations[i]) ++ ", " ++ show(output_data_latency[i]) ++ ", " ++ show(output_core_latency[i]) ++ ") ,\n" + | i in INSTRUCTIONS ]; +output [ "RET_loc: " ++ show(RET_loc) ]; diff --git a/etc/compile-by-zinc/femulDisplay_1.mzn b/etc/compile-by-zinc/femulDisplay_1.mzn new file mode 100644 index 000000000..eb423da61 --- /dev/null +++ b/etc/compile-by-zinc/femulDisplay_1.mzn @@ -0,0 +1,92 @@ +include "alldifferent.mzn"; +include "cumulative.mzn"; +%uint64_t x73 = x71 & 0x7ffffffffffff; +%uint128_t x74 = x72 + x66; +%uint64_t x75 = x74 >> 0x33; +%uint64_t x76 = x74 & 0x7ffffffffffff; +%uint128_t x77 = x75 + x68; +%uint64_t x78 = x77 >> 0x33; +%uint64_t x79 = x77 & 0x7ffffffffffff; +%uint128_t x80 = x78 + x44; +%uint64_t x81 = x80 >> 0x33; +%uint64_t x82 = x80 & 0x7ffffffffffff; +%uint64_t x83 = 0x13 * x81; +%uint64_t x84 = x70 + x83; +%uint64_t x85 = x84 >> 0x33; +%uint64_t x86 = x84 & 0x7ffffffffffff; +%uint64_t x87 = x85 + x73; +%uint64_t x88 = x87 >> 0x33; +%uint64_t x89 = x87 & 0x7ffffffffffff; +%uint64_t x90 = x88 + x76; +set of int: CORE = 1..3; +CORE: ADD_MUL = 1; CORE: MUL_CORE = 2; CORE: LEA_BW = 3; array[CORE] of string: CORE_NAMES = ["ADD_MUL", "MUL_CORE", "LEA_BW"]; + +set of int: INSTRUCTIONS = 1..18; +INSTRUCTIONS: x73 = 1; INSTRUCTIONS: x74 = 2; INSTRUCTIONS: x75 = 3; INSTRUCTIONS: x76 = 4; INSTRUCTIONS: x77 = 5; INSTRUCTIONS: x78 = 6; INSTRUCTIONS: x79 = 7; INSTRUCTIONS: x80 = 8; INSTRUCTIONS: x81 = 9; INSTRUCTIONS: x82 = 10; INSTRUCTIONS: x83 = 11; INSTRUCTIONS: x84 = 12; INSTRUCTIONS: x85 = 13; INSTRUCTIONS: x86 = 14; INSTRUCTIONS: x87 = 15; INSTRUCTIONS: x88 = 16; INSTRUCTIONS: x89 = 17; INSTRUCTIONS: x90 = 18; array[INSTRUCTIONS] of string: INSTRUCTIONS_NAMES = ["x73", "x74", "x75", "x76", "x77", "x78", "x79", "x80", "x81", "x82", "x83", "x84", "x85", "x86", "x87", "x88", "x89", "x90"]; + +set of int: OPS = 1..6; +OPS: SHL = 1; OPS: AND = 2; OPS: ADD = 3; OPS: MUL = 4; OPS: OR = 5; OPS: SHR = 6; array[OPS] of string: OPS_NAMES = ["SHL", "AND", "ADD", "MUL", "OR", "SHR"]; + +int: MAX_LOC = 78; + +set of int: LOCATIONS = 1..MAX_LOC; +array[INSTRUCTIONS] of var LOCATIONS: output_locations; +array[INSTRUCTIONS] of var int: output_data_latency; +array[INSTRUCTIONS] of var int: output_core_latency; +array[INSTRUCTIONS] of var CORE: output_cores; +array[INSTRUCTIONS] of OPS: input_ops = [AND, ADD, SHL, AND, ADD, SHL, AND, ADD, SHL, AND, MUL, ADD, SHL, AND, ADD, SHL, AND, ADD]; +array[INSTRUCTIONS] of var int: output_ADD_MUL_core_latency; +array[INSTRUCTIONS] of var 0..1: output_ADD_MUL_core_use; +constraint forall (i in INSTRUCTIONS) (0 <= output_ADD_MUL_core_latency[i]); +constraint forall (i in INSTRUCTIONS) (output_ADD_MUL_core_use[i] == 1 -> output_core_latency[i] == output_ADD_MUL_core_latency[i]); +array[INSTRUCTIONS] of var int: output_MUL_CORE_core_latency; +array[INSTRUCTIONS] of var 0..1: output_MUL_CORE_core_use; +constraint forall (i in INSTRUCTIONS) (0 <= output_MUL_CORE_core_latency[i]); +constraint forall (i in INSTRUCTIONS) (output_MUL_CORE_core_use[i] == 1 -> output_core_latency[i] == output_MUL_CORE_core_latency[i]); +array[INSTRUCTIONS] of var int: output_LEA_BW_core_latency; +array[INSTRUCTIONS] of var 0..1: output_LEA_BW_core_use; +constraint forall (i in INSTRUCTIONS) (0 <= output_LEA_BW_core_latency[i]); +constraint forall (i in INSTRUCTIONS) (output_LEA_BW_core_use[i] == 1 -> output_core_latency[i] == output_LEA_BW_core_latency[i]); +var LOCATIONS: RET_loc; + + +constraint alldifferent(output_locations); + +constraint output_locations[x74] + output_data_latency[x74] <= output_locations[x75]; +constraint output_locations[x74] + output_data_latency[x74] <= output_locations[x76]; +constraint output_locations[x75] + output_data_latency[x75] <= output_locations[x77]; +constraint output_locations[x77] + output_data_latency[x77] <= output_locations[x78]; +constraint output_locations[x77] + output_data_latency[x77] <= output_locations[x79]; +constraint output_locations[x78] + output_data_latency[x78] <= output_locations[x80]; +constraint output_locations[x80] + output_data_latency[x80] <= output_locations[x81]; +constraint output_locations[x80] + output_data_latency[x80] <= output_locations[x82]; +constraint output_locations[x81] + output_data_latency[x81] <= output_locations[x83]; +constraint output_locations[x83] + output_data_latency[x83] <= output_locations[x84]; +constraint output_locations[x84] + output_data_latency[x84] <= output_locations[x85]; +constraint output_locations[x84] + output_data_latency[x84] <= output_locations[x86]; +constraint output_locations[x85] + output_data_latency[x85] <= output_locations[x87]; +constraint output_locations[x73] + output_data_latency[x73] <= output_locations[x87]; +constraint output_locations[x87] + output_data_latency[x87] <= output_locations[x88]; +constraint output_locations[x87] + output_data_latency[x87] <= output_locations[x89]; +constraint output_locations[x88] + output_data_latency[x88] <= output_locations[x90]; +constraint output_locations[x76] + output_data_latency[x76] <= output_locations[x90]; + +constraint max([ output_locations[i] + output_data_latency[i] | i in INSTRUCTIONS ]) <= RET_loc; + + +constraint forall (i in INSTRUCTIONS) (input_ops[i] == SHL -> ((output_cores[i] == LEA_BW /\ output_LEA_BW_core_use[i] == 1 /\ output_LEA_BW_core_latency[i] == 4 /\ output_data_latency[i] == 4 /\ output_ADD_MUL_core_use[i] == 0 /\ output_ADD_MUL_core_latency[i] == 0 /\ output_MUL_CORE_core_use[i] == 0 /\ output_MUL_CORE_core_latency[i] == 0))); +constraint forall (i in INSTRUCTIONS) (input_ops[i] == AND -> ((output_cores[i] == LEA_BW /\ output_LEA_BW_core_use[i] == 1 /\ output_LEA_BW_core_latency[i] == 4 /\ output_data_latency[i] == 4 /\ output_ADD_MUL_core_use[i] == 0 /\ output_ADD_MUL_core_latency[i] == 0 /\ output_MUL_CORE_core_use[i] == 0 /\ output_MUL_CORE_core_latency[i] == 0))); +constraint forall (i in INSTRUCTIONS) (input_ops[i] == ADD -> ((output_cores[i] == ADD_MUL /\ output_ADD_MUL_core_use[i] == 1 /\ output_ADD_MUL_core_latency[i] == 4 /\ output_data_latency[i] == 4 /\ output_MUL_CORE_core_use[i] == 0 /\ output_MUL_CORE_core_latency[i] == 0 /\ output_LEA_BW_core_use[i] == 0 /\ output_LEA_BW_core_latency[i] == 0) \/ (output_cores[i] == LEA_BW /\ output_LEA_BW_core_use[i] == 1 /\ output_LEA_BW_core_latency[i] == 4 /\ output_data_latency[i] == 4 /\ output_ADD_MUL_core_use[i] == 0 /\ output_ADD_MUL_core_latency[i] == 0 /\ output_MUL_CORE_core_use[i] == 0 /\ output_MUL_CORE_core_latency[i] == 0))); +constraint forall (i in INSTRUCTIONS) (input_ops[i] == MUL -> ((output_cores[i] == ADD_MUL /\ output_ADD_MUL_core_use[i] == 1 /\ output_ADD_MUL_core_latency[i] == 4 /\ output_data_latency[i] == 12 /\ output_MUL_CORE_core_use[i] == 0 /\ output_MUL_CORE_core_latency[i] == 0 /\ output_LEA_BW_core_use[i] == 0 /\ output_LEA_BW_core_latency[i] == 0) \/ (output_cores[i] == MUL_CORE /\ output_MUL_CORE_core_use[i] == 1 /\ output_MUL_CORE_core_latency[i] == 4 /\ output_data_latency[i] == 12 /\ output_ADD_MUL_core_use[i] == 0 /\ output_ADD_MUL_core_latency[i] == 0 /\ output_LEA_BW_core_use[i] == 0 /\ output_LEA_BW_core_latency[i] == 0))); +constraint forall (i in INSTRUCTIONS) (input_ops[i] == OR -> ((output_cores[i] == LEA_BW /\ output_LEA_BW_core_use[i] == 1 /\ output_LEA_BW_core_latency[i] == 4 /\ output_data_latency[i] == 4 /\ output_ADD_MUL_core_use[i] == 0 /\ output_ADD_MUL_core_latency[i] == 0 /\ output_MUL_CORE_core_use[i] == 0 /\ output_MUL_CORE_core_latency[i] == 0))); +constraint forall (i in INSTRUCTIONS) (input_ops[i] == SHR -> ((output_cores[i] == LEA_BW /\ output_LEA_BW_core_use[i] == 1 /\ output_LEA_BW_core_latency[i] == 4 /\ output_data_latency[i] == 4 /\ output_ADD_MUL_core_use[i] == 0 /\ output_ADD_MUL_core_latency[i] == 0 /\ output_MUL_CORE_core_use[i] == 0 /\ output_MUL_CORE_core_latency[i] == 0))); + +constraint cumulative(output_locations, output_ADD_MUL_core_latency, output_ADD_MUL_core_use, 2); +constraint cumulative(output_locations, output_MUL_CORE_core_latency, output_MUL_CORE_core_use, 1); +constraint cumulative(output_locations, output_LEA_BW_core_latency, output_LEA_BW_core_use, 2); + +solve minimize RET_loc; + +output [ "(" ++ show(INSTRUCTIONS_NAMES[i]) ++ ", " ++ show(CORE_NAMES[fix(output_cores[i])]) ++ ", " ++ show(output_locations[i]) ++ ", " ++ show(output_data_latency[i]) ++ ", " ++ show(output_core_latency[i]) ++ ") ,\n" + | i in INSTRUCTIONS ]; +output [ "RET_loc: " ++ show(RET_loc) ]; -- cgit v1.2.3