Refine
Document Type
- Report (2)
Has Fulltext
- yes (2)
Keywords
- Boolean polynomials (1)
- Gröber basis (1)
- algebraic cryptoanalysis (1)
- analog circuits (1)
- formal verification (1)
- interval arithmetic (1)
- parametric (1)
- satisfiability (1)
- tolerance analysis (1)
Faculty / Organisational entity
This work presents a new framework for Gröbner basis computations with Boolean polynomials. Boolean polynomials can be modeled in a rather simple way, with both coefficients and degree per variable lying in {0, 1}. The ring of Boolean polynomials is, however, not a polynomial ring, but rather the quotient ring of the polynomial ring over the field with two elements modulo the field equations x2 = x for each variable x. Therefore, the usual polynomial data structures seem not to be appropriate for fast Gröbner basis computations. We introduce a specialized data structure for Boolean polynomials based on zero-suppressed binary decision diagrams (ZDDs), which is capable of handling these polynomials more efficiently with respect to memory consumption and also computational speed. Furthermore, we concentrate on high-level algorithmic aspects, taking into account the new data structures as well as structural properties of Boolean polynomials. For example, a new useless-pair criterion for Gröbner basis computations in Boolean rings is introduced. One of the motivations for our work is the growing importance of formal hardware and software verification based on Boolean expressions, which suffer – besides from the complexity of the problems – from the lack of an adequate treatment of arithmetic components. We are convinced that algebraic methods are more suited and we believe that our preliminary implementation shows that Gröbner bases on specific data structures can be capable to handle problems of industrial size.
Reliable methods for the analysis of tolerance-affected analog circuits are of great importance in nowadays microelectronics. It is impossible to produce circuits with exactly those parameter specifications proposed in the design process. Such component tolerances will always lead to small variations of a circuit’s properties, which may result in unexpected behaviour. If lower and upper bounds to parameter variations can be read off the manufacturing process, interval arithmetic naturally enters the circuit analysis area. This paper focuses on the frequency-response analysis of linear analog circuits, typically consisting of current and voltage sources as well as resistors, capacitances, inductances, and several variants of controlled sources. These kind of circuits are still widely used in analog circuit design as equivalent circuit diagrams for representing in certain application tasks Interval methods have been applied to analog circuits before. But yet this was restricted to circuit equations only, with no interdependencies between the matrix elements. But there also exist formulations of analog circuit equations containing dependent terms. Hence, for an efficient application of interval methods, it is crucial to regard possible dependencies in circuit equations. Part and parcel of this strategy is the handling of fill-in patterns for those parameters related to uncertain components. These patterns are used in linear circuit analysis for efficient equation setup. Such systems can efficiently be solved by successive application of the Sherman-Morrison formula. The approach can also be extended to complex-valued systems from frequency domain analysis of more general linear circuits. Complex values result here from a Laplace transform of frequency-dependent components like capacitances and inductances. In order to apply interval techniques, a real representation of the linear system of equations can be used for separate treatment of real and imaginary part of the variables. In this representation each parameter corresponds to the superposition of two fill-in patterns. Crude bounds – obtained by treating both patterns independently – can be improved by consideration of the correlations to tighter enclosures of the solution. The techniques described above have been implemented as an extension to the toolbox Analog Insydes, an add-on package to the computer algebra system Mathematica for modeling, analysis, and design of analog circuits.