Drechsler, Rolf
Loading...
Preferred name
Drechsler, Rolf
Official Name
Drechsler, Rolf
Alternative Name
Dechler, Rolf
Rolf, Dechsler
Main Affiliation
Email
drechsler@uni-bremen.de
ORCID
GND
2 results
Now showing 1 - 2 of 2
- Some of the metrics are blocked by yourconsent settings
Item type:Publication, On Acceleration of SAT-Based ATPG for Industrial Designs(IEE, 2008-06-17); ; ; ; Due to the rapidly growing size of integrated circuits, there is a need for new algorithms for automatic test pattern generation (ATPG). While classical algorithms reach their limit, there have been recent advances in algorithms to solve Boolean Satisfiability (SAT). Because Boolean SAT solvers are working on conjunctive normal forms (CNFs), the problem has to be transformed. During transformation, relevant information about the problem might get lost and, therefore, is not available in the solving process. In this paper, we present a technique that applies structural knowledge about the circuit during the transformation. As a result, the size of the problem instances decreases, as well as the run time of the ATPG process. The technique was implemented, and experimental results are presented. The approach was combined with the ATPG framework of NXP Semiconductors. It is shown that the overall performance of an industrial framework can significantly be improved. Further experiments show the benefits with regard to the efficiency and robustness of the combined approach.journal articleBand:27Heft:7113 124 - Some of the metrics are blocked by yourconsent settings
Item type:Publication, RevSCA-2.0: SCA-Based Formal Verification of Nontrivial Multipliers Using Reverse Engineering and Local Vanishing RemovalThe formal verification of integer multipliers is one of the important but challenging problems in the verification community. Recently, the methods based on symbolic computer algebra (SCA) have shown very good results in comparison to all other existing proof techniques. However, when it comes to verification of huge and structurally complex multipliers, they completely fail as an explosion happens in the number of monomials. The reason for this explosion is the generation of redundant monomials known as vanishing monomials. This article introduces the SCA-based approach REVSCA-2.0 that combines reverse engineering and local vanishing removal to verify large and nontrivial multipliers. For our approach, we first come up with a theory for the origin of vanishing monomials, i.e., we prove that the gates/nodes where both outputs of half adders (HAs) converge are the origins of vanishing monomials. Then, we propose a dedicated reverse engineering technique to identify atomic blocks including HAs. The identified HAs are the basis for detecting converging cones and locally removing vanishing monomials, which finally results in a vanishing-free global backward rewriting. The efficiency of REVSCA-2.0 is demonstrated using an extensive set of multipliers with up to several million gates.journal articleBand:41Heft:5166 201