×

Method, system, and program product for automated verification of gating logic using formal verification

  • US 7,448,008 B2
  • Filed: 08/29/2006
  • Issued: 11/04/2008
  • Est. Priority Date: 08/29/2006
  • Status: Expired due to Fees
First Claim
Patent Images

1. A method of verifying gating rules comprising the steps of generating a testbench hardware design language code from a design source hardware design language code, and building a formal verification model comprising the testbench hardware design language code and a hardware design language for a design under test to provide to a design verification tool, by the steps as follows:

  • (I) generating the testbench hardware design language code from the design source hardware design language code by the steps as follows;

    a. identifying interface signals requiring gating verification, including denoting registers and/or latches that are asserted to remain stable from a design source;

    b. identifying each component to be independently verified using the design source and an assertion that registers and latches within a component will remain stable during gating;

    c. extracting a list of interfaces, registers, and latches from each component;

    d. generating a testbench, said testbench driving a formal verification step utilizing the list of interfaces, registers, and latches from each component as an input to produce the testbench, the testbench having automated rules to verify assertions regarding latch stability;

    e. compiling the testbench to form a verification model; and

    (II) building a formal verification model comprising the testbench hardware design language code and the hardware design language for the design under test for provision thereof to a design verification tool, by the steps as follows;

    f. executing a formal verification process to determine that all latches and registers asserted to remain stable under a gating condition are stable, including attempting to produce a counter example, illustrating how a particular latch can change state while its associated fence signal is being applied; and

    g. if counter examples exist, repetitively updating the design source to fix an error until the design source completes the formal verification process without any counter examples, else characterizing that the verification process is complete and all identified interfaces are concluded to be properly gated.

View all claims
  • 6 Assignments
Timeline View
Assignment View
    ×
    ×