US20260105231
2026-04-16
Physics
G06F30/3323
The patent describes a method for enhancing semi-formal verification (SFV) in integrated circuit design. It combines bounded model checking (BMC) with simulation to improve the identification of design flaws. The method focuses on guiding simulations based on the rarity of sub-states in register partitions of the logic design, discounting those nearing saturation. This approach aims to improve the effectiveness and efficiency of SFV by identifying satisfied verification properties with fewer computational resources.
Integrated circuit design requires rigorous functional verification to ensure correctness. Traditional simulation methods often fall short in coverage, failing to identify all potential design flaws. Formal verification (FV) offers exhaustive checking but struggles with scalability in large designs. SFV emerges as a middle ground, leveraging symbolic algorithms to cover more complex designs than FV alone. However, SFV faces challenges such as slow rarity computation, repetitive state simulation, and resource limitations that hinder its effectiveness.
The invention introduces rarity-guided SFV techniques that address these historical limitations. By using rarity scores to guide simulation progress and focusing on diverse design states, the method enhances bug detection and verification coverage. It also reduces computational waste by avoiding redundant state checks and optimizes resource usage, thus enabling deeper exploration of complex designs without exhausting memory or processing power.
The techniques can be implemented as methods, systems, or computer program products. They involve processing circuitry that performs SFV on a logic design, utilizing both BMC and simulation. The method includes narrative descriptions, flowcharts, and block diagrams to illustrate various aspects. It allows flexibility in operation order and integration, ensuring adaptability to different technological contexts and requirements.
The method can be executed within a computing environment comprising various components such as processors, memory, and storage devices. It can be performed on different types of computers, including desktops, laptops, and cloud-based systems. The environment supports distributed processing, enabling the method to be implemented across multiple locations or systems, thus enhancing its scalability and applicability to large-scale designs.