CN117970070B - Boolean satisfaction-based compression method and device for automatic circuit test vector - Google Patents

Abstract

The present application discloses a method and device for compressing automatic test vectors of circuits based on Boolean satisfiability. The method includes: obtaining the original test vector set and test fault set of the target chip, wherein the original test vector set includes multiple test vectors; using the first test vector subset of the original test vector set to perform fault simulation on all test faults in the test fault set, and determine the tested fault subset of the test fault set; using the second test vector subset of the original test vector set and the untested fault subset of the test fault set to establish a local fault dictionary, the local fault dictionary is used to record the association between the test vectors in the second test vector subset and the test faults in the untested fault subset; calling the Pure MaxSAT problem solver to solve the local fault dictionary, thereby obtaining a streamlined test vector. The present application solves the technical problem that vector compression is relatively time-consuming in the related art.

Description

Method and device for compressing circuit automatic test vectors based on Boolean satisfiability

Technical Field

The present application relates to the field of chip testing, and in particular, to a method and device for compressing circuit automatic test vectors based on Boolean satisfiability.

Background Art

This section is intended to provide a background or context to what is stated in the claims or specification, and no admission is made that what is described herein is prior art by inclusion in this section.

Static Test Vector Compression is a technique used in chip testing to reduce test data storage requirements and test time while maintaining full coverage of chip functions. In chip testing, a large number of test vectors are needed to verify the functionality and performance of the chip. These test vectors are a series of input data used to stimulate the chip and observe the output results. However, the number of test vectors is usually very large, especially for complex chip designs, which can lead to a significant increase in storage requirements and test time.

Static test vector compression technology compresses test vectors by utilizing the redundancy and repetitiveness between test vectors and the internal state information of the chip. Specifically, it can achieve compression in the following ways:

1) Coding-based compression: This method uses coding techniques to convert the test vector into a more compact representation. For example, run-length encoding can be used to encode consecutive identical bit patterns into a count value, thereby reducing storage space.

2) Compression based on pattern matching: This method achieves compression by identifying and storing repeated patterns between test vectors. When the same test vector or a similar test vector sequence is found, the pattern only needs to be stored once, and then the corresponding instructions or parameters are used to reproduce the pattern.

3) Compression based on state compression: This method uses the internal state information of the chip to compress the test vectors. By storing and reusing the internal state of the chip during the test process, the number of test vectors required can be reduced. This can be achieved by sharing state information between test vectors or through state recovery techniques.

Static test vector compression technology can significantly reduce the storage requirements and test time of test data, thereby reducing the cost and complexity of chip testing. However, static test vector compression technology also faces some challenges. For example, the compression and decompression process may increase the test time because additional calculations and operations are required. In addition, the design and implementation of the compression algorithm need to take into account the characteristics and test requirements of the chip to ensure that the compressed test vectors can still effectively cover the functions of the chip.

To address the above-mentioned problems, no effective solution has been proposed yet.

Summary of the invention

The embodiments of the present application provide a method and device for compressing circuit automatic test vectors based on Boolean satisfiability, so as to at least solve the technical problem that vector compression in related technologies is relatively time-consuming.

According to one aspect of an embodiment of the present application, a method for compressing automatic test vectors of circuits based on Boolean satisfiability is provided, comprising: obtaining an original test vector set and a test fault set of a target chip, wherein the original test vector set includes multiple test vectors, and the test fault set includes multiple test faults; using a first test vector subset of the original test vector set, performing fault simulation on all test faults in the test fault set, and determining a tested fault subset of the test fault set, wherein the original test vector set includes the first test vector subset and the second test vector subset, and the test fault set includes the tested fault subset and the untested fault subset, the tested fault subset is used to store tested test faults, and the untested fault subset is used to store untested test faults; using the second test vector subset and the untested fault subset, establishing a local fault dictionary, wherein the local fault dictionary is used to record the association between the test vectors in the second test vector subset and the test faults in the untested fault subset; calling a Pure MaxSAT problem solver to solve the local fault dictionary, thereby obtaining a simplified test vector.

Optionally, the first test vector subset of the original test vector set is used to perform fault simulation on all test faults in the test fault set to determine the tested fault subset of the test fault set, including: dividing the original test vector set into the first test vector subset and the second test vector subset according to a preset ratio, wherein the number of test vectors in the second test vector subset is greater than the number of test vectors in the first test vector subset; and the first test vector subset is used to perform fault simulation on all test faults in the test fault set to determine the tested fault subset.

Optionally, a local fault dictionary is established using the second test vector subset and the untested fault subset, including: using the test vectors in the second test vector subset to perform fault simulation on the test faults in the untested fault subset to obtain the relationship between each test vector and all test faults; and establishing the local fault dictionary using the relationship between each test vector and all test faults, wherein each row of the local fault dictionary corresponds to a test vector or a test fault, and each column corresponds to a test fault or a test vector, and an element at the intersection of any row and a column is used to represent the relationship between the corresponding test vector and the corresponding test fault, and when the value of the element is 1, it indicates that the test vector can detect the test fault, and when the value of the element is 0, it indicates that the test vector cannot detect the test fault.

Optionally, after calling the Pure MaxSAT problem solver to solve the local fault dictionary to obtain a simplified test vector, the method further includes: using the obtained simplified test vector of the second test vector subset and the first test vector subset as the final test vector of the target chip.

Optionally, obtaining the original test vector set of the target chip includes: before calling the automatic test vector generation ATPG tool to generate test vectors for the target chip, setting the test mode of the automatic test vector generation tool to a specified test mode, wherein the specified test mode is used to indicate the number of vectors n required for a test fault, and the value of n is 2 or 3; calling the automatic test vector generation ATPG tool to generate the original test vector set for the target chip.

Optionally, calling a Pure MaxSAT problem solver to solve the local fault dictionary to obtain a simplified test vector includes: processing the local fault dictionary to obtain a WCNF file to be input into the Pure MaxSAT problem solver, wherein the WCNF file records a data structure of the local fault dictionary; inputting the WCNF file into the Pure MaxSAT problem solver for solving to obtain the simplified test vector.

Optionally, in the process of inputting the WCNF file into the Pure MaxSAT problem solver for solving, the method further includes: identifying a key vector in the WCNF file, wherein the key vector is a test vector that is uniquely capable of detecting a certain test fault; and solving the key vector as a vector that must be retained.

According to another aspect of an embodiment of the present application, a compression device for automatic circuit test vectors based on Boolean satisfiability is also provided, including: an acquisition unit, used to acquire an original test vector set and a test fault set of a target chip, wherein the original test vector set includes multiple test vectors, and the test fault set includes multiple test faults; a determination unit, used to use a first test vector subset of the original test vector set to perform fault simulation on all test faults in the test fault set, and determine a tested fault subset of the test fault set, wherein the original test vector set includes the first test vector subset and the second test vector subset, and the test fault set includes the tested fault subset and the untested fault subset, the tested fault subset is used to store tested test faults, and the untested fault subset is used to store untested test faults; a creation unit, used to use the second test vector subset and the untested fault subset to establish a local fault dictionary, wherein the local fault dictionary is used to record the association between the test vectors in the second test vector subset and the test faults in the untested fault subset; a compression unit, used to call Pure The MaxSAT problem solver solves the local fault dictionary to obtain a simplified test vector.

According to another aspect of an embodiment of the present application, a storage medium is further provided, which includes a stored program, and the above method is executed when the program is run.

According to another aspect of an embodiment of the present application, an electronic device is further provided, including a memory, a processor, and a computer program stored in the memory and executable on the processor, wherein the processor executes the above method through the computer program.

According to one aspect of the present application, a computer program product or a computer program is provided, the computer program product or the computer program comprising computer instructions, the computer instructions being stored in a computer-readable storage medium. A processor of a computer device reads the computer instructions from the computer-readable storage medium, and the processor executes the computer instructions, so that the computer device performs the steps of any one of the embodiments of the above method.

In an embodiment of the present application, an original test vector set and a test fault set of a target chip are obtained, wherein the original test vector set includes multiple test vectors, and the test fault set includes multiple test faults; a first test vector subset of the original test vector set is used to perform fault simulation on all test faults in the test fault set to determine a tested fault subset of the test fault set, wherein the original test vector set includes a first test vector subset and a second test vector subset, and the test fault set includes a tested fault subset and an untested fault subset, wherein the tested fault subset is used to store tested test faults, and the untested fault subset is used to store untested test faults; a local fault dictionary is established using the second test vector subset and the untested fault subset, wherein the local fault dictionary is used to record the association between the test vectors in the second test vector subset and the test faults in the untested fault subset; a Pure MaxSAT problem solver is called to solve the local fault dictionary to obtain a simplified test vector. In this solution, a local fault dictionary is established, and a small batch of vectors are selected for fault simulation to screen out untested faults and the remaining vectors to form a local fault dictionary, and the vector reduction of the fault dictionary is converted into a Pure MaxSAT problem; proposed a method to expand the candidate vector set, providing the "n-detect" mode in the ATPG algorithm to provide more candidate vectors for vector reduction, improving the reduction effect; proposed to introduce a dedicated solver for Pure MaxSAT problem in SAT problem into STC, and realized fast STC problem solving through efficient local search algorithm design. It can solve the technical problem that vector compression is time-consuming in related technologies.

BRIEF DESCRIPTION OF THE DRAWINGS

The drawings described herein are used to provide a further understanding of the present application and constitute a part of the present application. The illustrative embodiments of the present application and their descriptions are used to explain the present application and do not constitute an improper limitation on the present application. In the drawings:

FIG1 is a flow chart of an optional method for compressing circuit automatic test vectors based on Boolean satisfiability according to an embodiment of the present application;

FIG2 is a schematic diagram of an optional compression scheme for circuit automatic test vectors based on Boolean satisfiability according to an embodiment of the present application;

FIG3 is a schematic diagram of an optional compression scheme for circuit automatic test vectors based on Boolean satisfiability according to an embodiment of the present application;

FIG4 is a schematic diagram of an optional circuit automatic test vector compression device based on Boolean satisfiability according to an embodiment of the present application; and,

FIG5 is a structural block diagram of a terminal according to an embodiment of the present application.

DETAILED DESCRIPTION

In order to enable those skilled in the art to better understand the solution of the present application, the technical solution in the embodiments of the present application will be clearly and completely described below in conjunction with the drawings in the embodiments of the present application. Obviously, the described embodiments are only part of the embodiments of the present application, not all of the embodiments. Based on the embodiments in the present application, all other embodiments obtained by ordinary technicians in this field without creative work should fall within the scope of protection of the present application.

It should be noted that the terms "first", "second", etc. in the specification and claims of the present application and the above-mentioned drawings are used to distinguish similar objects, and are not necessarily used to describe a specific order or sequence. It should be understood that the data used in this way can be interchangeable where appropriate, so that the embodiments of the present application described herein can be implemented in an order other than those illustrated or described herein. In addition, the terms "including" and "having" and any of their variations are intended to cover non-exclusive inclusions, for example, a process, method, system, product or device comprising a series of steps or units is not necessarily limited to those steps or units clearly listed, but may include other steps or units that are not clearly listed or inherent to these processes, methods, products or devices.

In static test vector compression STC, the STC problem can be converted into a special case of Pure Maximum Satisfiability (Pure MaxSAT) in the Partial Maximum Satisfiability (Partial MaxSAT) problem by establishing a fault dictionary, that is, a record of the fault set that each test vector can detect. Partial MaxSAT requires that in a Boolean expression, the truth value assignment of variables must satisfy all hard clauses and the maximum number of soft clauses; PureMaxSAT, under the above premise, requires that all hard clauses in the Boolean expression are pure clauses with the same polarity (positive), and all soft clauses are pure clauses with opposite polarity (negative).

Building a fault dictionary and solving the Pure MaxSAT problem converted from the fault dictionary are two crucial time bottlenecks in STC. However, STC is a set of NP-Complete problems, which means that there is no algorithm that can effectively solve the problem in linear time.

For a circuit with a test vector set consisting of n test vectors and a fault set consisting of m faults, establishing a fault dictionary requires fault simulation for each vector. Simulating each fault will bring too much computational complexity in actual production applications.

To solve the above STC problem, a multi-objective test set optimization method (DPSO) based on particle swarm can be used to guide the particle swarm's heuristic algorithm to search for compressed test sets with the maximum fault detection rate, the minimum number of tests and the minimum test cost as the optimization goals. The row weighting local search method (RWLS) proposes a preprocessing step to effectively reduce the search space before the local search, and uses multiple taboo strategies to effectively avoid search repetition and loops to search for compressed test sets. In addition, there are some solution algorithms based on genetic algorithms, single-objective optimization particle swarm algorithms and dedicated set cover problem solvers.

The above-mentioned STC problem solving algorithm will greatly increase the solving time when the problem scale is too large. The time increase mainly comes from two aspects: first, it takes a lot of time to build a fault dictionary for fault simulation. Each vector needs to simulate all faults. The size of the fault set grows linearly with the growth of the circuit scale. Although the vector does not grow linearly, it will also increase, resulting in a super-linear growth in the size of the fault dictionary. Second, the increase in the size of the fault dictionary makes it very difficult to solve the STC problem. The solving time of the solver generally grows super-linearly with the linear growth of the size of the fault dictionary.

The STC effect is severely restricted by the quality of the vector. The quality of a vector is generally evaluated by the number of faults that can be detected by a vector. The more faults a vector can detect, the better the quality. However, due to the traditional ATPG algorithm (ATPG stands for Automatic Test Pattern Generation, which is the process of automatically generating test pattern vectors used in semiconductor electrical testing by a program. Test vectors are loaded sequentially onto the input pins of the device, and the output signals are collected and compared with the budgeted test vectors to determine the test results. ATPG effectiveness is an important indicator for measuring test error coverage) every time a fault is detected during execution, the fault will be discarded, and each newly generated vector is to detect faults that are not currently detected, so the vector quality is not necessarily high.

In order to efficiently realize static compression (STC) of digital circuit automatic test vectors and improve their performance, according to one aspect of the embodiment of the present application, a method embodiment of a method for compressing circuit automatic test vectors based on Boolean satisfiability is provided. By establishing a local fault dictionary, the size of the fault dictionary can be greatly reduced, thereby greatly reducing the fault simulation time required to establish the fault dictionary and the time for Pure MaxSAT problem solver to solve; by using the "n-detect" mode in the ATPG algorithm, a larger range of candidate test vectors is provided, and better vector reduction effects can be achieved.

FIG. 1 is a flow chart of an optional method for compressing circuit automatic test vectors based on Boolean satisfiability according to an embodiment of the present application. As shown in FIG. 1 , the method may include the following steps:

Step S102, obtaining an original test vector set and a test fault set of the target chip, wherein the original test vector set includes a plurality of test vectors, and the test fault set includes a plurality of test faults.

In the technical solution of the present application, when obtaining the original test vector set of the target chip, the test mode of the automatic test vector generation tool is set to the specified test mode, and the specified test mode is used to indicate the number of vectors n required for a test fault, and the value of n is 2 or 3. Then, the automatic test vector generation ATPG tool is called to generate the original test vector set for the target chip. In the automatic test program generation (ATPG) algorithm, "n-detect" is a fault detection metric used to evaluate the detection ability of the test pattern for the faults in the chip. In the technical solution of the present application, the value of n is small, and the test efficiency is higher at this time: a smaller n value means that the test pattern only needs to detect a small number of faults to meet the requirements, which can reduce the number of test patterns and test time, and improve test efficiency.

Step S104, using the first test vector subset of the original test vector set, perform fault simulation on all test faults in the test fault set to determine the tested fault subset of the test fault set, the original test vector set includes the first test vector subset and the second test vector subset, the test fault set includes a tested fault subset and an untested fault subset, the tested fault subset is used to save the tested test faults, and the untested fault subset is used to save the untested test faults.

In the technical solution of the present application, the original test vector set can be divided into a first test vector subset and a second test vector subset according to a preset ratio, and the number of test vectors in the second test vector subset is much larger than the number of test vectors in the first test vector subset. For example, the above preset ratio is 1:9; the first test vector subset is used to perform fault simulation on all test faults in the test fault set to determine the tested fault subset.

Step S106, using the second test vector subset and the untested fault subset, a local fault dictionary is established, where the local fault dictionary is used to record associations between test vectors in the second test vector subset and test faults in the untested fault subset.

In the technical solution of the present application, the test vectors in the second test vector subset are used to perform fault simulation on the test faults in the untested fault subset to obtain the relationship between each test vector and all test faults; a local fault dictionary is established using the relationship between each test vector and all test faults, each row of the local fault dictionary corresponds to a test vector or a test fault, and each column corresponds to a test fault or a test vector. The elements that intersect any row and column are used to represent the relationship between the corresponding test vector and the corresponding test fault. When the value of the element is 1, it indicates that the test vector can detect the test fault, and when the value of the element is 0, it indicates that the test vector cannot detect the test fault.

Step S108, calling the Pure MaxSAT problem solver to solve the local fault dictionary, thereby obtaining a simplified test vector.

In the technical solution of the present application, the local fault dictionary is processed to obtain a WCNF file to be input into a Pure MaxSAT problem solver, wherein the WCNF file records the data structure of the local fault dictionary; the WCNF file is input into the Pure MaxSAT problem solver for solving to obtain the simplified test vector.

In the process of inputting the WCNF file into the Pure MaxSAT problem solver for solving, identifying a key vector in the WCNF file, wherein the key vector is a test vector that is uniquely capable of detecting a certain test fault;

After the Pure MaxSAT problem solver is called to solve the local fault dictionary to obtain a reduced test vector, the reduced test vector of the second test vector subset and the first test vector subset are used as the final test vector of the target chip.

Through the above steps, the original test vector set and test fault set of the target chip are obtained, the original test vector set includes multiple test vectors, and the test fault set includes multiple test faults; the first test vector subset of the original test vector set is used to perform fault simulation on all test faults in the test fault set to determine the tested fault subset of the test fault set, the original test vector set includes the first test vector subset and the second test vector subset, the test fault set includes the tested fault subset and the untested fault subset, the tested fault subset is used to save the tested test faults, and the untested fault subset is used to save the untested test faults; the second test vector subset and the untested fault subset are used to establish a local fault dictionary, the local fault dictionary is used to record the association between the test vectors in the second test vector subset and the test faults in the untested fault subset; the Pure MaxSAT problem solver is called to solve the local fault dictionary to obtain a simplified test vector. In this scheme, a local fault dictionary is established, and a small batch of vectors are selected for fault simulation to screen out the untested faults and the remaining vectors to form a local fault dictionary, and the vector reduction of the fault dictionary is converted into Pure MaxSAT problem; proposed a method to expand the candidate vector set, providing the "n-detect" mode in the ATPG algorithm to provide more candidate vectors for vector reduction, improving the reduction effect; proposed to introduce a dedicated solver for Pure MaxSAT problem in SAT problem into STC, and realized fast STC problem solving through efficient local search algorithm design. It can solve the technical problem that vector compression is time-consuming in related technologies.

The digital circuit test vector reduction scheme based on Pure MaxSAT solver proposed in this application is based on the idea of: targeting the two bottlenecks of large-scale circuit STC problems, the time bottleneck of too many fault simulations required to establish the fault dictionary, and the bottleneck of difficulty in solving the problem caused by the large size of the fault dictionary. As an optional embodiment, the technical solution of this application is further described in detail below in combination with specific implementation methods:

The following uses the example in Figure 2 to describe the overall framework of the solution, which is mainly divided into four steps: executing the commercial DFT process (DFT stands for Design for Testability, which is a design technology and method that aims to enhance the testability of integrated circuits. It is a series of technologies and strategies used in the integrated circuit design process to ensure that the design can be effectively tested and fault detected), establishing a fault dictionary, generating CNF, and solving with a dedicated SAT solver. Figure 2 shows a schematic diagram of the entire process.

1) Execute the commercial DFT flow. The traditional ATPG algorithm running in the commercial DFT tool is generally "1-detection", which means that when a fault is detected, it is discarded and only test vectors are generated for the currently undetected faults.

The commercial DFT (Design for Testability) process is a series of technologies and methods used in the integrated circuit design process to ensure the testability and reliability of the design. The commercial DFT process usually includes the following key steps:

1.1) Test requirements analysis: At the beginning of the design phase, determine the test objectives, constraints, and requirements. This includes defining test coverage targets, fault models, test resource budgets, etc.

1.2) DFT planning: Develop test strategies and plans based on test requirements. Determine which DFT techniques and methods to use and how to apply them in the design.

1.3) Scan chain design: Scan chain is a commonly used DFT technique to simplify the loading and output of test patterns. In scan chain design, the registers in the design are converted into a scannable form so that the test pattern can enter and exit the circuit through the scan chain.

1.4) Boundary Scan Design: Boundary scan is a scanning technique used to test the input and output interfaces in a design. By adding scan chains on the input and output interfaces, the functionality and communication of these interfaces can be effectively tested.

1.5) Fault simulation and test pattern generation: Use fault simulation tools to perform fault simulation on the design to evaluate the coverage and fault detection capabilities of the test pattern. Generate test patterns based on the fault simulation results to activate and detect faults in the design.

1.6) ATPG is a technology that automatically generates test patterns. By using ATPG tools, test patterns that can detect faults in the design are automatically generated based on fault models and test requirements.

1.7) Special testing technologies: Commercial DFT processes can also include some special testing technologies, such as BIST (Built-In Self-Test), Boundary Scan, etc. These technologies can provide self-test and self-verification functions inside the chip, reducing dependence on external testing equipment.

1.8) Verification and simulation: After the design is completed, verification and simulation are performed to ensure the correctness and testability of the design under various working conditions. This includes functional verification, timing verification, and simulation of test modes, etc.

The goal of the commercial DFT process is to ensure that the design has good test coverage, high fault detection capability and reliability. By integrating test-related technologies and methods in the design process, the chip testing efficiency can be improved, the testing cost can be reduced, and the product quality and reliability can be improved.

In the context of ATPG algorithms, "n-detect" refers to a fault detection metric that measures the minimum number of test vectors required to detect each fault in a circuit. It specifies the number of vectors required to detect all faults at least n times, where n is typically set to 2 or more. For example, if set to "2-detect", this means that at least two vectors are required to detect that fault to achieve the desired fault coverage. This metric can be used to evaluate the effectiveness of a test set and optimize the number of test vectors required to achieve the desired fault coverage. In general, the "n-detect" metric will increase the number of test vectors generated by the ATPG algorithm.

Therefore, when running the ATPG algorithm in commercial DFT tools, “2-detect” and “3-detect” modes are also specified in the expectation of generating more candidate test vectors, without considering a larger “n-detect” as this will result in longer ATPG execution time and an excessive number of generated vectors.

2) Establish a fault dictionary. This solution selects 10% of the vectors generated by the commercial ATPG tool for fault simulation, discards the faults that can be detected, and obtains the retained 90% vectors and the currently undetectable faults for single-vector fault simulation. This generates a fault dictionary that records the faults that can be detected by each vector. The selected 10% vectors are directly retained without reduction.

3) WCNF generation. The dedicated SAT solver designed in this scheme is a Pure MaxSAT solver, and its input file is called WCNF (weighted conjunctive normal form). In order to describe the WCNF generation process, the following definitions and symbols are used. Let T = {T ₁ , T ₂ , ..., T _m } be a given set of test vectors, where _Ti is a single test vector and m is the count of T. The set of stuck-at faults (SAFs) is represented as F = {F ₁ , F ₂ , ..., F _n }, where F _j is a single testable fault and n is the count of F. The fault dictionary that describes the mapping between test vectors and faults can be represented as a matrix, with m rows representing test vectors and n columns representing faults. For test vector _ti and fault _fj , the value of the matrix is represented as r( _ti , _fj ). If test vector _ti (row) can detect fault _fj (column), the value of the matrix takes r( _ti , _fj ) = 1, otherwise r( _ti , _fj ) = 0.

Figure 3 shows the process of converting the fault dictionary to CNF. TestSet( _fj ) represents the set of vectors that can detect fault _fj , and _Cj represents the jth clause in WCNF, where the number of clauses is equal to the vector count plus the fault count in the fault dictionary, that is, m+n.

4) Dedicated SAT solver. This proposal designs a dedicated partial Pure MaxSAT solver that combines preprocessing to identify key vectors, aiming to accelerate the solving process. A key vector is defined as a vector that can uniquely detect a specific fault in the fault dictionary. By querying the size of TestSet(f _j ), we can identify the key vector. If the size of TestSet(f _j ) is equal to 1, it means that fault f _j can only be detected by this key vector and this vector must be retained. This information can then be used to accelerate the initial solution.

In summary, the present invention proposes a test vector static compression method based on Pure MaxSAT solver. The local fault dictionary established by single vector fault simulation can be converted into WCNF input to Pure MaxSAT solver to obtain a simplified vector set, thereby achieving the purpose of reducing test cycle and test cost. The invention was verified on the ISCAS89 and ITC99 benchmark circuits, and the results verified the effectiveness of the invention.

The present invention is verified on ISCAS89 and ITC99 benchmark circuits, and the number of vectors and test cycles before and after the test vector set is reduced are comprehensively evaluated. The results show the effectiveness of the present invention compared with the traditional heuristic strategy. The present invention can solve the STC problem faster while the program occupies less memory, and the reduction effect is not much different from that of the complete fault dictionary.

It should be noted that, for the aforementioned method embodiments, for the sake of simplicity, they are all expressed as a series of action combinations, but those skilled in the art should be aware that the present application is not limited by the described order of actions, because according to the present application, certain steps can be performed in other orders or simultaneously. Secondly, those skilled in the art should also be aware that the embodiments described in the specification are all preferred embodiments, and the actions and modules involved are not necessarily required by the present application.

Through the description of the above implementation methods, those skilled in the art can clearly understand that the method according to the above embodiment can be implemented by means of software plus a necessary general hardware platform, and of course by hardware, but in many cases the former is a better implementation method. Based on this understanding, the technical solution of the present application, or the part that contributes to the prior art, can be embodied in the form of a software product, which is stored in a storage medium (such as ROM/RAM, magnetic disk, optical disk), and includes a number of instructions for a terminal device (which can be a mobile phone, computer, server, or network device, etc.) to execute the methods described in each embodiment of the present application.

According to another aspect of the embodiment of the present application, a Boolean satisfiability-based circuit automatic test vector compression device for implementing the above-mentioned Boolean satisfiability-based circuit automatic test vector compression method is also provided. FIG4 is a schematic diagram of an optional Boolean satisfiability-based circuit automatic test vector compression device according to an embodiment of the present application. As shown in FIG4, the device may include:

An acquisition unit 41 is used to acquire an original test vector set and a test fault set of a target chip, wherein the original test vector set includes a plurality of test vectors, and the test fault set includes a plurality of test faults;

A determination unit 43 is used to perform fault simulation on all test faults in the test fault set by using the first test vector subset of the original test vector set to determine a tested fault subset of the test fault set, wherein the original test vector set includes the first test vector subset and the second test vector subset, the test fault set includes the tested fault subset and the untested fault subset, the tested fault subset is used to store the tested test faults, and the untested fault subset is used to store the untested test faults;

A creating unit 45, configured to establish a local fault dictionary using the second test vector subset and the untested fault subset, wherein the local fault dictionary is used to record associations between test vectors in the second test vector subset and test faults in the untested fault subset;

The compression unit 47 is used to call the Pure MaxSAT problem solver to solve the local fault dictionary, so as to obtain a simplified test vector.

Optionally, the determination unit is also used to: divide the original test vector set into the first test vector subset and the second test vector subset according to a preset ratio, wherein the number of test vectors in the second test vector subset is greater than the number of test vectors in the first test vector subset; use the first test vector subset to perform fault simulation on all test faults in the test fault set to determine the tested fault subset.

Optionally, the creation unit is also used to: use the test vectors in the second test vector subset to perform fault simulation on the test faults in the untested fault subset to obtain the relationship between each test vector and all test faults; use the relationship between each test vector and all test faults to establish the local fault dictionary, wherein each row of the local fault dictionary corresponds to a test vector or a test fault, and each column corresponds to a test fault or a test vector, and the elements that intersect any row and column are used to represent the relationship between the corresponding test vector and the corresponding test fault, and when the value of the element is 1, it indicates that the test vector can detect the test fault, and when the value of the element is 0, it indicates that the test vector cannot detect the test fault.

Optionally, the compression unit is further used to, after calling the Pure MaxSAT problem solver to solve the local fault dictionary to obtain a reduced test vector, use the reduced test vector of the second test vector subset and the first test vector subset as the final test vector of the target chip.

Optionally, the acquisition unit is also used to: before calling the automatic test vector generation ATPG tool to generate test vectors for the target chip, set the test mode of the automatic test vector generation tool to a specified test mode, wherein the specified test mode is used to indicate the number of vectors n required for a test fault, and the value of n is 2 or 3; and call the automatic test vector generation ATPG tool to generate the original test vector set for the target chip.

Optionally, the compression unit is also used to: process the local fault dictionary to obtain a WCNF file to be input into a PureMaxSAT problem solver, wherein the WCNF file records a data structure of the local fault dictionary; input the WCNF file into the Pure MaxSAT problem solver for solving, to obtain the simplified test vector.

Optionally, the compression unit is also used to: during the process of inputting the WCNF file into the Pure MaxSAT problem solver for solving, identify the key vector in the WCNF file, wherein the key vector is the only test vector that can detect a certain test fault; and solve the key vector as a vector that must be retained.

Through the above module, the original test vector set and test fault set of the target chip are obtained, wherein the original test vector set includes multiple test vectors, and the test fault set includes multiple test faults; using the first test vector subset of the original test vector set, all test faults in the test fault set are subjected to fault simulation to determine the tested fault subset of the test fault set, wherein the original test vector set includes the first test vector subset and the second test vector subset, and the test fault set includes the tested fault subset and the untested fault subset, wherein the tested fault subset is used to store the tested test faults, and the untested fault subset is used to store the untested test faults; using the second test vector subset and the untested fault subset, a local fault dictionary is established, wherein the local fault dictionary is used to record the association between the test vectors in the second test vector subset and the test faults in the untested fault subset; calling Pure The MaxSAT problem solver solves the local fault dictionary to obtain a simplified test vector. In this solution, a local fault dictionary is established, and by selecting a small batch of vectors for fault simulation, untested faults and the remaining vectors are screened out to form a local fault dictionary, and the vector simplification of the fault dictionary is converted into a Pure MaxSAT problem; a method for expanding the candidate vector set is proposed, and the "n-detect" mode in the ATPG algorithm is provided to provide more candidate vectors for vector simplification, thereby improving the simplification effect; it is proposed to introduce a special solver for solving Pure MaxSAT problems in the SAT problem into STC, and realize fast STC problem solving through efficient local search algorithm design. The technical problem that vector compression is relatively time-consuming in related technologies can be solved.

It should be noted that the examples and application scenarios implemented by the above modules and corresponding steps are the same, but are not limited to the contents disclosed in the above embodiments. It should be noted that the above modules, as part of the device, can be run in a corresponding hardware environment, can be implemented by software, and can also be implemented by hardware, wherein the hardware environment includes a network environment.

According to another aspect of an embodiment of the present application, a server or terminal is provided for implementing the above-mentioned method for compressing automatic circuit test vectors based on Boolean satisfiability.

Figure 5 is a structural block diagram of a terminal according to an embodiment of the present application. As shown in Figure 5, the terminal may include: one or more (only one is shown in the figure) processors 501, a memory 503, and a transmission device 505. As shown in Figure 5, the terminal may also include an input and output device 507.

Among them, the memory 503 can be used to store software programs and modules, such as the program instructions/modules corresponding to the compression method and device of the circuit automatic test vector based on Boolean satisfiability in the embodiment of the present application. The processor 501 executes various functional applications and data processing by running the software programs and modules stored in the memory 503, that is, the compression method of the circuit automatic test vector based on Boolean satisfiability is realized. The memory 503 may include a high-speed random access memory, and may also include a non-volatile memory, such as one or more magnetic storage devices, flash memory, or other non-volatile solid-state memory. In some instances, the memory 503 may further include a memory remotely arranged relative to the processor 501, and these remote memories can be connected to the terminal via a network. Examples of the above-mentioned network include, but are not limited to, the Internet, an intranet, a local area network, a mobile communication network, and a combination thereof.

The above-mentioned transmission device 505 is used to receive or send data via a network, and can also be used for data transmission between a processor and a memory. The above-mentioned network specific examples may include wired networks and wireless networks. In one example, the transmission device 505 includes a network adapter (Network Interface Controller, NIC), which can be connected to other network devices and routers via a network cable so as to communicate with the Internet or a local area network. In one example, the transmission device 505 is a radio frequency (Radio Frequency, RF) module, which is used to communicate with the Internet wirelessly.

Specifically, the memory 503 is used to store application programs.

The processor 501 may call the application stored in the memory 503 through the transmission device 505 to perform the following steps:

Acquire an original test vector set and a test fault set of a target chip, wherein the original test vector set includes a plurality of test vectors, and the test fault set includes a plurality of test faults;

Utilizing the first test vector subset of the original test vector set, performing fault simulation on all test faults in the test fault set, and determining a tested fault subset of the test fault set, wherein the original test vector set includes the first test vector subset and the second test vector subset, the test fault set includes the tested fault subset and the untested fault subset, the tested fault subset is used to store the tested test faults, and the untested fault subset is used to store the untested test faults;

Using the second test vector subset and the untested fault subset, a local fault dictionary is established, wherein the local fault dictionary is used to record associations between test vectors in the second test vector subset and test faults in the untested fault subset;

The Pure MaxSAT problem solver is called to solve the local fault dictionary, thereby obtaining a simplified test vector.

Optionally, the specific examples in this embodiment may refer to the examples described in the above embodiments, and this embodiment will not be described in detail here.

It can be understood by those skilled in the art that the structure shown in FIG5 is for illustration only, and the terminal may be a smart phone (such as an Android phone, an iOS phone, etc.), a tablet computer, a PDA, a mobile Internet device (MID), a PAD, and other terminal devices. FIG5 does not limit the structure of the above electronic devices. For example, the terminal may also include more or fewer components (such as a network interface, a display device, etc.) than those shown in FIG5, or have a configuration different from that shown in FIG5.

A person of ordinary skill in the art can understand that all or part of the steps in the various methods of the above embodiments can be completed by instructing the hardware related to the terminal device through a program, and the program can be stored in a computer-readable storage medium, and the storage medium may include: a flash drive, a read-only memory (ROM), a random access memory (RAM), a magnetic disk or an optical disk, etc.

The embodiment of the present application further provides a storage medium. Optionally, in this embodiment, the storage medium can be used to execute the program code of the method for compressing circuit automatic test vectors based on Boolean satisfiability.

Optionally, in this embodiment, the storage medium may be located on at least one network device among a plurality of network devices in the network shown in the above embodiment.

Optionally, in this embodiment, the storage medium is configured to store program codes for executing the following steps:

Acquire an original test vector set and a test fault set of a target chip, wherein the original test vector set includes a plurality of test vectors, and the test fault set includes a plurality of test faults;

Utilizing the first test vector subset of the original test vector set, performing fault simulation on all test faults in the test fault set, and determining a tested fault subset of the test fault set, wherein the original test vector set includes the first test vector subset and the second test vector subset, the test fault set includes the tested fault subset and the untested fault subset, the tested fault subset is used to store the tested test faults, and the untested fault subset is used to store the untested test faults;

Using the second test vector subset and the untested fault subset, a local fault dictionary is established, wherein the local fault dictionary is used to record associations between test vectors in the second test vector subset and test faults in the untested fault subset;

The Pure MaxSAT problem solver is called to solve the local fault dictionary, thereby obtaining a simplified test vector.

Optionally, the specific examples in this embodiment may refer to the examples described in the above embodiments, and this embodiment will not be described in detail here.

Optionally, in this embodiment, the above-mentioned storage medium may include but is not limited to: a USB flash drive, a read-only memory (ROM), a random access memory (RAM), a mobile hard disk, a magnetic disk or an optical disk, and other media that can store program codes.

The serial numbers of the above-mentioned embodiments of the present application are for description only and do not represent the advantages or disadvantages of the embodiments.

If the integrated units in the above embodiments are implemented in the form of software functional units and sold or used as independent products, they can be stored in the above computer-readable storage medium. Based on this understanding, the technical solution of the present application, or the part that contributes to the prior art, or all or part of the technical solution can be embodied in the form of a software product, which is stored in a storage medium and includes several instructions for enabling one or more computer devices (which may be personal computers, servers, or network devices, etc.) to execute all or part of the steps of the methods described in the various embodiments of the present application.

In the above embodiments of the present application, the description of each embodiment has its own emphasis. For parts that are not described in detail in a certain embodiment, please refer to the relevant description of other embodiments.

In the several embodiments provided in the present application, it should be understood that the disclosed client can be implemented in other ways. Among them, the device embodiments described above are only schematic. For example, the division of the units is only a logical function division. There may be other division methods in actual implementation. For example, multiple units or components can be combined or integrated into another system, or some features can be ignored or not executed. Another point is that the mutual coupling or direct coupling or communication connection shown or discussed can be through some interfaces, indirect coupling or communication connection of units or modules, which can be electrical or other forms.

The units described as separate components may or may not be physically separated, and the components shown as units may or may not be physical units, that is, they may be located in one place or distributed on multiple network units. Some or all of the units may be selected according to actual needs to achieve the purpose of the solution of this embodiment.

In addition, each functional unit in each embodiment of the present application may be integrated into one processing unit, or each unit may exist physically separately, or two or more units may be integrated into one unit. The above-mentioned integrated unit may be implemented in the form of hardware or in the form of software functional units.

The above is only a preferred implementation of the present application. It should be pointed out that for ordinary technicians in this technical field, several improvements and modifications can be made without departing from the principles of the present application. These improvements and modifications should also be regarded as the scope of protection of the present application.

Claims (9)

1. A method for compressing circuit automatic test vectors based on Boolean satisfiability, characterized by comprising: Acquire an original test vector set and a test fault set of a target chip, wherein the original test vector set includes a plurality of test vectors, and the test fault set includes a plurality of test faults; Utilizing the first test vector subset of the original test vector set, performing fault simulation on all test faults in the test fault set, and determining a tested fault subset of the test fault set, wherein the original test vector set includes the first test vector subset and the second test vector subset, the test fault set includes the tested fault subset and the untested fault subset, the tested fault subset is used to store the tested test faults, and the untested fault subset is used to store the untested test faults; Using the second test vector subset and the untested fault subset, a local fault dictionary is established, including: using the test vectors in the second test vector subset to perform fault simulation on the test faults in the untested fault subset to obtain the relationship between each test vector and all the test faults in the untested fault subset; using the relationship between each test vector and all the test faults in the untested fault subset to establish the local fault dictionary, wherein each row of the local fault dictionary corresponds to a test vector or a test fault, and each column corresponds to a test fault or a test vector, and an element at the intersection of any row and a column is used to represent the relationship between the corresponding test vector and the corresponding test fault, and when the value of the element is 1, it indicates that the test vector can detect the test fault, and when the value of the element is 0, it indicates that the test vector cannot detect the test fault, wherein the local fault dictionary is used to record the association between the test vector in the second test vector subset and the test fault in the untested fault subset; The Pure MaxSAT problem solver is called to solve the local fault dictionary, thereby obtaining a simplified test vector. 2. The method according to claim 1, characterized in that the method comprises: using the first test vector subset of the original test vector set to perform fault simulation on all test faults in the test fault set to determine the tested fault subset of the test fault set, comprising: Dividing the original test vector set into the first test vector subset and the second test vector subset according to a preset ratio, wherein the number of test vectors in the second test vector subset is greater than the number of test vectors in the first test vector subset; Fault simulation is performed on all test faults in the test fault set using the first test vector subset to determine the tested fault subset. 3. The method according to claim 1, characterized in that obtaining the original test vector set of the target chip comprises: Before calling the automatic test vector generation ATPG tool to generate test vectors for the target chip, setting the test mode of the automatic test vector generation ATPG tool to a specified test mode, wherein the specified test mode is used to indicate the number of vectors n required for a test fault, and the value of n is 2 or 3; The automatic test vector generation ATPG tool is called to generate the original test vector set for the target chip. 4. The method according to claim 1, characterized in that calling a Pure MaxSAT problem solver to solve the local fault dictionary to obtain a simplified test vector comprises: Processing the local fault dictionary to obtain a WCNF file to be input into a Pure MaxSAT problem solver, wherein the WCNF file records a data structure of the local fault dictionary; The WCNF file is input into the Pure MaxSAT problem solver for solving to obtain the simplified test vector. 5. The method according to claim 4, characterized in that, in the process of inputting the WCNF file into the Pure MaxSAT problem solver for solving, the method further comprises: Identifying a key vector in the WCNF file, wherein the key vector is a test vector that is uniquely capable of detecting a certain test fault; The key vector is taken as a vector that must be retained for solving. 6. The method according to any one of claims 1 to 5, characterized in that after calling the Pure MaxSAT problem solver to solve the local fault dictionary to obtain a reduced test vector, the method further comprises: The obtained simplified test vectors of the second test vector subset and the first test vector subset are used as final test vectors of the target chip. 7. A circuit automatic test vector compression device based on Boolean satisfiability, characterized by comprising: An acquisition unit, used to acquire an original test vector set and a test fault set of a target chip, wherein the original test vector set includes a plurality of test vectors, and the test fault set includes a plurality of test faults; a determination unit, configured to perform fault simulation on all test faults in the test fault set by using the first test vector subset of the original test vector set, and determine a tested fault subset of the test fault set, wherein the original test vector set includes the first test vector subset and the second test vector subset, the test fault set includes the tested fault subset and the untested fault subset, the tested fault subset is used to store the tested test faults, and the untested fault subset is used to store the untested test faults; A creation unit, used to establish a local fault dictionary using the second test vector subset and the untested fault subset, including: using the test vectors in the second test vector subset to perform fault simulation on the test faults in the untested fault subset to obtain the relationship between each test vector and all the test faults in the untested fault subset; establishing the local fault dictionary using the relationship between each test vector and all the test faults in the untested fault subset, wherein each row of the local fault dictionary corresponds to a test vector or a test fault, and each column corresponds to a test fault or a test vector, and an element at the intersection of any row and a column is used to represent the relationship between the corresponding test vector and the corresponding test fault, and when the value of the element is 1, it indicates that the test vector can detect the test fault, and when the value of the element is 0, it indicates that the test vector cannot detect the test fault, wherein the local fault dictionary is used to record the association between the test vector in the second test vector subset and the test fault in the untested fault subset; The compression unit is used to call the Pure MaxSAT problem solver to solve the local fault dictionary, so as to obtain a simplified test vector. 8. A storage medium, characterized in that the storage medium comprises a stored program, wherein the program executes the method described in any one of claims 1 to 6 when running. 9. An electronic device comprising a memory, a processor, and a computer program stored in the memory and executable on the processor, wherein the processor executes the method described in any one of claims 1 to 6 through the computer program.