Lightweight Specification-based Testing of Memory Cards: A Case Study

As the markets of mobile devices are expanding, needs for developing reliable memory cards are increasing, too. Samsung, one of the major players in memory card business, is also trying to improve the validation process for their memory card products. To this aim, we conducted a pilot project where a formal method and a specification-based testing technique are adopted to validate our MMC (MultiMediaCard) system. System under testing (SUT) is an MMC card which is implemented in two languages, Verilog for RTL and C for firmware. To test MMC cards, we formalize the fully general behavior model of MMC host with Esterel. It is also used as a test oracle in order to automate testing of SUT. Then, the two models of host and card are co-simulated on the verification environment Seamless. We conducted scenario-based testing and random testing.