SAT encoding of Board-Level Multi-Terminal Net Assignment

The benchmarks presented here are the results of a satisfiability-based formulation for the board-level multi-terminal net routing problem in the digital design of Clos-Folded FPGA based logic emulation systems. We transform the FPGA board-level routing task into conjunctive normal form (CNF) such that the formula is satisfiable if and only if the problem is routable.

Problem Definition

A detailed description of the problem is given in [SHM-2002]. Here, we briefly outline the basic concepts of the problem.

The FPGAs are referred to as chips. Let us assume that all chips are identical and the interconnection crossbars are used only to connect to the chips but not to each other. Let F be a set of p identical FPGA chips, numbered by 1, 2, ..., p. A chip has a set of I/O ports. I/O ports of each chip are evenly divided into k groups of size m: S1, S2, ..., Sk. We assign a distinct type for each group, Si, i = 1,..., k. We use labels: A, B, C, ..., to represent their types. An I/O port in a group Si possesses the type of Si. In other words, we say I/O ports of each chip are evenly divided into k groups of size m such that (i) type(S1), type(S2), ...., type(Sk) are pairwise distinct; (ii) size(S1) = size(S2) =...= size(Sk) = m.

In terms of the number of terminals per net, two kinds of board-level routing problems (BLRPs) are identified: (i) two-terminal BLRP where all nets are two-terminal nets; and (ii) multiterminal BLRP where at least one net has more than two terminals.

A two-terminal board level routing problem (2BLRP) is defined as follows. Given a set of two-terminal interchip nets M={n1, n2, ..., nN}, where nt = <i, j>, i j, i, j {1, ..., p}, and t=1, 2, ..., N, we want to find an assignment of M to I/O ports of F such that, for each net nt = <i, j>, type(i) = type(j), i j, i, j {1, ..., p}, and t = 1, 2, ... , N.

Note that no net can have its two terminals in the same chip. Any two I/O ports of the same type at different chips can be connected by FPGA crossbar switch. Since we have a one-to-one correspondence between the terminal (the ending point of a net) and its chip, we use the chip number to identify the ends of a net.

In the following, m is the number of the pins having the same type in each chip, k is the number of types in each chip which represents the number of crossbars, and p is the number of FPGA chips. Pins of each chip are evenly routed to k crossbar switches using N nets. A 2BLRP with parameters m, k, p and N is denoted by 2BLRP(m, k, p, N).

A multi-terminal board level routing problem (BLRP) is defined as follows. Given a set of multiterminal interchip nets M={n1, n2, ..., nN}, where nt = {i1, ..., is}, ig ih, ig, ih {1, ..., p}, g, h {1, ..., s}, t = 1, 2, ..., N, find an assignment of M to I/O ports of F such that, for each net nt = {i1, ..., is}, type(ig) = type(ih), ig ih, ig, ih {1, ..., p}, g, h {1, ..., s}, and t = 1, 2, ..., N.

SAT Formulation

To express the constraints, consider the set of requirements for a feasible solution. The requirements are of two types: (1) the covering constraints, and (2) the closure constraints. The first group of constraints ensures that each net is routed at least once. The second group ensures that (2a) no net is routed more than once, and that (2b) for each chip and each pin type, the number of associated nets does not exceed the number of available pins. Further details about generating these constraints in SAT encoding can be found in [SHM-2002].

The Benchmark

The following table shows the detail configuration of the benchmark. Benchmark is the name of a generated benchmark. P is the number of chips. K is the number of pin types. M is the number of pins of each type. Max is the largest number of terminals (size) of a net. Ave is the average size of all nets. Vars is the number of variables needed to encode the problem. Clauses is the number of clauses. Literals is the number of positive and negative polarity literals in all clauses. Routability shows whether the benchmark is satisfiable (routable) or not.

Download the benchmark

Benchmark P K M N Max Ave Vars Clauses Literals Routability
p020_k5_m2_n07 20 5 2 49 7 4 245 12039 35725 yes
p020_k5_m2_n08 20 5 2 52 8 3.8 260 12147 36025 yes
p020_k5_m2_n06 20 5 2 59 6 3.3 295 12149 35975 yes
p020_k5_m2_n05 20 5 2 64 5 3.1 320 12279 36325 yes
p020_k5_m2_n04 20 5 2 76 4 2.6 380 12411 36625 yes
p020_k5_m3_n14 20 5 3 55 13 5.4 275 133855 534375 yes
p020_k5_m3_n11 20 5 3 60 11 5 300 135340 540220 yes
p020_k5_m3_n09 20 5 3 66 9 4.5 330 132051 526950 yes
p020_k5_m3_n08 20 5 3 68 8 4.4 340 132898 530300 yes
p020_k5_m3_n07 20 5 3 77 7 3.9 385 132997 530525 yes
p020_k5_m3_n06 20 5 3 88 6 3.4 440 134218 535200 yes
p020_k5_m3_n05 20 5 3 99 5 3 495 134339 535475 yes
p020_k5_m3_n04 20 5 3 114 4 2.6 570 134504 535850 yes
p020_k3_m3_n08 20 3 3 36 8 5 108 7536 29892 yes
p020_k4_m3_n10 20 4 3 30 10 6 120 21110 84080 no
p020_k4_m3_n08 20 4 3 67 8 3.6 268 39409 156832 yes
p020_k5_m3_n15 20 5 3 30 15 8 150 91620 365910 no
p020_k7_m3_n08 20 7 3 105 8 4 735 811055 3240125 yes
p050_k5_m3_n07 50 5 3 150 7 4 750 244720 975030 no
p050_k5_m3_n08 50 5 3 171 8 4.4 855 337956 1348575 yes
p050_k6_m3_n08 50 6 3 212 8 4.2 1272 911222 3638952 yes
p050_k7_m3_n08 50 7 3 241 8 4.3 1687 2070897 8274189 yes
p100_k5_m3_n08 100 5 3 344 8 4.4 1720 684464 2731320 yes
p150_k5_m3_n08 150 5 3 552 8 4.1 2760 1024647 4088100 yes
p200_k3_m3_n45 200 3 3 45 45 24 135 15843 63057 no
p200_k4_m3_n55 200 4 3 50 55 28 200 70646 281984 no
p200_k5_m3_n55 200 5 3 90 55 28 450 862730 3449210 no
p200_k5_m3_n08 200 5 3 717 8 4.2 3585 1368537 5460525 yes

Download the benchmark

References

[SHM-2002] Xiaoyu Song, William N. N. Hung, Alan Mishchenko, Malzorgata Chrzanowska-Jeske, Alan Coppola and Andrew Kennings. Board-Level Multiterminal Net Assignment. 12th ACM/IEEE Great Lakes Symposium on VLSI (GLSVLSI), New York, New York, April 2002.

[SHM-2003] Xiaoyu Song , William N. N. Hung, Alan Mishchenko, Malzorgata Chrzanowska-Jeske, Andrew Kennings and Alan Coppola. Board-Level Multiterminal Net Assignment for the Partial Cross-Bar Architecture. IEEE Transactions on VLSI Systems, Volume 11, Number 3, June, 2003, pp. 511-514.

For more information, please contact Xiaoyu Song or William N. N. Hung.



E-mail: william_hung AT alumni DOT utexas DOT net
Last Modified: 14 August 2003