首页>
外国专利>
Verification Technique Including Deriving Invariants From Constraints
Verification Technique Including Deriving Invariants From Constraints
展开▼
机译:包括从约束中得出不变量的验证技术
展开▼
页面导航
摘要
著录项
相似文献
摘要
A method of performing formal verification on a design for an integrated circuit can include accessing a set of constraints for the design. These constraints can be partitioned based on their variables, wherein any overlapping variables can result in the conjoining of their corresponding constraints. Binary decision diagrams (BDDs) can be generated based on such conjoining. Notably, invariants can be derived from the BDDs. These invariants can include constant, symmetric/implication, one-hot/zero-hot, and ternary invariants. Deriving the invariants can include cofactoring and counting of minterms of the BDDs. Using the invariants while performing formal verification on the design can advantageously optimize system performance.
展开▼