The application of formal methods to the system-level design of hardware components is still an open issue for which concrete
case-studies are needed. We present here an industrial experiment concerning the application of the process algebraic language
lotos (iso standard 8807) to the design of polykid, a cc-numa (cache coherent – non-uniform memory access ) multiprocessor
architecture developed by bull. The formal descriptions developed for polykid have served as a basis not only for model-checking
verification using cadp (caesar/aldebaran development package), but also for hardware-software co-simulation using the
exec/caesartool, and for automatic generation of executable tests using the tgv tool.
Key words: Cache coherency – cc-numa – Code generation – Co-design – Computer architecture – Conformance testing – Co-simulation
– Formal methods – Formal specification – Hardware design – lotos – Process algebra – numa – Rapid prototyping – System level
design – Test generation – Testing – Validation – Verification
Published online: 18 July 2001