DETAILED ACTION
A summary of this action:
Claims 1-20 have been presented for examination.
This action is non-Final.
Notice of Pre-AIA or AIA Status
The present application, filed on or after March 16, 2013, is being examined under the first inventor to file provisions of the AIA .
Claim Rejections - 35 USC § 101
35 U.S.C. 101 reads as follows:
Whoever invents or discovers any new and useful process, machine, manufacture, or composition of matter, or any new and useful improvement thereof, may obtain a patent therefor, subject to the conditions and requirements of this title.
Claims 1-20 are rejected under 35 U.S.C. 101 because the claimed invention is directed to an abstract idea of a mental process or mathematical concept without significantly more.
Step 1: Claims 1-6 are directed to a method, which is a process and is a statutory category invention. Claims 7-13 are directed to a device, which is a system and is a statutory invention. Claims 14-20 are direction to a non-transitory computer readable medium, which is a manufacture and a statutory invention. Therefore, claims 1-20 are directed to patent eligible categories of invention.
Claim 1
Step 2A, Prong 1: Independent claims 7 and 14, as drafted, are a process that, under its broadest reasonable interpretation, cover performance of the limitation in the mind but for the recitation of generic computer components. That is, other than reciting “processing device,” “non-transitory memory storage,” “memory storage,” “ one or more processors,” and “non-transitory computer-readable medium,” nothing in the claim element precludes the step from practically being performed in the mind.
Independent claims 1, 7, and 11 similarly recite generating a plurality of instructions to transition the at least one resource from an existing state to the at least one target state value, which is an abstract idea and covers mental processes of verifying the function of a test model before generating a plurality of instructions, as described in [0005] of the specification, because the claims are derived from Mental Processes based on concepts performed in the human mind or with the aid of pencil and paper.
Independent claim 1 recites redesigning the model based on whether the state information was successfully changed, which is an abstract idea and covers mental processes of verifying the function of a test model before redesigning the model based on whether the state information was successfully changed, as described in [0005] of the specification, because the claims are derived from Mental Processes based on concepts performed in the human mind or with the aid of pencil and paper.
Independent claims 1, 7, and 11 similarly recite generating a plurality of instructions to transition the at least one resource from an existing state to the at least one target state value, which is an abstract idea and covers mental processes of verifying the function of a test model before generating a plurality of instructions, as described in [0005] of the specification, because the claims are derived from Mental Processes based on concepts performed in the human mind or with the aid of pencil and paper.
Thus, the claims recite the abstract idea of a mental process performed in the human mind, or with the aid of pencil and paper.
Dependent claims 2-6, 8-13, and 14-20 further narrow the abstract ideas, identified in the independent claims. See analysis below.
Step 2A, Prong 2: The judicial exception is not integrated into a practical application. Independent claim 7 and dependent claims 8-13 recite the additional limitation “processing device,” independent claim 7 recites the additional limitation “memory storage,” independent claim 7 recites the additional limitation “non-transitory memory storage,” dependent claim 9 recites the additional limitation “system memory,” independent claim 14 and dependent claims 15-20 recite the additional limitation “non-transitory computer-readable medium,” and independent claim 14 and dependent claim 15 recite the additional limitation of “one or more processors,” this limitation does not integrate the judicial exception into a practical application because it is nothing more than generally linking the use of the judicial exception to a particular technological environment. See MPEP 2106.05(h). Alternatively, this additional element merely uses a computer device as a tool to perform the abstract idea. (MPEP 2106.05(f)).
The additional recited claims 1, 7, and 14 similarly recite receiving a test sequence including a specification of at least one target state value for at least one resource of a model of the integrated circuit, the specification including a state object including at least one state element defining the target state value for the resource, are mere instructions to implement an abstract idea using a computer in its ordinary capacity, or merely uses the computer as a tool to perform the identified abstract idea. See MPEP (2106.05(f)) use of a computer or other machinery in its ordinary capacity for economic or other tasks (e.g., to receive, store, or transmit data) or simply adding a general purpose computer or computer components after the fact to an abstract idea (e.g., a mental process) does not integrate a judicial exception into a practical application. (MPEP 2106.05(f)(2)).
The additional recited claims 1, 7, and 14 similarly recite executing the instructions according to the test sequence to transition the at least one resource in the model to the defined state, are mere instructions to implement an abstract idea using a computer in its ordinary capacity, or merely uses the computer as a tool to perform the identified abstract idea. See MPEP (2106.05(f)) use of a computer or other machinery in its ordinary capacity for economic or other tasks (e.g., to receive, store, or transmit data) or simply adding a general purpose computer or computer components after the fact to an abstract idea (e.g., a mental process) does not integrate a judicial exception into a practical application. (MPEP 2106.05(f)(2)).
The additional recited claims 1, 7, and 14 similarly recite after executing the instructions, outputting state information on the hardware design model to determine whether the target state value for the resource was successfully changed, can be viewed as is insignificant extra-solution activity, specifically pertaining to mere data gathering/output necessary to perform the abstract idea (MPEP 2106.05(g)) and is not sufficient to integrate the judicial exception into a practical application. This is akin to selecting information, based on types of information and availability of information in a power-grid environment, for collection, analysis and display, which has been identified as extra solution activity. Therefore, the judicial exception is not integrated into a practical application.
The additional recited claims 6 and 20 similarly recite maintaining a mapping between each of a computer implemented execution thread and an execution thread executing the test model, are mere instructions to implement an abstract idea using a computer in its ordinary capacity, or merely uses the computer as a tool to perform the identified abstract idea. See MPEP (2106.05(f)) use of a computer or other machinery in its ordinary capacity for economic or other tasks (e.g., to receive, store, or transmit data) or simply adding a general purpose computer or computer components after the fact to an abstract idea (e.g., a mental process) does not integrate a judicial exception into a practical application. (MPEP 2106.05(f)(2)).
Dependent claims 2-6, 8-13, and 15-20 further narrow the abstract ideas, identified in the independent claims, and do not introduce further additional elements for consideration beyond those addressed above. The additional elements have been considered both individually and as an ordered combination in to determine whether they integrate the exception into a practical application. Therefore, the dependent claims do not integrate the claimed invention into a practical application.
Step 2B:
The claims do not amount to significantly more. The judicial exception does not amount to significantly more. Independent claim 7 and dependent claims 8-13 recite the additional limitation “processing device,” independent claim 7 recites the additional limitation “memory storage,” independent claim 7 recites the additional limitation “non-transitory memory storage,” dependent claim 9 recites the additional limitation “system memory,” independent claim 14 and dependent claims 15-20 recite the additional limitation “non-transitory computer-readable medium,” and independent claim 14 and dependent claim 15 recite the additional limitation of “one or more processors,” this limitation does not amount to significantly more because it is nothing more than generally linking the use of the judicial exception to a particular technological environment. See MPEP 2106.05(h). Alternatively, this additional element merely uses a computer device as a tool to perform the abstract idea. (MPEP 2106.05(f)).
The additional recited claims 1, 7, and 14 similarly recite receiving a test sequence including a specification of at least one target state value for at least one resource of a model of the integrated circuit, the specification including a state object including at least one state element defining the target state value for the resource, are mere instructions to implement an abstract idea using a computer in its ordinary capacity, or merely uses the computer as a tool to perform the identified abstract idea. See MPEP (2106.05(f)) use of a computer or other machinery in its ordinary capacity for economic or other tasks (e.g., to receive, store, or transmit data) or simply adding a general purpose computer or computer components after the fact to an abstract idea (e.g., a mental process) does not amount to significantly more. (MPEP 2106.05(f)(2)).
The additional recited claims 1, 7, and 14 similarly recite executing the instructions according to the test sequence to transition the at least one resource in the model to the defined state, are mere instructions to implement an abstract idea using a computer in its ordinary capacity, or merely uses the computer as a tool to perform the identified abstract idea. See MPEP (2106.05(f)) use of a computer or other machinery in its ordinary capacity for economic or other tasks (e.g., to receive, store, or transmit data) or simply adding a general purpose computer or computer components after the fact to an abstract idea (e.g., a mental process) does not amount to significantly more. (MPEP 2106.05(f)(2)).
The additional recited claims 1, 7, and 14 similarly recite after executing the instructions, outputting state information on the hardware design model to determine whether the target state value for the resource was successfully changed, can be viewed as is insignificant extra-solution activity, specifically pertaining to mere data gathering/output necessary to perform the abstract idea (MPEP 2106.05(g)) and does not amount to significantly more. This is akin to selecting information, based on types of information and availability of information in a power-grid environment, for collection, analysis and display, which has been identified as extra solution activity. Therefore, the judicial exception does not amount to significantly more.
The additional recited claims 6 and 20 similarly recite maintaining a mapping between each of a computer implemented execution thread and an execution thread executing the test model, are mere instructions to implement an abstract idea using a computer in its ordinary capacity, or merely uses the computer as a tool to perform the identified abstract idea. See MPEP (2106.05(f)) use of a computer or other machinery in its ordinary capacity for economic or other tasks (e.g., to receive, store, or transmit data) or simply adding a general purpose computer or computer components after the fact to an abstract idea (e.g., a mental process) does not amount to significantly more. (MPEP 2106.05(f)(2)).
Dependent claims 2-6, 8-13, and 15-20 further narrow the abstract ideas, identified in the independent claims, and do not introduce further additional elements for consideration beyond those addressed above. The additional elements have been considered both individually and as an ordered combination in to determine whether they amount to significantly more. Therefore, the dependent claims does not amount to significantly more.
Therefore, the claims as a whole does not include additional elements that are sufficient to amount to significantly more than the judicial exception because the additional elements, when considered alone or in combination, do not amount to significantly more than the judicial exception.
As stated in Section I.B. of the December 16, 2014 101 Examination Guidelines, “[t]o be patent-eligible, a claim that is directed to a judicial exception must include additional features to ensure that the claim describes a process or product that applies the exception in a meaningful way, such that it is more than a drafting effort designed to monopolize the exception.”
The dependent claims include the same abstract ideas recited as recited in the independent claims, and merely incorporate additional details that narrow the abstract ideas and fail to add significantly more to the claims.
Dependent claims 2, 8, and 15 similarly recite “wherein the test sequence is defined in source code script and further including instantiating the state object to call a method to perform the generating,” which further narrows the abstract idea identified in the independent claim, which is directed to a “Mental Process.”
Dependent claim 3, 11, and 17 similarly recite “wherein the test sequence includes a default processing order for the state elements comprising an order the state elements are defined in the source code script,” which further narrows the abstract idea identified in the independent claim, which is directed to a “Mental Process.”
Dependent claim 4, 12, and 18 similarly recite “wherein the script defines a test sequence which defines a processing order for the state elements by grouping similar state elements,” which further narrows the abstract idea identified in the independent claim, which is directed to a “Mental Process.”
Dependent claim 5, 13, and 19 similarly recite “wherein the source code defines instruction sequences for more than one execution thread,” which further narrows the abstract idea identified in the independent claim, which is directed to a “Mental Process.”
Dependent claim 9 recites “wherein the resources comprise at least one of: general purpose registers (GPRs), floating point registers (FPRs), system registers, and system memory, and each state element defines a value of the resource after the state transition,” which further narrows the abstract idea identified in the independent claim, which is directed to a “Mental Process.”
Dependent claim 10 and 16 similarly recite “wherein the test sequence defines a processing order for the state elements,” which further narrows the abstract idea identified in the independent claim, which is directed to a “Mental Process.”
Claim Rejections - 35 USC § 103
In the event the determination of the status of the application as subject to AIA 35 U.S.C. 102 and 103 (or as subject to pre-AIA 35 U.S.C. 102 and 103) is incorrect, any correction of the statutory basis (i.e., changing from AIA to pre-AIA ) for the rejection will not be considered a new ground of rejection if the prior art relied upon, and the rationale supporting the rejection, would be the same under either status.
The following is a quotation of 35 U.S.C. 103 which forms the basis for all obviousness rejections set forth in this Office action:
A patent for a claimed invention may not be obtained, notwithstanding that the claimed invention is not identically disclosed as set forth in section 102, if the differences between the claimed invention and the prior art are such that the claimed invention as a whole would have been obvious before the effective filing date of the claimed invention to a person having ordinary skill in the art to which the claimed invention pertains. Patentability shall not be negated by the manner in which the invention was made.
The factual inquiries for establishing a background for determining obviousness under 35 U.S.C. 103 are summarized as follows:
1. Determining the scope and contents of the prior art.
2. Ascertaining the differences between the prior art and the claims at issue.
3. Resolving the level of ordinary skill in the pertinent art.
4. Considering objective evidence present in the application indicating obviousness or nonobviousness.
Claims 1-4, 7-8, 10-12, and 14-18 are rejected under are rejected under 35 U.S.C. 103 as being unpatentable over ZHOU (Functional Test Generation for Hard-to-Reach States Using Path Constraint Solving), herein ZHOU, and in view of MCFARLAND (Formal Verification of Sequential Hardware: A Tutorial), herein MCFARLAND.
Claim 1 is rejected because ZHOU teaches a computer implemented method of determining the operability of an integrated circuit ZHOU ([Abstract] “In this paper, we present a path constraint solving-based test generation method (PACOST) which operates in an abstraction-guided semiformal verification framework to cover hard-to-reach states. PACOST combines concrete simulation and symbolic simulation on the design under verification for path constraint extraction and mutation (PACOST is considered a computer-implemented method for determining the operability of an integrated circuit specifically used in the functional verification phase to generate test vectors that drive an IC design to hard-to-reach), and uses a sequential path constraint extractor to generate a set of valid input vectors for exploring different simulation paths with different next states. It then works on a target state-oriented abstract model to select the next state with the smallest abstract distance. In addition, the value of register variables in control logic can be controlled by analyzing the data dependence between variables, which helps the simulation converge to the target states. Experimental results show that PACOST can generate shorter traces reaching hard-to-reach states, in comparison with previous abstraction-guided semiformal methods.”)
ZHOU also teaches receiving a test sequence including a specification of at least one target state value for at least one resource of a model of the integrated circuit ZHOU ([Section D. Trace Sequence Controller | pdf page 7 of 14] “Table I shows the test generation process of PACOST for the target state F in the example given in Fig. 4. In the table, the new three-cycle stimuli are generated by solving the new constraint with the SMT solver. Simulation with the new stimuli from the current state will lead to a new sequential path, and a set of visited states along the path are obtained. Using abstract distance information in Fig. 5(b) to evaluate the visited states and the most excellent one (with the smallest abstract distance) is added to the list of candidate next states. At each simulation step, the abstract distance information is also used to evaluate the candidate next states and the one with the smallest abstract distance is selected as the next start state. Finally, we get the traversed state sequence A-B-D-E-F with generated tests {0001, 0010, 1001, 0011, 0000}.”) See also ZHOU ([Table 1], [Figure 2], [Figure 4], and [Figure 5].) See also ZHOU ([Section A. Motivation of Our Approach| pdf page 2 of 13] “In addition, invalid test vectors may be generated. Zhang et al. [7] applied an instruction set-based Markov model that integrates vector correlations to generate input vectors for microprocessor verification. The performance of historical instruction sequences is utilized to guide test sequence generation. The scope of application is limited to processors since the Markov model is built according to the instruction set architecture. The work in [8] uses the steady-state probabilities that calculated from the abstract model to guide the concrete simulation.”)
PNG
media_image1.png
613
585
media_image1.png
Greyscale
ZHOU Figure 4 Reference
PNG
media_image2.png
531
595
media_image2.png
Greyscale
ZHOU Figure 5 Reference
PNG
media_image3.png
645
642
media_image3.png
Greyscale
ZHOU Table 1 Reference
ZHOU also teaches the specification including a state object including at least one state element defining the target state value for the resource ZHOU ([Section D. Trace Sequence Controller | pdf page 6 of 13] “The test generation process of PACOST for the target state F in the example given in Fig. 4 is as follows. We unroll the RTL design for a depth of three, that is to say, we will simulate for three cycles in each simulation step. The index i for ina[i] is the annotation corresponding to the cycle number. The initial state of the design is assumed to be state = 0. The value… “Since it does not extract the data dependence between f and ina, and it cannot invert the constraint defined by the register variable f. In contrast, PACOST with multicycle path constraint extraction can control the value of f via data dependence analysis. It can jump out of the loop immediately and promote the search process.”) See also ZHOU ([Abstract] “Test generation for hard-to-reach states is important in functional verification. In this paper, we present a path constraint solving-based test generation method (PACOST) which operates in an abstraction-guided semiformal verification framework to cover hard-to-reach states. PACOST combines concrete simulation and symbolic simulation on the design under verification for path constraint extraction and mutation, and uses a sequential path constraint extractor to generate a set of valid input vectors for exploring different simulation paths with different next states. It then works on a target state-oriented abstract model to select the next state with the smallest abstract distance. In addition, the value of register variables in control logic can be controlled by analyzing the data dependence between variables, which helps the simulation converge to the target states. Experimental results show that PACOST can generate shorter traces reaching hard-to-reach states, in comparison with previous abstraction-guided semiformal methods.”)
ZHOU also teaches generating a plurality of instructions to transition the at least one resource from an existing state to the at least one target state value ZHOU ([Section A. Motivation of Our Approach] “Zhang et al. [7] applied an instruction set-based Markov model that integrates vector correlations to generate input vectors for microprocessor verification. The performance of historical (from an existing state) instruction sequences (generating a plurality of instructions) is utilized to guide (to transition) test sequence (at least one resource) generation. The scope of application is limited to processors since the Markov model is built according to the instruction set architecture. The work in [8] uses the steady-state probabilities that calculated from the abstract model to guide the concrete simulation (to the at least one target state value).”)
ZHOU also teaches executing the instructions according to the test sequence to transition the at least one resource in the model to the defined state ZHOU ([Section III. Framework of PACOST | pdf pages 2-3] “The framework of PACOST (model) is shown in Fig. 2. It accepts (executing the instructions) the RTL description (at least one resource in the model) of the DUV and the target state as inputs. Its output is a sequence (executing the instructions) of input vectors (according to the test sequence) directing (transition) to the target state (defined state).”)
PNG
media_image4.png
561
517
media_image4.png
Greyscale
ZHOU Figure 2 Reference
ZHOU also teaches after executing the instructions, outputting state information on the hardware design model to determine whether the target state value for the resource was successfully changed; ZHOU ([Section III. Framework of PACOST | pdf page 3 of 13] “The abstraction process on a DDG is demonstrated in Fig. 3. The abstract model is extracted from the target state variables (targets) backward in the DDG. The control registers in the fan-in cones of the targets in the DDG are considered to be added into the abstract model by a breadth-first algorithm. While the registers in the data flow-related logic (such as operands and outputs of a floating point unit) are added as the output or input signals of the abstract model. The combinational logic between the selected registers is also added. After building the abstract model, the abstract distances from the target state are calculated on this model by verification interacting with synthesis (VIS) [16]. Note if the scale of the abstract model exceeds the capability of VIS, control registers which are farther away from the targets in the DDG will have a higher priority to be removed to meet the capability of the formal tool.
ZHOU does not explicitly teach redesigning the model based on whether the state information was successfully changed.
However, MCFARLAND teaches redesigning the model based on whether the state information was successfully changed MCFARLAND ([Section 2.4 Extensions to the Basic Method | pdf page 9 of 22] “The proofs in our example seem quite simple, and in the end they are. Yet even these proofs embody several important insights about the hardware being verified. For example, the proof that ready (t + 9) is asserted does not work unless we can assume - start(t + i) for i from 1 to 8. This shows that in using the circuit as designed, we would have to ensure that start was asserted once at the beginning of the conversion cycle and locked out the rest of the time. If this could not be guaranteed, we would have to redesign the circuit to insulate it from the start line after the initial signal was detected. The verification also helps to establish the correct boundary conditions for the shift-and-count loop. It shows that, given the timing model used, eight must be loaded into the counter initially rather than seven or nine, and the parallel output is available on the ninth cycle rather than the eighth. The reason the proofs seem so simple is that we got the specification and design right.”)
It would have been obvious to one of ordinary skill in the art, before the effective filing date, to combine the teachings of MCFARLAND with ZHOU, as the references relates to the field of verification of semiconductor integrated circuit hardware designs. MCFARLAND would modify ZHOU wherein redesigning the model based on whether the state information was successfully changed. The benefits of doing removes the need to make everything an explicit function of time, in some cases leading to simpler specifications of sequential behavior and also makes it unnecessary to use second-order logic, which can result in a simpler, more efficient proof system. (MCFARLAND [Section IV. | Temporal Logic | pdf page 10 of 22]). Accordingly, claim 1 is rejected based on the combination of these references.
Claim 7
Claim 7 is rejected because it is the system embodiment of claim 1, with similar limitations to claim 1, and is such rejected using the same reasoning found in claim 1.
Claim 14
Claim 7 is rejected because it is the non-transitory computer-readable medium embodiment of claim 1, with similar limitations to claim 1, and is such rejected using the same reasoning found in claim 1.
Claim 2
Claim 2 is rejected because the combination of ZHOIU and MCFARLAND teaches the claim 1 limitations.
ZHOU teaches wherein the test sequence is defined in source code script and further including instantiating the state object to call a method to perform the generating ZHOU ([Section A. Abstraction Engine | pdf page 4 of 13] “1) Construction of CFG and DFUD Chains: The source code of the DUV is instrumented with additional counters which act as a communication channel between the concrete and symbolic simulations. To assist the path constraint extraction, the CFG of the DUV is built. Meanwhile, the data flow graph (DFG) of the DUV, representing as DFUD chains, is built based on the CFG to obtain the data dependence between variables. The CFG is extracted from the Verilog RTL model of the DUV. Each node of the CFG corresponds to a single statement or conditional expression in the design. The design with additional counters and its corresponding CFG for the example given in Fig. 4(a) are shown in Fig. 6. Each branch node is followed by an additional counter (ik <= ik + 1), which has been underlined in Fig. 6(a). Their values are monitored during simulation to record the concrete paths.”) See also ZHOU ([Figure 4].) Accordingly, claim 2 is rejected based on the combination of these references.
PNG
media_image5.png
487
481
media_image5.png
Greyscale
ZHOU Figure 4 Reference
Claim 8
Claim 8 is rejected because it is the system embodiment of claim 2, with similar limitations to claim 2, and is such rejected using the same reasoning found in claim 2.
Claim 15
Claim 15 is rejected because it is the non-transitory computer-readable medium embodiment of claim 2, with similar limitations to claim 2, and is such rejected using the same reasoning found in claim 2.
Claim 3
Claim 3 is rejected because the combination of ZHOU and MCFARLAND teach the claim 2 limitations.
ZHOU does not explicitly teach wherein the test sequence includes a default processing order for the state elements comprising an order the state elements are defined in the source code script.
However, MCFARLAND teaches wherein the test sequence includes a default processing order for the state elements comprising an order the state elements are defined in the source code script MACFARLAND ([Section III. Higher Order Logic | pdf page 5 of 22] “There is a hierarchy of logics for formal reasoning (in order the state elements), arranged according to the generality of their data types and operators (state elements) [46]. For the example in Fig. 1, a simple propositional logic (are defined in the source code script) was adequate. In propositional or zerothorder logic, only propositional variables (are defined in the source code script) are allowed, that is, variables over {true,false}; and the only operators or functions allowed are the logical operators /\, V, - , and other operators derived from these. Propositional logic can be extended in a small way by adding the quantification operators V and 3 .”) See also MCFARLAN ([Section 2.4 Extensions to the Basic Method] “As the above discussion indicates, verifying real designs makes many demands on the underlying formal system. It must be able to handle data types, such as the integers, and complex objects, such as arrays and time dependent sequences (the test sequence); and it must be capable of describing hierarchy and structure (includes a default processing order) and relating these to behavior. There are three basic ways to extend the formal system to meet these demands. First, we can use a higher order logic that is powerful enough to allow us to define and reason about the complex objects involved in verification. Second, we can extend the logic by adding new operators and rules (are defined in the source code script) specially adapted to reasoning about sequences and structure. And third, we can imbed the logic in another system that is designed specifically to handle some of the issues that are difficult to represent in logic.”)
It would have been obvious to one of ordinary skill in the art, before the effective filing date, to combine the teachings of MCFARLAND with ZHOU, as the references relates to the field of verification of semiconductor integrated circuit hardware designs. MCFARLAND would modify ZHOU wherein the test sequence includes a default processing order for the state elements comprising an order the state elements are defined in the source code script. The benefits of doing removes the need to make everything an explicit function of time, in some cases leading to simpler specifications of sequential behavior and also makes it unnecessary to use second-order logic, which can result in a simpler, more efficient proof system. (MCFARLAND [Section IV. | Temporal Logic | pdf page 10 of 22]). Accordingly, claim 3 is rejected based on the combination of these references.
Claim 11
Claim 11 is rejected because it is the system embodiment of claim 3, with similar limitations to claim 3, and is such rejected using the same reasoning found in claim 3.
Claim 17
Claim 17 is rejected because it is the non-transitory computer-readable medium embodiment of claim 3, with similar limitations to claim 3, and is such rejected using the same reasoning found in claim 3.
Claim 4
Claim 4 is rejected because the combination of ZHOU and MCFARLAND teach the claim 2 limitations.
ZHOU does not explicitly teach wherein the script defines a test sequence which defines a processing order for the state elements by grouping similar state elements.
However, MCFARLAND teaches wherein the script defines a test sequence which defines a processing order for the state elements by grouping similar state elements MACFARLAND ([Section 5.1 Predicate Transformers | pdf page 15 of 22] “One technique that is often used to simplify the verification is to add "checkpoints" at corresponding places in the two descriptions where the states can be compared. For example, one might find the point in a microprogram where the execution of a certain portion of the machine language instruction (script defines a test sequence) has been completed and the registers visible at the architectural level are in a well-defined state…This approach has often been used in hardware verification, including the verification of microcode [18], [8], [9], a 10 000-transistor signal-processing chip [63], the verification of logic implementations (15], (19], and even the verification of layout (which defines a processing order) (44). These systems and others like them differ in input languages, the type of constructs handled, and the way the predicates are represented and manipulated. The basic approach is the same, however Symbolic simulation is used to derive logic expressions describing the states (order for the state elements) in two parallel hardware descriptions, and these are checked for correspondence using some form of automatic theorem prover. Other groups have combined temporal logic with symbolic simulation (grouping similar state elements). One example of this is the DDL Verifier of Maruyama and Fujita [47). This system takes a register-transfer hardware description in the DDL language and checks assertions supplied by the user for validity with respect to that description. The logic used is based on first order temporal logic with equality, but it is still restricted enough that the proofs of individual assertions can be automated and done efficiently.”)
It would have been obvious to one of ordinary skill in the art, before the effective filing date, to combine the teachings of MCFARLAND with ZHOU, as the references relates to the field of verification of semiconductor integrated circuit hardware designs. MCFARLAND would modify ZHOU wherein the script defines a test sequence which defines a processing order for the state elements by grouping similar state elements. The benefits of doing removes the need to make everything an explicit function of time, in some cases leading to simpler specifications of sequential behavior and also makes it unnecessary to use second-order logic, which can result in a simpler, more efficient proof system. (MCFARLAND [Section IV. | Temporal Logic | pdf page 10 of 22]). Accordingly, claim 4 is rejected based on the combination of these references.
Claim 12
Claim 12 is rejected because it is the system embodiment of claim 4, with similar limitations to claim 4, and is such rejected using the same reasoning found in claim 4.
Claim 18
Claim 18 is rejected because it is the non-transitory computer-readable medium embodiment of claim 4, with similar limitations to claim 4, and is such rejected using the same reasoning found in claim 4.
Claim 10
Claim 10 is rejected because the combination of ZHOU and MCFARLAND teaches the claim 7 limitations.
ZHOU teaches wherein the test sequence defines a processing order for the state elements ZHOU ([Section A. Abstraction Engine | pdf page 4 of 13] “1) Construction of CFG and DFUD Chains: The source code of the DUV is instrumented with additional counters which act as a communication channel between the concrete and symbolic simulations. To assist the path constraint extraction, the CFG of the DUV is built (test sequence). Meanwhile, the data flow graph (DFG) of the DUV, representing as DFUD chains, is built based on the CFG to obtain the data dependence between variables (defines a processing order). The CFG is extracted from the Verilog RTL model of the DUV. Each node of the CFG (state elements) corresponds to a single statement or conditional expression (test sequence defined) in the design. The design with additional counters and its corresponding CFG for the example given in Fig. 4(a) are shown in Fig. 6. Each branch node is followed by an additional counter (ik <= ik + 1), which has been underlined in Fig. 6(a). Their values are monitored during simulation to record the concrete paths.”) See also ZHOU ([Figure 4].) Accordingly, claim 10 is rejected based on the combination of these references.
PNG
media_image5.png
487
481
media_image5.png
Greyscale
ZHOU Figure 4 Reference
Claim 16
Claim 16 is rejected because it is the non-transitory computer-readable medium embodiment of claim 10, with similar limitations to claim 10, and is such rejected using the same reasoning found in claim 10.
Claims 9 is rejected under are rejected under 35 U.S.C. 103 as being unpatentable over ZHOU, in view of MCFARLDAN, and in further view of view of Paul (Leveraging Accelerated Simulation for Floating-Point Regression), herein PAUL.
Claim 9
Claim 9 is rejected because the combination of ZHOU and MCFARLAND teach the claim 7 limitations.
The combination of ZHOU and MCFARLAND does not explicitly teach wherein the resources comprise at least one of: general purpose registers (GPRs), floating point registers (FPRs), system registers, and system memory, and each state element defines a value of the resource after the state transition.
However, PAUL teaches wherein the resources comprise at least one of: general purpose registers (GPRs), floating point registers (FPRs), system registers, and system memory, and each state element defines a value of the resource after the state transition PAUL ([Figure 1], [Figure 2], and [Section 3 FP Regression Tool] “The high level execution flow of the tool is described in Figure 1. We start with a set of test-cases pre-generated by FPgen[5], as depicted in the leftmost section of the Figure 1. FPgen is a test-generation framework that provides a convenient platform for biasing and generating operand data for floating-point instructions. The verification engineer can choose the set of test-cases so they focus on a specific instruction or event (for example, sqrt) or opt for a set that provides broad coverage of the entire floating point spectrum. Our tool outputs a single program that includes all the desired test-cases. Next, our tool generates the initial program and then executes it on a software reference model that is instruction accurate2, as depicted in the middle section of the Figure 1”…Footnotes states “An instruction accurate reference model calculates the values that will appear in the registers and memory after each executed instruction, as specified in the architecture book.” See also PAUL ([Section 3.2 Program Structure] “The kernel is in charge of initializing the relevant resources once the execution of the program begins. We demonstrate the concept on a real Power TM design, and thus, we make extensive use of General Purpose Registers (GPRs). We assign most of the processor’s general purpose registers with fixed roles for managing the test program. Table 1 lists these roles. For example, we use GPR9 and GPR10 as base pointer and offset register, respectively, to the expected results table. After values are saved to the expected results table, GPR10 is incremented to point to the next available entry in the table. Note that GPR5, GPR6, GPR7 and GPR8 point to different tables in the two.”)
It would have been obvious to one of ordinary skill in the art, before the effective filing date, to combine the teachings of PAUL with ZHOU and MCFARLAND, as the references relates to the field of verification of semiconductor integrated circuit hardware designs. PAUL would modify ZHOU and MCFARLAND wherein the resources comprise at least one of: general purpose registers (GPRs), floating point registers (FPRs), system registers, and system memory, and each state element defines a value of the resource after the state transition. The benefits of doing presents a novel acceleration-only tool, which enables a fast and efficient methodology for floating point regression and overcome the lack of test-bench in this environment through self-checking. (PAUL [Abstract]). Accordingly, claim 9 is rejected based on the combination of these references.
PNG
media_image6.png
643
836
media_image6.png
Greyscale
Paul Figure 1 Reference
PNG
media_image7.png
687
808
media_image7.png
Greyscale
Paul Figure 2 Reference
Claims 5, 6, 13, 19 and 20 is rejected under are rejected under 35 U.S.C. 103 as being unpatentable over ZHOU, in view of MCFARLDAN, and in further view of view of DIAS (Precise Detection of Atomicity Violations), herein DIAS.
Claim 5
Claim 5 is rejected because the combination of ZHOU and MCFARLAND teach the claim 2 limitations.
The combination of ZHOU and MCFARLAND does not explicitly teach wherein the source code defines instruction sequences for more than one execution thread.
However, DIAS teaches wherein the source code defines instruction sequences for more than one execution thread DIAS ([Introduction | pdf page 1 of 16] “High-level data races results from the misspecification of the scope of an atomic block, by splitting it in two or more atomic blocks with other (possibly empty) non-atomic block between them. This anomaly is often referred as a high-level data race, and is illustrated in Fig. 1(a). A thread uses the method are Equal() to check if the fields ‘a’ and ‘b’ are equal. This method reads both fields in separate atomic blocks, storing their values in local variables, which are then compared.”)
It would have been obvious to one of ordinary skill in the art, before the effective filing date, to combine the teachings of DIAS with ZHOU and MCFARLAND, as the references relates to the field of verification of semiconductor integrated circuit hardware designs. DIAS would modify ZHOU and MCFARLAND wherein the source code defines instruction sequences for more than one execution thread. The benefits of doing detects both high-level data races and stale-value errors and performs better than previous approaches, achieving higher precision for small and medium sized programs, making it a good basis for a practical tool. (DIAS [Abstract]). Accordingly, claim 5 is rejected based on the combination of these references.
Claim 13
Claim 13 is rejected because it is the system embodiment of claim 5, with similar limitations to claim 5, and is such rejected using the same reasoning found in claim 5.
Claim 19
Claim 19 is rejected because it is the non-transitory computer-readable medium embodiment of claim 5, with similar limitations to claim 5, and is such rejected using the same reasoning found in claim 5.
Claim 6
Claim 6 is rejected because the combination of ZHOU, MCFARLAND, and DIAS teaches the claim 5 limitations.
ZHOU does not explicitly teach wherein the method further includes maintaining a mapping between each of a computer implemented execution thread and an execution thread executing the test model.
However, MCFARLAND teaches wherein the method further includes maintaining a mapping between each of a computer implemented execution thread and an execution thread executing the test model MCFARLAND ([Section III. Higher Order Logic | pdf page 9 of 22] “What Hunt does is to build lists of values for inputs and outputs, then pull values off the input lists when needed and add output values to the output lists (execution thread executing the test model) as they are generated. Moreover, instead of proving that the specification and implementation represent the same mapping of inputs to outputs for all time (method of mapping between each of a computer implemented execution thread), Hunt assumes that one macroinstruction cycle corresponds to a certain number N of microcycles, and proves that for any inputs and any state of memory, one macroinstruction cycle has the same effect as N microcycles. There is an implicit inductive argument that if both descriptions have the same effect after one macroinstruction cycle, they will have the same effect after any number of them. The advantage of the Boyer-Moore theorem prover is its efficiency and ease of use. The user must break down the problem into a series of small theorems that lead to the desired result, but once a theorem is posed, the theorem prover proceeds on its own (method further includes maintaining a mapping), using a powerful set of heuristics to guide the proof.)
It would have been obvious to one of ordinary skill in the art, before the effective filing date, to combine the teachings of MCFARLAND with ZHOU, as the references relates to the field of verification of semiconductor integrated circuit hardware designs. MCFARLAND would modify ZHOU wherein the method further includes maintaining a mapping between each of a computer implemented execution thread and an execution thread executing the test model. The benefits of doing removes the need to make everything an explicit function of time, in some cases leading to simpler specifications of sequential behavior and also makes it unnecessary to use second-order logic, which can result in a simpler, more efficient proof system. (MCFARLAND [Section IV. | Temporal Logic | pdf page 10 of 22]). Accordingly, claim 6 is rejected based on the combination of these references.
Claim 20
Claim 20 is rejected because it is the non-transitory computer-readable medium embodiment of claim 6, with similar limitations to claim 6, and is such rejected using the same reasoning found in claim 6.
Conclusion
Any inquiry concerning this communication or earlier communications from the examiner should be directed to MARTIN K VU whose telephone number is (703)756-5944. The examiner can normally be reached 7:30 am to 4:30 pm M-F.
Examiner interviews are available via telephone, in-person, and video conferencing using a USPTO supplied web-based collaboration tool. To schedule an interview, applicant is encouraged to use the USPTO Automated Interview Request (AIR) at http://www.uspto.gov/interviewpractice.
If attempts to reach the examiner by telephone are unsuccessful, the examiner’s supervisor, Renee Chavez can be reached on 571-270-1104. The fax phone number for the organization where this application or proceeding is assigned is 571-273-8300.
Information regarding the status of published or unpublished applications may be obtained from Patent Center. Unpublished application information in Patent Center is available to registered users. To file and manage patent submissions in Patent Center, visit: https://patentcenter.uspto.gov. Visit https://www.uspto.gov/patents/apply/patent-center for more information about Patent Center and https://www.uspto.gov/patents/docx for information about filing in DOCX format. For additional questions, contact the Electronic Business Center (EBC) at 866-217-9197 (toll-free). If you would like assistance from a USPTO Customer Service Representative, call 800-786-9199 (IN USA OR CANADA) or 571-272-1000.
/M.K.V./Examiner, Art Unit 2186
/RENEE D CHAVEZ/Supervisory Patent Examiner, Art Unit 2186