DETAILED ACTION
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 . This Office Action responds to the Application filed on 12/30/2022. Claims 1-20 are pending.
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 18-20 are rejected under 35 U.S.C. 101 because the claimed invention is directed to non-statutory subject matter. The claim(s) does/do not fall within at least one of the four categories of patent eligible subject matter because the claims are directed to computer (or machine) readable (storage) medium which could include transitory readable medium such as carrier wave or electromagnetic wave since Applicant's specification does NOT explicitly exclude the transitory readable medium, wherein based on the broadest reasonable interpretation of the claims in view of Applicant's specification and in view of the customary and typical meaning the terms computer readable media, it is determined that Applicant's “machine-readable storage medium” would include both forms of transitory and non-transitory computer readable media since the terms as defined in Applicant's specification are open-ended (see Applicant’s specification, paragraphs [0066]-[0067] see also the USPTO Official Gazette 1351 OG 212 on Guidelines for Computer Readable Media).
Applicant may want to insert –non-transitory—before “machine-readable” (line 1, claim 18) to limit the claims to patent eligible subject matter.
Claim Rejections - 35 USC § 102
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 the appropriate paragraphs of 35 U.S.C. 102 that form the basis for the rejections under this section made in this Office action:
A person shall be entitled to a patent unless –
(a)(1) the claimed invention was patented, described in a printed publication, or in public use, on sale, or otherwise available to the public before the effective filing date of the claimed invention.
Claim(s) 1-20 is/are rejected under 35 U.S.C. 102(a)(1) as being anticipated by McIlwain et al. (US Patent No. 10,643,012 B1).
As per claims 1 and 18, Fig. 3 illustrates the elements of the claims comprising:
synthesizing (steps 302, 304) a plurality of intermediate netlists (i.e., design d1…n-1 are intermediate netlists—see col. 6, lines 21-34) from a register transfer level (RTL) description (i.e., RTL design d0) of the IC;
launching formal verification processes (step 306; see also col. 6, lines 7-20) for the plurality of intermediate netlists (designs di..dj, wherein 0<=I,=j<=n) concurrently with the synthesizing;
synthesizing (steps 304, 306) the plurality of intermediate netlists (i.e., design d1…n-1 are intermediate netlists—see col. 6, lines 21-34) while the formal verification processes execute concurrently with the synthesizing;
and receiving an indication of validity or non-validity for the plurality of intermediate netlists from the formal verification processes (see col. 5, lines 35-51); wherein the machine-readable medium is further described in col. 7, lines 50-62.
As per claims 2-5,20, Figs. 2A and 2B further illustrates the sequences in which the synthesis tool and formal verification tool operate in that:
The RTL design 202 is the design d0, and the netlist 204 is the final design dn and designs di and dj, where 1<i<j<n are intermediate checkpoint designs (which are also in the form of netlist—see col. 6, lines 21-34) which are obtained through the synthesis tool 206 (see also col. 4, lines 59-67);
The intermediate checkpoint design di (i.e., any of the plurality of intermediate netlists) can be formally checked for equivalence against a) the original RTL design d0, b) another intermediate check point design dj or c) the final netlist dn (see col. 4, line 67 to col. 5, line 3);
Formal equivalent checking tool 208 can be executed concurrently or in parallel with the synthesis tool 206 as follows:
Per claims 2-3, after a first intermediate netlist (intermediate design di) is synthesized by the synthesis tool 206, formal verification (i.e., equivalence checking tool 208) can concurrently check equivalences between RTL design d0 and the first intermediate netlist (i.e., checkpoint design di), while synthesis tool 208 continues to concurrently synthesize sequentially second or subsequent intermediate netlists (i.e., intermediate designs dj) (see col. 5, lines 14-24).
Per claim 4, formal verification (i.e., equivalence checking tool 208) is performed for a subsequent intermediate netlist (i.e., intermediate design dj) with a prior intermediate netlist (intermediate design di) (see col. 5, lines 24-27).
Per claims 5,20, since there is no limitation as how many intermediate designs are synthesized, there exists overlapping operations in which at least two separate netlists are being formally verified. That is, equivalent checking tool 208 could overlapping (concurrently) operates for situations of claims 2-4 as described above until the final netlist dn is generated and checked (see col. 5, lines 14-34).
As per claim 6, proving that the RTL description d0 is formally equivalent to a final netlist dn using the intermediate netlists (intermediate designs di..dj) by proving that the intermediate netlists are valid or passed equivalent check (see col. 5, lines 49-63).
As per claim 7, further comprising: modifying an optimization for the RTL description in response to a non-valid intermediate netlist that is indicated as non-valid during the formal verification process in order to define a modified optimization for the RTL description; synthesizing a new intermediate netlist from the modified optimization for the RTL description; and launching a formal verification process for the new intermediate netlist (see col. 5, lines 38-51).
As per claim 8, wherein the intermediate netlists have different transformations comprising at least one of: optimizations (see col. 5, lines 20-21, 40-41).
As per claim 9, the pausing synthesizing of a subsequent intermediate netlist until a previous intermediate netlist is validated by the formal verification process; and resuming synthesizing the subsequent intermediate netlists when the prior intermediate netlist is validated by the formal verification process is taught in col. 5, lines 35-41, wherein verification process is paused when two designs are not equivalent, requiring user interactive correction before further verification can be performed as further evidence by the fact that “in some embodiments, the corrective action can be to continue the synthesis and attempt proving equivalences with the next intermediate checkpoint design” (col. 5, lines 31-49), implying the same paragraph cited, that correction action would stop or pause the synthesis process until the previous intermediate netlist is validated before continuing to synthesize the subsequent intermediate netlist.
As per claim 10, since the system of McIlwain et al. allow for user interaction (see col. 5, lines 35-51) and user set-up commands (see col. 7, lines 15), it is within the scope of McIlwain et al. to allow entering a command to a synthesis engine capable of performing synthesizing, in order to launch the formal verification process for the intermediate netlist to begin.
As per claim 11, wherein the synthesizing and the formal verification processes are performed by separate synthesis and formal verification engines as illustrated in Fig. 2B with Synthesis Tool 206 and Equivalence Checking Tool 208, respectively, and wherein the synthesis engine launches the formal verification processes for the formal verification engine (i.e., “Specifically, one implementation can be as follows: (1) at start of compile, a synthesis tool invokes [or launches] a formal logic equivalence checker”—col. 4, lines 21-23).
As per claim 12, further comprising: sending the intermediate netlists sequentially from a synthesis engine to a formal verification engine (i.e., the “synthesis tool invokes a formal logic equivalence checker…the synthesis tool writes intermediate checkpoint designs [intermediate netlists]” which the “formal logic equivalence checker reads each checkpoint design” (col. 4, lines 22-30), implying that intermediate checkpoint was sent by the synthesis engine in order for the verification tool to have read it.
As per claim 13, further comprising: specifying formal verification parameters for the formal verification processes selected from the group comprising at least one of: mode of formal verification or not formal verification (i.e., timing constrain verification or equivalence checking—col. 3, line 49-51); a selection of a formal verification engine (see col. 3, lines 37-44, i.e., IC designer would be able to select the particular software tools including for formal verification that best suits the needs); incremental dumps of intermediate netlists (col.5, lines 35-51, i.e., since user interaction is required to apply corrective action, allowing the synthesis to pause before verification is applied as discussed in the rejection of claim 9 above, the dumping or writing of the intermediate checkpoint design is incrementally written).
As per claim 14, launching the formal verification processes further comprises launching formal verification processes for an intermediate netlist with two different formal verification engines in parallel (see col. 6, lines 16-20, the formal verification synthesis tool on different computers concurrently executing could also be considered as two different formal verification engines, one on each different computer).
As per claim 15, McIlwain et al. teach all of the elements of claim 1, from which the claim depends as discussed in the rejection of claim 1 above; including the formal verification process for equivalent checking as discussed in the rejection of claim 1 above, wherein the second formal verification processes that is a simulation-based verification process would be within the scope of McIlwain et al. (col. 1, lines 14-19; col. 3, lines 49-52, i.e., timing constraints verification).
As per claim 16, Fig. 3 illustrates the elements of the claims comprising:
synthesizing (steps 302, 304) a plurality of intermediate netlists (i.e., design d1…n-1 are intermediate netlists—see col. 6, lines 21-34) from a register transfer level (RTL) description (i.e., RTL design d0) of the IC;
launching formal verification processes (step 306; see also col. 6, lines 7-20) for the plurality of intermediate netlists (designs di..dj, wherein 0<=I,=j<=n) concurrently with the synthesizing;
synthesizing (steps 304, 306) the plurality of intermediate netlists (i.e., design d1…n-1 are intermediate netlists—see col. 6, lines 21-34) while the formal verification processes execute concurrently with the synthesizing;
and proving that the RTL description is formally equivalent to a final netlist formed of the intermediate netlists by proving that the all the intermediate netlists are valid (see col. 5, lines 49-63; see also rejection of claim 6 above).
As per claim 17, launching formal verification processes for at least two separate intermediate netlists in parallel since there is no limitation as how many intermediate designs are synthesized, there exists overlapping operations in which at least two separate netlists are being formally verified. That is, equivalent checking tool 208 could overlapping (concurrently) operates for situations of claims 2-4 as described above until the final netlist dn is generated and checked (see col. 5, lines 14-34). (See rejection of claim 5 above).
As per claim 19, the system of McIlwain et al. involves user interaction to correct reported failure, in which graphical user interface (GUI) would part of the user interactive display (see col. 7, lines 6-39) as part of the state of the art, McIlwain et al. would necessarily cover the displaying (i.e., reporting) the indication of validity or non-validity of the intermediate netlists through a graphical user interface (GUI).
Conclusion
Any inquiry concerning this communication or earlier communications from the examiner should be directed to PHALLAKA KIK whose telephone number is (571)272-1895. The examiner can normally be reached Maxiflex Mon-Fri 8:30AM-5PM.
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, Jack Chiang can be reached at 5712727483. 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.
Any response to this action should be mailed to:
Commissioner for Patents
P. O. Box 1450
Alexandria, VA 22313-1450
or faxed to:
571-273-8300
/PHALLAKA KIK/Primary Examiner, Art Unit 2851 December 27, 2025