Mixing ATPG and property checking for testing HW/SW interfaces

A critical part of the design of HW/SW systems concerns the definition of the HW/SW interface. Such interfaces do not directly map a functionality of the system description, but they are inferred by the characteristics of the selected programmable device (CPUs, DSPs, ASIPs, etc.). Their addition to the design can modify the behavior of the original system, thus their verification is a hard task. The proposed verification methodology joins functional verification and property checking in order to avoid their respective limitations. The methodology is focused on SystemC descriptions that can be automatically synthesized. This is particularly important since commercial model checking tools work on structural hardware descriptions, which can be obtained by performing rapid prototyping of both HW and SW parts of SystemC models. The proposed approach has been verified on the SystemC model that is the reference synthesis example of one of the most powerful SystemC synthesis environment.