利用高階圖型表示式來製作數學運算器

Abstract

在這一篇論文中,我們提出一個新的方法來解聯立方式 方法中利用高階圖形表示式(word-level decision diagrams)。由於高階圖形表示式本身，它可以表示整數函數以及表示式本身有一些基本數學運算(arithmetic operations)以便可以求出解(solutions)。在初步的實驗中，我們發現將原本方程式的順序重排之後，求解的時間以及減低記憶體要求會不一樣。我們自己發展一套方程式重排引擎(Reorder Engine)，它本身會先分析每一道方程式；之後才會調整方程式的順序以致於在時間以及記憶體的耗損都可以有效地降低。在解聯立方程式的過程中，會利用二元樹狀結構(Binary Tree Structure)來表達我們解聯立方程式的順序及計算模式(computation model)。最後我們會用分割(partition)的方法來處理記憶體耗盡(out of memory)的問題。

While the model checking is getting popular, it would be convenient for users to have an arithmetic solver that can compute solutions to satisfy equation set formulated from datapath. In this paper, we propose a novel technique using word-level decision diagrams (called *PHDDs) to solve equation set. Owing to the property of *PHDDs, it can represent integer function and use a set of word-level arithmetic operations on the *PHDDs graph to obtain solutions represented by BDDs. We develop a Reorder Engine to rearrange the order of equation set so that we can significantly reduce the execution time and memory consumption. By tree structure, the order of equations and the computation model, which is related to variable overlap, can be stored in tree to conveniently compute. However, different tree structures can deeply affect execution time and memory. Finally, for more sophisticated equations, using Partition technique handles out of memory problem for getting partial solutions.