Parallel Stimulus Generation Based on Model Checking for Coherence Protocol Verification

The complexity of the multicore communication protocols makes it a huge effort to validate the corresponding register transfer level (RTL). To achieve the high coverage of simulation, this brief proposes a covalidation method to generate the RTL testbench based on the model-checking technique. An object-oriented event-mapping technique is proposed to transform the sequential traces created by formal method to parallel RTL stimulus. A case study on the modified, exclusive, shared and invalid protocol was performed and showed that the covalidation method could save significant effort to create RTL testbenches while maintaining high coverage.