During Bounded Model Checking (BMC) blocks of a design are often considered separately due to complexity issues. Because the environment of a block is not available for the proof, invalid input sequences frequently lead to false negatives, i. e. counter-examples that can not occur in the complete design. Finding and understanding such false negatives is currently a time-consuming manual task. Here, we propose a method to automatically avoid false negatives which are caused by invalid input sequences for blocks connected by standard communication protocols.
展开▼
