This paper describes the multithreaded MiraXT SAT solver which was designed to take advantage of current and future shared memory multiprocessor systems. The paper highlights design and implementation details that allow the multiple threads to run and cooperate efficiently. Results show that in single threaded mode, MiraXT compares well to other state of the art solvers on industrial problems. In threaded mode, it provides cutting edge performance, as speedup is obtained on both SAT and UNSAT instances.
1 June 2009 in Journal on Satisfiability, Boolean Modeling and Computation
This article describes PaMiraXT, a powerful parallel SAT algorithm. PaMiraXT follows a master/client model based on message passing, making it suitable for any kind of workstation cluster. For the clients, MiraXT is used, which itself is thread-based
We present SATSEQ, a timing-aware ATPG system for small-delay faults in non-scan circuits. The tool identifies the longest paths suitable for functional fault propagation and generates the shortest possible sub-sequences per fault. Based on advanced model-checking techniques, SATSEQ provides detection of small-delay faults through the longest functional paths. All test sequences start at the circuit's initial state; therefore, overtesting is avoided. Moreover, potential invalidation of the fault detection is taken into account. Experimental results show high detection and better performance than scan testing in terms of test application time and overtesting-avoidance.
We present a flow to extract, simulate and generate test patterns for interconnect open defects. In contrast to previous work, the accuracy of defect modeling is improved by taking the thresholds of logic gates as well as noise margins into account. Efficient fault simulation is enabled by employing an aggressive fault collapsing strategy and an optimized fault list ordering heuristic which allows to combine the advantages of event-driven simulation with bit parallelism. Test generation complexity is kept in check by generating patterns for technology-independent segment-stuck-at faults first, thus reducing (though not completely eliminating) the need for sophisticated technology-aware test generation. Moreover, a comprehensive untestability analysis identifies new classes of untestable faults. Experimental results demonstrate high efficiency of the new flow, outperforming earlier work by two orders of magnitude.
21 January 2008 in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Test application at reduced power supply voltage (low-voltage testing) or reduced temperature (low-temperature testing) can improve the defect coverage of a test set, particularly of resistive short defects. Using a probabilistic model of two-line nonfeedback short defects, we quantify the coverage impact of low-voltage and low-temperature testing for different voltages and temperatures. Effects of statistical process variations are not considered in the model. When quantifying the coverage increase, we differentiate between defects missed by the test set at nominal conditions and undetectable defects (flaws) detected at non nominal conditions. In our analysis, the performance degradation of the device caused by lower power supply voltage is accounted for. Furthermore, we describe a situation in which defects detected by conventional testing are missed by low-voltage testing and quantify the resulting coverage loss. Experimental results suggest that test quality is improved even if no cost increase is allowed. If multiple test applications are acceptable, a combination of low voltage and low temperature turns out to provide the best coverage of both hard defects and flaws.