Improving Taylor Expansion Diagrams for Boolean Function Manipulation
- 格式：pdf
- 大小：209.68 KB
- 文档页数：6
Improving Taylor Expansion Diagrams for Boolean Function Manipulation Pejman Lotfikamran, Mostafa Naderi, Hadi Parandeh Afshar, Hamid Shojaei and Zainalabedin Navabi Electrical and Computer Engineering Department, Faculty of Engineering / University of Tehran / Tehran, Iran {plotfi, mnaderi, hparand, shojai } @ cad.ece.ut.ac.ir Tel: 617-373-3034; Fax: 617-373-8973; navabi@ece.neu.edu
Abstract: Increasing size and complexity of digital systems requires higher level structures for verification. Recently
a new, canonical and graph-based representation called TED has been introduced. TED can represent algebraic equations effectively but suffers from not having a good logic level representation. In this paper, we present modifications to TED that improve its ability for logic level representation. Our experimental results show a 100% reduction in the number of TED nodes in some benchmarks.
1. Introduction Today hardware complexity increases and makes verification process more essential and critical. Therefore validating of a design plays an important role, and a reliable and high level method for validating a design is essential. In many verification techniques, functions and relations are represented in a data structure, which is canonical and compact, for applying verification algorithms. Several data structures like ROBDD [1], FDD [2], KFDD [3], HDD [4], *BMD [5], k*BMD [6] and TED [7] [8] [9] are proposed. All of these structures are graph based and canonical. The latter, (TED) is a new, canonical and graph-based representation for algebraic and boolean functions. It uses the Taylor series as decomposition rule and supports more than one degree arithmetic functions. Our experiences show that although TED can represent algebraic equations effectively, it suffers from not having a good logic level representation. When a design consists of both algebraic and logic parts, its TED occupies a large amount of memory. Therefore, it is necessary to have a representation which can represent both algebraic and logic level designs effectively. In this paper, we propose Improved TED, which can represent Algebraic and Logic level functions better than TED. However, in this paper, our focus is on Logic level improvement of Improved TED. This paper is organized as follows: In Section 2, TED is introduced briefly. In Section 3, a general idea about our Improved TED’s structure is introduced by some examples. In Section 4, Improved TED is introduced formally and would be shown that this structure is canonical. Experimental results are discussed in Section 5 and conclusion part is the last Section.
2. Taylor Expansion Diagrams TED is a graph-based representation which uses the Taylor series as decomposition rule [7] [8] [9]. The Taylor series of a real differentiable function f(x) around x=0 are:
...)0()3(3!31
)0(''2
!21
)0(')0()(++++=fxfxxffxf (1)
Where f’ (0), f’’ (0) and f (3) (0) are first, second and third derivations of function f around x=0 respectively. The decomposition will be performed based on Equation (1) recursively. It has been proved that, with a special restriction on the order of variables, TED is a canonical representation [7] [8] [9]. For functions typically encountered in RTL specifications (e.g. x – y, x + y and xk for arbitrary k, etc), TED is
linear in the number of variables [7] [8] [9]. TED can also represent functions containing both algebraic and boolean expressions [7] [8] [9]. To represent boolean expressions, the following formulae should be used [7] [8] [9]: Not(x) = x
′ = 1 – x (2)
And(x, y) = x ∧ y = x * y (3) Or(x, y) = x ∨ y = x + y – x * y (4) Any circuit, containing purely boolean logic, can be represented using these formulae [7] [8] [9]. 3. Improved TED This section, presents the idea of Improved TED by some examples. The details of this idea are discussed in the next section. Consider the TED representation of three basic boolean functions (And, Or, Not) in Fig.1.
-1abb011
Or (a + b - a * b)aba10011
And (a * b)Not (1-a)
-1 Fig.1. TED representation of basic boolean functions As it is shown, Not and And functions are presented with minimal nodes, but the Or function has some extra nodes in comparison with binary decision diagrams. So improving the TED representation of this function would reduce the size of boolean functions’ TED representation. As explained, the TED of Or function is constructed according to equation 4, Where ‘a’ and ‘b’ are two valued integer variables (0 and 1). If we consider the ‘a’ variable as root, then two edges are originated from it: • 0-child, which is equal to ‘b’ • 1-child, which is equal to ’b−1’. As ‘a’ and ‘b’ are two valued variables (0 and 1), then function ‘b−1’ logically is the complement of ‘b’. This property can be used for graph reduction. Indeed, the sub-graph of ‘b’ representation can be shared between 0-child and 1-child of the root node. This requires that an attribute is added to edges’ structure. This attribute is used to show the complementation of the following node. For example, the TED representation of the Or function is converted to the graph shown in Fig.2.
