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 is response to Application 18/340,662 filed on 06/23/2023. Claims 1-20 are pending in the current application.
Claim Objections
Claims 5-6, 12-13, and 17-18 are objected to because of the following informalities:
As per claim 5: line 3, replaces “X injection” with -- unknown logic value (X value) injection --.
As per claim 6: line 4, replaces “X injection” with -- X value injection --.
As per claim 12: line 3, replaces “X injection” with -- unknown logic value (X value) injection --.
As per claim 13: line 5, replaces “X injection” with -- X value injection --.
As per claim 17: line 2, replaces “X injection” with -- unknown logic value (X value) injection --.
As per claim 18: line 4, replaces “X injection” with -- X value injection --.
Appropriate correction is required.
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.
Claim(s) 1-6, 8-13, 15-18, and 20 is/are rejected under 35 U.S.C. 103 as being unpatentable over Lo et al., (U.S. Pub. 2022/0083717) in view of Pedneau, Mike (U.S. Pat. 10,896,277).
As per claims 1, 9, and 16: Lo teaches an apparatus, a method, and a computer-readable medium (‘717, the abstract, fig. 11, par. [0031]), comprising:
interface circuitry (‘717, the abstract, fig. 11, par. [0031] –[0033]);
machine readable instructions (‘717, the abstract, fig. 11, par. [0031]); and
programmable circuitry to at least one of instantiate or execute the machine readable instructions (‘717, the abstract, fig. 11, par. [0031]) to:
obtain an assumption property associated with a system on a chip (SoC) architecture (‘717, the abstract, “attribute-point-based timing formal verification (FV) of ASIC and SOC designs”, par. [0002], “timing attributes are add-on informative tags, notes, or symbolic properties which can be adopted or queried when performing static timing analysis (STA) to compiled design databases”; par. [0017], attributed-point-based (e.g., features or properties of the pins of the nets) timing constraint for formal verification);
obtain a timing assertion associated with the SoC architecture (‘717, the abstract, “attribute-point-based timing formal verification of ASIC and SOC designs. A target circuit design having a first set of netlists and timing constraint is received”, fig. 3, 320 and 340, par. [0021]);
determine, using a formal property verification (FPV) tool, valid functional vectors (i.e., test cases: case values) for the SoC architecture based on the assumption property and the timing assertion (‘717, fig. 2, par. [0019], the point based program 230 checks each attribute (e.g., false paths, multi-cycle paths, and case value settings), fig. 3, 350, and fig. 4, 420, and 440, par. [0022]); and
determine whether to accept a timing constraint based on the valid functional vectors, the timing constraint corresponding to the timing assertion (‘717, fig. 3 and fig. 4, 440, 450, and 460, par. [0022]).
Lo does not teach determine counter examples in the formal verification.
Pedneau teaches an electronic design automation formal verification EDA application is configured to receive an initial evaluation of a circuit design of an integrated circuit (IC) chip. The circuit design of the IC chip includes a list of properties for the IC chip, and the list of properties includes a list of assertions for the IC chip. The formal verification EDA program extracts a counter-example trace from the initial evaluation. The counter-example trace characterizes a set of signals over a plurality of cycles that reach a state in which a given assertion in the list of assertions does not hold true. The formal verification EDA program identifies a subset of signals in the counter-example trace that remain in a specific constant value over the plurality of cycles. The formal verification (VF) EDA program executes an over constraint formal verification for the circuit design (‘277, the abstract, fig. 1, counter example traces 76 and also see formal verification engine 72 and also see fig. 3 and fig. 8).
It would have been obvious to one of ordinary skill in the art at the time of the effective filling date of claimed invention to combine Pedneau and Lo to modifying Lo’s FV method includes Fedneau’s counter example trace to prove that there is no possible way to violate any properties of the circuit design when the counter example is not found (‘277, col. 5, ll. 9-18).
As per claims 2 and 10: Lo and Pedneau teach wherein the programmable circuitry is to obtain the timing assertion based on user input to the FPV tool (‘717, fig. 3, par. [0021] and par. [0022], user manually modify corresponding netlist and timing constraint).
As per claims 3 and 11: Lo and Pedneau teach wherein the programmable circuitry is to:
obtain the timing constraint based on user input to the FPV tool (‘717, fig. 3, par. [0021]); and
convert the timing constraint into the timing assertion (‘717, fig. 2, 210 to 220).
As per claim 4: Lo and Pedneau teach wherein the timing constraint corresponds to at least one of a multi cycle path, a false path, a maximum delay path, a minimum delay path, or a reconverge cross clock path (‘717, par. 19, and also see fig. 3, 320).
As per claims 5, 12, and 17: Lo and Pedneau teach wherein the programmable circuitry is to select, based on the timing assertion, at least one of a location or a duration for X injection in a register-transfer level (RTL) design, the RTL design corresponding to the SoC architecture (‘717, fig. 3, 320 and par. [0021], timing constraint; ‘277, col. 4, ll. 15-46, fig. 3, 302, col. 7, ll. 58-62, RTL).
As per claims 6, 13, and 18: Lo and Pedneau teach wherein the programmable circuitry is to:
identify a timing path associated with the timing assertion, the timing path from a start point to an end point based on the RTL design (‘717, fig. 5, starting point 502/552 and ending 514/564, par. [0023]); and
select the location for the X injection corresponding to the timing path (‘717, fig. 5, false path input of 506/556 or input 514/564, par. [0024]).
As per claim 8, 15, and 20: Lo and Pedneau teach wherein the programmable circuitry is to output the valid functional vectors and the counter examples without outputting vectors that do not satisfy the assumption property (‘277, fig. 3, counter example 318 and output result 334 from over constraint formal verification result 330).
Allowable Subject Matter
Claims 7, 14, and 19 are objected to as being dependent upon a rejected base claim, but would be allowable if rewritten in independent form including all of the limitations of the base claim and any intervening claims.
The following is a statement of reasons for the indication of allowable subject matter: wherein the programmable circuitry is to:
based on the evaluation, determine whether the timing assertion is satisfied;
based on the timing assertion being satisfied, assign the input vector as one of the valid functional vectors; and
based on the timing assertion not being satisfied, assign the input vector as one of the counter examples.
Conclusion
any inquiry concerning this communication or earlier communications from the examiner should be directed to NGHIA M DOAN whose telephone number is (571)272-5973. The examiner can normally be reached Mon - Fri 7:00 AM - 5:00 PM.
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 571-272-7483. 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.
NGHIA M. DOAN
Primary Examiner
Art Unit 2851
/NGHIA M DOAN/Primary Examiner, Art Unit 2851
Prosecution Insights