講演名 2018-05-16
Partial logic synthesis by using sum of products or product of sums based quantified boolean formulae
ハン ショウラン(東大), ガラバギ アミル マスード(東大), 藤田 昌宏(東大),
PDFダウンロードページ PDFダウンロードページへ
抄録(和)
抄録(英) documentclass[a4paper,11pt]{jarticle}usepackage{kws} usepackage{amssymb}usepackage{amsmath,array,graphicx}usepackage{kantlipsum}graphicspath{{/Users/xiaoranhan/Desktop}}begin{document}OnlyEnglishtrueetitle{Partial logic synthesis by using sum of products or product of sums based quantified boolean formulae}eauthor{Xiaoran Han hspace{2.5cm} Amir Masoud Gharehbaghi hspace{1.8cm} Masahiro Fujita }eaddress{The University of Tokyo hspace{1.5cm} The University of Tokyo hspace{1.5cm} The University of Tokyo }maketitlesection*{Abstract} Partial logic synthesis is to synthesize the vacant portions in the given entire circuit and has been formulated with QBF(Quantified Boolean Formula) using LUT (Look up Table). As LUT can practically represent 16 or so inputs, the vacant portions cannot have large numbers of inputs. In this paper, we show a way to partial synthesis by using SOP (sum of product) and POS (product of sum) based QBF formulation. Any SOP/POS formulae with $n$ variables and $m$ products/sums are represented by a set of coefficients which are associated with literals, and the synthesis problem is to find appropriate values for the coefficients by solving the QBF problems. We show the partial synthesis experiments on ISCAS89 circuits. The SOP and the POS perform better than the previous LUT based QBF method when the vacant portions have more than 16 inputs, however, depending on the circuit, the performance is different. The SOP based QBF method can synthesis up to 27 inputs, the POS based method can synthesis up to 24 inputs. section{Introduction}Synthesis is very important in designing a circuit. By giving the specification, generate a design implementation in terms of logic gates. However, in many cases already have partial of the design. In these cases, instead of synthesize the whole design, we only need to synthesize the partial of the design. There are many existing ways to do logic synthesiscite{b1}cite{b2}cite{b3}cite{b4}. One existing way of partial logic synthesis is using LUT(Look at Table) based QBF(Quantified Boolean Formula) formulationcite{b5}. Use LUT to represent the vacant parts, which need to be synthesized, and solve by QBF formulation. This method can synthesize the logic gate practically with up to 16 inputs. According to the LUT, if the number of inputs of the gate is $m$, then the number of the variables is $2^m$. So, the number of variables grows exponentially when the number of inputs increased. Therefore, LUT based QBF formulation couldn't synthesize the vacant parts with large inputs. In order to solve this problem, we introduce another two ways, SOP and POS based QBF formula. In these methods, instead of using LUT, using SOP and POS models to represent the vacant portions, which decrease the number of variables compared with the LUT based QBF formulation. We conduct the various SOP based QBF formulation and POS based QBF formulation experiments on ISCAS 89 benchmark circuits. The paper is organized as follows. In the next section we give basic knowledge on LUT based QBF synthesis. Then in the following section we introduce SOP based QBF partial synthesis, and POS based QBF partial synthesis. Then we show various experimental results and discuss the differences between the two methods. The last section gives concluding remarks and the future work. section{LUT based QBF partial synthesis}Here we introduce LUT based QBF synthesis. The experiment is shown in Figure 1. The black box is the vacant part that need to be synthesized. We use the LUT to represent the black box, and introduce $a^m$ variables each of which corresponds to a row in the truth table of the function, f, with $m$ inputs, any logic functions with $m$ inputs can be represented. If we can find appropriate values for such program variables, we can identify the function f. In order to synthesize the black box, for all the possible inputs $X$, $x_1 = x_2 = X$, the corresponding outputs $y_1(X) $ and $y_2(X)$ are also the same. We solve this problem by using QBF(Quantified Boolean Formula) formulationcite{b6}, which we represent in equation 1. begin{equation}exists a_1, a_2, a_{2^m}, forall X Rightarrow y_1(X) = y_2(X) end{equation}begin{figure} centering includegraphics[width=0.85linewidth, height=6cm]{1} caption{LUT based QBF partial synthesis experiment} label{fig:1}end{figure}As long as the number of inputs is small, up to 16 or less, this methods can quickly find the solution for most of the ISCAS89 circuits. However, if the number of inputs increases, the number of variables that needed to be solved also exponentially increased. Therefore, we introduce the following SOP and POS based QBF partial synthesis. section{SOP and POS based QBF partial synthesis}subsection{SOP based partial synthesis}SOP format is defined as follows: Let $X = x_1, x_2, ..., x_n$, be a set of Boolean variables and let $f(x)$ be boolean function defined over these variables. Use $c_m$ to denote some products over the variables in $X$. We consider synthesizing $m$ products $c_1, c_2, ..., c_m$ that are equivalent to $f(x)$. begin{equation}exists c_1,...c_m, forall X Rightarrowvee^m_{i=1} c_m(X) = f(X)label{eq1}end{equation}The product terms $c_1, c_2,...c_m$ are defined in following: Exists the set of variables $A$: $A = { a_{ij0}, a_{ij1} | 1 leqslant i leqslant m, 1 leqslant j leqslant n} $. Let $g(A, X) = vee_{i=1} ^m wedge ^n _{j=1} (a_{ij0} wedge bar{x_j} vee a_{ij1} wedge x_j$) represents the formula in DNF with $m$ conjunctions over the variables $X$. Here when $a_{ij0} = 0 wedge a_{ij1} = 1 $, representing the clause $x_j$ is in the product $i$. When $a_{ij0} = 1 wedge a_{ij1} = 0 $, representing the clause $bar{x_j}$ is in the product $i$. When $a_{ij0=1} wedge a_{ij1} = 1$, representing $x_j$ is a don't care in product $i$. When $a_{ij0} = 0 wedge a_{ij1} = 0$, representing the constant 0 is in the product $i$. Given the above definition, we can rewrite equation 2 as follows:begin{equation}exists A, forall X Rightarrow g(A,X) = f(X) label{eq2}end{equation}Now we need to find the set of variables $A$ that satisfied this formula. We solve this formula by using QBF solver implemented on ABCcite{b7}. subsection{SOP based partial synthesis experiment}Now let us discuss the experiment of SOP based partial synthesis. The experiment is shown in Figure 2. We use the ISCAS89 benchmark circuit, and extract sub circuit with more than 16 inputs. We replace the extracted sub circuit with a black box, which is represented by SOP. For all the possible inputs $X$, $x_1=x_2=X$, the corresponding outputs $y_1(X)$ and $y_2(X)$ are also the same. In the experiment, we know which nodes are the internal inputs of the black box, and the internal output of the black box. Then we present the black box sub circuit's function in the following SOP function: begin{equation*}vee_{i=1} ^m wedge ^n _{j=1} (a_{ij0} wedge bar{x_j} vee a_{ij1} wedge x_j) end{equation*}Then we identify the set of variables $A$ by QBF formulation, the formula is written in equation 4. begin{equation}exists A, forall X Rightarrow y_1(X) = y_2(X)label{eq2}end{equation}We get the result by using QBF solver. begin{figure} centering includegraphics[width=0.85linewidth, height=6cm]{2} caption{SOP based partial synthesis experiment} label{fig:2}end{figure}subsection{POS based partial synthesis}POS on the other hand is the complement of the SOP. The POS based QBF partial synthesis is defined in the following: begin{equation}exists A forall X Rightarrow overline{vee_{i=1} ^m wedge ^n _{j=1} (a_{ij0} wedge bar{x_j} vee a_{ij1} wedge x_j)} = f(X) end{equation}And by using the QBF solver, we could get the variables that satisfied the formula. subsection{POS based partial synthesis experiment} The experiment is shown in Figure 3. Simply add a not gate at the output of the SOP based way. In the POS based partial synthesis experiment, we present the black box sub circuit's function in the following formation: begin{equation*} overline{vee_{i=1} ^m wedge ^n _{j=1} (a_{ij0} wedge bar{x_j} vee a_{ij1} wedge x_j) }end{equation*}Then we identify the set of variables $A$ by QBF formulation, the formula is written in equation 6. begin{equation}exists A, forall X Rightarrow y_1(X) = y_2(X)label{eq2}end{equation}We get the result by using QBF solver. begin{figure} centering includegraphics[width=0.85linewidth, height=6cm]{3} caption{POs based partial synthesis experiment} label{fig:3}end{figure}section{Experiment Results}subsection{SOP and LUT based QBF partial synthesis comparison}Table~ref{tab1} shows the experiments of small number of inputs on both LUT and SOP based way. As we can see, when the number of inputs is small, LUT and SOP based way have the same performance, since the number of iterations are the same. Both can solve the problem well. begin{table}[htbp] Large resizebox{columnwidth}{!}{% resizebox{!}{1textheight}{ begin{tabular}{|c|c|c|c|c|} hline & LUT(3 inputs) & SOP(3 inputs) & LUT(4 inputs) & SOP(4 inputs) \ hline s1423& 1 & 1 & 1 & 1\ hline s1494& 1 & 1 & 1 & 1\ hline s9234& 1 & 1 & 1 & 1\ hline end{tabular} } } caption{SOP and LUT based QBF partial synthesis experiments} label{tab1}end{table}subsection{POS and LUT based QBF partial synthesis comparison}Table~ref{tab2} shows the experiments of small number of inputs on both LUT and POS based way. As we can see, when the number of inputs is small, POS has better performance than LUT, which has much less iteration times. begin{table}[htbp] Large resizebox{columnwidth}{!}{% resizebox{!}{1textheight}{ begin{tabular}{|c|c|c|c|c|} hline & LUT(3 inputs) & POS(3 inputs) & LUT(4 inputs) & POS(4 inputs) \ hline s1488& 7 & 1 & 14 & 1\ hline s5378& 5 & 1 & 14 & 1\ hline s13207& 2 & 1 & 4 & 1\ hline s15850& 7 & 1 & 4 & 1\ hline s38417& 6 & 1 & 15 & 1\ hline end{tabular} } } caption{POS and LUT based QBF partial synthesis experiments} label{tab2}end{table}subsection{SOP based QBF partial synthesis with more than 16 inputs}Now, we show the experiment results with the number of inputs more than 16, where LUT based QBF formula couldn't solve. The experiment results on ISCAS 89 benchmark circuits are showed in the following in Table~ref{tab3}, Table~ref{tab4}, and Table~ref{tab5}. begin{table}[htbp] Large resizebox{columnwidth}{!}{% resizebox{!}{1textheight}{ begin{tabular}{|c|c|c|c|c|c|c|} hline textbf{}&multicolumn{6}{|c|}{textbf{S38584 benchmark circuit}} \ hline Number of inputs& 27 & 24 & 19 & 18 & 17 & 17\ hline Number of products & 2 & 7 & 7 & 6 & 9 & 3 \ hline Average Runtime(sec) & 0.06 & 10.54 & 1.12 & 0.61 & 7.3 & 0.25 \ hline end{tabular} }} caption{SOP based QBF partial synthesis experiment result on S38584 benchmark circuit} label{tab3} bigskip Large resizebox{columnwidth}{!}{% resizebox{!}{1textheight}{ begin{tabular}{|c|c|c|c|c|c|c|} hline textbf{}&multicolumn{6}{|c|}{textbf{S15850 benchmark circuit}} \ hline Number of inputs& 26 & 25 & 20 & 19 & 19 & 18\ hline Number of products & 1 & 9 & 8 & 9 & 2 & 6 \ hline Average Runtime(sec) & 0.00 & 14.22 & 320 & 8.66 & 0.35 & 0.1 \ hline end{tabular} }} caption{SOP based QBF partial synthesis experiment result on S15850 benchmark circuit} label{tab4} bigskip Large resizebox{columnwidth}{!}{% resizebox{!}{1textheight}{ begin{tabular}{|c|c|c|c|c|} hline textbf{}&multicolumn{4}{|c|}{textbf{S13207 benchmark circuit}} \ hline Number of inputs& 26 & 20 & 17 & 16\ hline Number of products & 13 & 16 & 1 & 1\ hline Average Runtime(sec) & 94.92 & 138.13 & 0.00 & 0.01\ hline end{tabular} }} caption{SOP based QBF partial synthesis experiment result on S13207 benchmark circuit} label{tab5}end{table}As we can see from the Table~ref{tab3}, Table~ref{tab4}, and Table~ref{tab5}. SOP based QBF formula could synthesize up to 27 inputs with 2 product terms in Table~ref{tab3}, and 26 inputs with 13 product terms in Table~ref{tab5}. The runtime depends on the number of inputs and number of products. When the number of inputs becomes larger or the number of product terms becomes larger, the runtime increases. subsection{POS based QBF partial synthesis experiment results compared with SOP based QBF partial synthesis}Here we show the experiment results on both SOP and POS based QBF partial synthesis experiment results in Table~ref{tab6}, Table~ref{tab7}, and Table~ref{tab8}. In the experiment, the POS based QBF partial synthesis can synthesize the gate with number of inputs up to 24 with 14 product terms. The limitaion is slightly less than SOP based QBF formulation, which can synthesize the number of inputs up to 27 with 2 product terms. begin{table}[htbp] Large resizebox{columnwidth}{!}{% begin{tabular}{|c|c|c|c|} hline textbf{}&multicolumn{3}{|c|}{textbf{S15850 benchmark circuit}} \ hline Type of formulation& POS & SOP & SOP \ hline Number of inputs& 24 & 25 & 26\ hline Number of products& 14 & 9 & 1 \ hline Average Runtime(sec) & 117.62 & 14.22 & 0.00 \ hline end{tabular} } caption{SOP and POS based QBF partial synthesis experiment results on S15850 benchmark circuit} label{tab6} Large resizebox{columnwidth}{!}{% begin{tabular}{|c|c|c|c|} hline textbf{}&multicolumn{3}{|c|}{textbf{S13207 benchmark circuit}} \ hline Type of formulation& POS & SOP & SOP \ hline Number of inputs& 24 & 26 & 20\ hline Number of products& 11 & 13 & 16\ hline Average Runtime(sec) & 18.06 & 94.92 & 138.13 \ hline end{tabular} } caption{SOP and POS based QBF partial synthesis experiment results on S13207 benchmark circuit} label{tab7} bigskip Large resizebox{columnwidth}{!}{% begin{tabular}{|c|c|c|} hline textbf{}&multicolumn{2}{|c|}{textbf{S9234 benchmark circuit}} \ hline Type of formulation& POS & SOP \ hline Number of inputs& 20 & 19 \ hline Number of products& 6 & 9\ hline Average Runtime(sec) & 0.17 & 6.56 \ hline end{tabular} } caption{SOP and POS based QBF partial synthesis experiment results on S9234 benchmark circuit} label{tab8}end{table}subsection{Discussion}Depending on different vacant portions, SOP and POS have totally different performances. While the SOP based way works, the POS based way doesn't work. However, while the POS based way works, the SOP based way doesn't work at all. Runtime for SOP and POS based way both depend on the number of inputs, and the number of products. Because when the number of inputs or the number of products increase, the total number of variaibles increase as well. Therefore, the runtime increases significantly. However, compared with LUT based way, which the number of the variables is increased in exponential way, in SOP and POS based way, the number of variables is increased in polynomial way. Therefore SOP and POS based way show much more potential in solving the large number of inputs cases. section{Conclusion and future work}Using the SOP or POS based QBF formulat
キーワード(和)
キーワード(英) Partial logic synthesislogic correctionQBFSOP representationSOP representationECO
資料番号 VLD2018-1
発行日 2018-05-09 (VLD)

研究会情報
研究会 VLD / IPSJ-SLDM
開催期間 2018/5/16(から1日開催)
開催地(和) 北九州国際会議場
開催地(英) Kitakyushu International Conference Center
テーマ(和) システム設計および一般
テーマ(英) System Design, etc.
委員長氏名(和) 越智 裕之(立命館大) / 田宮 豊(富士通研)
委員長氏名(英) Hiroyuki Ochi(Ritsumeikan Univ.) / Yutaka Tamiya(Fujitsu Laboratories)
副委員長氏名(和) 峯岸 孝行(三菱電機)
副委員長氏名(英) Noriyuki Minegishi(Mitsubishi Electric)
幹事氏名(和) 永山 忍(広島市大) / 新田 高庸(NTTデバイスイノベーションセンタ) / 柴田 誠也(NEC) / 密山 幸男(高知工科大) / 細谷 英一(NTT)
幹事氏名(英) Shinobu Nagayama(Hiroshima City Univ.) / Koyo Nitta(NTT) / Seiya Shibata(NEC) / Yukio Mitsuyama(Kochi Univ. of Tech.) / Eiichi Hosoya(NTT)
幹事補佐氏名(和)
幹事補佐氏名(英)

講演論文情報詳細
申込み研究会 Technical Committee on VLSI Design Technologies / Special Interest Group on System and LSI Design Methodology
本文の言語 ENG
タイトル(和)
サブタイトル(和)
タイトル(英) Partial logic synthesis by using sum of products or product of sums based quantified boolean formulae
サブタイトル(和)
キーワード(1)(和/英) / Partial logic synthesislogic correctionQBFSOP representationSOP representationECO
第 1 著者 氏名(和/英) ハン ショウラン / Xiaoran Han
第 1 著者 所属(和/英) 東京大学(略称:東大)
University of Tokyo(略称:UTokyo)
第 2 著者 氏名(和/英) ガラバギ アミル マスード / Amir Masoud Gharehbaghi
第 2 著者 所属(和/英) 東京大学(略称:東大)
University of Tokyo(略称:UTokyo)
第 3 著者 氏名(和/英) 藤田 昌宏 / Masahiro Fujita
第 3 著者 所属(和/英) 東京大学(略称:東大)
University of Tokyo(略称:UTokyo)
発表年月日 2018-05-16
資料番号 VLD2018-1
巻番号(vol) vol.118
号番号(no) VLD-29
ページ範囲 pp.1-5(VLD),
ページ数 5
発行日 2018-05-09 (VLD)