Teaching formal methods within system-on-a-programmable-chip design

The paper analyses the use of formal methods within a digital systems design process, having programmable logic devices as implementation devices. An alternative paper title could be "From modeling formalisms to SoPC (system-on-a-programmable-chip) implementations on FPGAs", where the emphasis is put on the design of the control/reactive part of the system. A set of formalisms have been considered for the task, ranging from state diagrams to Petri nets, and including state diagrams with data-paths, hierarchical and concurrent state diagrams, and statecharts. How to handle concurrency modeling through the referred set of formalisms is analyzed using a set of mini-projects, which are proposed as exercises to the students. Implementation platforms include FPGAs and CPLDs (complex programmable logic devices), which give adequate flexibility for exercising different implementation strategies, allowing laboratory prototyping.