Philippe LEDENT

Abstract
In SoC (System-on-Chip) design, finding bugs before production is mandatory to prevent wasting time, money, and material. Considering that traditional directed tests are not sufficient, the EDA (Electronic Design Automation) industry proposes the new language PSS (Portable test and Stimulus Standard) to move towards modeling for testing. Our work makes the CADP toolbox and its companion tools a formal-based support for PSS. We propose an alternative for PSS test generation by formal- izing PSS semantics in order to express models as LTSs (Labeled Transition Systems). The two immediate benefits are: (1) access to model checking that finds modeling errors prior to test generation, and (2) connection to confor- mance testing that produces the CTG (Complete Test Graph) containing all possible executions of the behavioral model that respect the desired test, from which extracted test suites guarantee coverage of the CTG.

 

Our methodology is applied to three examples: (1) ARM’s APB (Advanced Peripheral Bus) protocol, (2) a carefully crafted example that illustrates PSS semantic ambiguities, and (3) the security requirement of hardware resource isolation. The tests produced by this work have detected bugs on an SoC under development at STMicroelectronics.