CN-122021489-A - DRC design rule positive and negative example automatic generation method based on large language model and formal verification

CN122021489ACN 122021489 ACN122021489 ACN 122021489ACN-122021489-A

Abstract

The invention discloses a DRC design rule positive and negative example automatic generation method based on large language model and formal verification, which relates to the field of electric digital data processing, and comprises the following steps of firstly, accurately converting natural language rules into logic expression by utilizing an entity library and a function library which are constructed by combining the large language model; the method comprises the steps of carrying out logical disassembly and full-coverage enumeration traversal of a Boolean algebra space, then introducing an SMT solver to construct a target optimization problem, automatically solving coordinates to generate a test layout closely attached to rule boundaries, distributing clear positive and negative example labels, and finally eliminating false positive false alarms caused by multi-rule interference and intelligently identifying redundant rules through an innovative hierarchical context management mechanism. The invention greatly improves the verification coverage rate and the automation level, and can obviously reduce the labor cost of chip physical verification.

Inventors

YANG FAN
ZENG HUANLONG
YANG XINYI
YAN XIU

Assignees

复旦大学

Dates

Publication Date: 20260512
Application Date: 20260413

Claims (10)

1. A DRC design rule positive and negative example automatic generation method based on a large language model and formal verification is characterized by comprising the following steps: s1, converting design rules of natural language description into a logic expression based on a layout geometric relationship by using a large language model; s2, decomposing the logic expression into a plurality of basic predicates, and performing full coverage enumeration on truth combinations of the basic predicates based on a Boolean algebra space to construct a complete test space; s3, inputting the enumerated truth value combination as constraint conditions into a satisfaction model theory solver for solving, mapping the solved coordinates to generate a test layout, and distributing positive and negative example labels which characterize the compliance or violation rules for the test layout according to whether the corresponding truth value combination meets an original logic expression or not; s4, introducing a context management mechanism based on layout layer information, introducing background constraint of association rules when generating a test layout, and identifying redundant rules in a design rule base.
2. The DRC design rule positive and negative example automatic generation method based on large language model and formal verification of claim 1, wherein the step of S1 further comprises the steps of: s11, establishing an entity library for defining the geometric shape of the layout and a function library for expressing geometric relations; S12, inputting natural language design rules and examples into a large language model, and enabling the natural language design rules and examples to call the entity library and the function library to generate corresponding logic expression codes; s13, carrying out grammar checking and runtime checking on the generated codes, and feeding back error information to the large language model for correction when checking errors.
3. The DRC design rule positive and negative example automatic generation method based on large language model and formal verification of claim 1, wherein the step of S2 further comprises the steps of: s21, grouping and preprocessing predicates which have the same geometric meaning but different action objects to control the quantity of the predicates; S22, based on the Boolean algebra completeness theorem, systematically enumerating all 2 n true and false assignment combinations of the decomposed n basic predicates.
4. The DRC design rule forward and backward example automatic generation method based on the large language model and formal verification of claim 1, wherein in the step S3, the satisfiability model theory solver builds an optimization problem with the aim of minimizing the distance between the geometric parameters and the rule boundaries when solving so as to generate a test layout clung to the design rule boundaries.
5. The DRC design rule positive and negative example automatic generation method based on the large language model and formal verification of claim 4, wherein the optimization objective of the optimization problem is expressed as: wherein lhs and rhs respectively represent Each arithmetic predicate in (a) Left and right sides of (a).
6. The DRC design rule positive and negative example automatic generation method based on the large language model and formal verification according to claim 1 is characterized in that in the step S4, the context management mechanism specifically comprises the steps of identifying layout layers related to all design rules, dividing rules related to the same layout layers into the same rule group, when a test layout is generated aiming at a target rule, taking other rules in the same group as background constraint conditions, and jointly inputting the combination of the other rules and true values of the target rule into a solver, and if any negative example test layout cannot be generated for the target rule under the background constraint conditions, marking the rules as redundant rules.
7. The automatic generation method of the positive and negative examples of the DRC design rule based on the large language model and formal verification of claim 1 is further applied to automatic closed-loop correction of the DRC script, and specifically comprises the steps of inputting the generated test layout and the positive and negative example labels thereof and the logic expression generated in the step S1 into the large language model for generating the DRC script as feedback information so as to guide the generated script to be corrected.
8. The DRC design rule positive and negative example automatic generation method based on the large language model and formal verification of claim 1 is characterized in that the logic expression generated in the S1 step is formed by combining geometric conditions through logic operators, and the basic predicate in the S2 step is an arithmetic predicate.
9. An electronic device comprising at least one processor, and a memory communicatively coupled to at least one of the processors; wherein the memory stores a computer program to be executed by at least one of the processors, the computer program being executed by at least one of the processors to enable the at least one of the processors to perform the large language model and formal verification-based DRC design rule forward and backward automatic generation method of any one of claims 1-8.
10. A computer readable storage medium storing computer instructions for causing a processor to implement the large language model and formal verification-based DRC design rule forward and backward automatic generation method according to any one of claims 1-8 when executed.

Description

DRC design rule positive and negative example automatic generation method based on large language model and formal verification Technical Field The invention relates to the technical field of electric digital data processing, in particular to an integrated circuit computer aided design and electronic design automation, and specifically relates to a DRC design rule forward and backward example automatic generation method based on a large language model and formal verification. Background Design rule checking (Design Rule Check, DRC for short) is an indispensable core step in chip physical design. Design rules defined by the foundry describe geometric and electrical constraints, establishing limits for the manufacturing process, such as specifying minimum linewidths and spacing between polygons, etc. These rules, provided in a human-readable natural language format, form the basis for ensuring chip manufacturability and design reliability. In order for an EDA tool (e.g., calibre) to consistently and efficiently automatically detect violations in a layout, the design rules for these natural languages must be translated into machine-readable DRC scripts. However, the translation of design rules into scripts is highly labor-dependent, a multi-step and highly error-prone process. The accuracy of the script is critical and any error may lead to a real manufacturing violation being missed or a large number of false positives, both of which may have serious consequences. In actual engineering, to verify the correctness of DRC scripts, foundry typically relies on engineers to manually design test layouts (Test layouts). The experienced engineers have to spend months manually drawing a large number of test layouts for each design rule in an effort to cover all critical boundary conditions and thoroughly verify the script. With the continued evolution of nanoscale manufacturing processes, the number and complexity of design rules has increased significantly, further exacerbating the challenges of script verification. In response to the above problems, some methods for assisting in script verification have emerged in the industry. For example, a parameterized element (PCELL) is used as a seed test structure and is manually modified to create the desired variants, or a generic shape is completely manually created for each rule. There have also been studies that propose to use constraint-based parameterized patterns to generate test patterns by extrapolating constraints from similar rules in the mature process. In recent years, the development of large language model (Large Language Models, LLM) technology has also provided new ideas for automated script translation, and some research efforts have attempted to utilize large models for rule-to-script translation, such as normalizing rules by preprocessing and using sequence-to-sequence models for translation. Nevertheless, the existing methods still have significant drawbacks. The manner of extrapolation based on parameterization units or constraints is heavily dependent on existing mature process rules, limiting its applicability to new process node rules. The script generated by the large language model still has higher error rate due to the extremely strict physical rule logic of the integrated circuit, so that independent and strict test verification on the script is an unavoidable essential link. On the other hand, formal verification is widely applied in the field of hardware design, but how to accurately map DRC rules written in natural language into formal logic formulas, and automatically and completely generate a test layout with definite positive and negative case labels by utilizing a large language model collaborative solver, so that systematic solutions are not available for a long time. Disclosure of Invention The invention overcomes the defects of the prior art, provides a DRC design rule forward and backward example automatic generation method based on large language model and formal verification, which converts natural language rules into strict logic expression by using the large language model, then builds a complete test space through logic decomposition and Boolean space full coverage enumeration, then introduces a satisfiability module theory solver to automatically generate a test layout clinging to rule boundaries and allocate forward and backward example labels, finally eliminates multi-rule interference and identifies redundant rules through a context management mechanism, thereby systematically solving the problems of low automation degree and incomplete test coverage in DRC script verification. In order to achieve the purpose, the technical scheme adopted by the invention is that the first aspect provides a DRC design rule forward and backward example automatic generation method based on a large language model and formal verification, which comprises the following steps: s1, converting design rules of natural language description into a logic e