Method for decomposing a hardware model and for accelerating formal verification of the hardware model

摘要

Described is a method performed by a computing device, the method comprises: deriving a hierarchal structure of hardware instances of a hardware block, wherein the hardware block is described in a register transfer language (RTL); determining complexity of at least one hardware instance, in the hierarchal structure, with reference to a complexity metric; identifying, in response to the determined complexity of the at least one hardware instance, whether the at least one hardware instance is to be modeled; and modifying the hierarchal structure with information about the to be modeled hardware instance.

主权项

1. A method performed by a computing device, the method comprising:
deriving, by the computing device having a processor and a memory, a hierarchical structure of hardware instances of a hardware block, wherein the hardware block is described in a register transfer language (RTL); determining, by the computing device, complexity of at least one hardware instance, in the hierarchical structure, with reference to a complexity metric, wherein the complexity metric is one or more of the following or is a weighted average of two or more of the following:
a sum of flip-flop bits in the at least one hardware instance;a sum of latch bits in the at least one hardware instance; ora sum of port bits of the at least one hardware instance; identifying, by the computing device, in response to the determined complexity of the at least one hardware instance, whether the hardware instance is to be modeled; and modifying, by the computing device, the hierarchical structure of the hardware instances of the hardware block with information about the to-be modeled hardware instance.