This paper analyses formal methods usage within digital systems design process, having programmable logic devices as implementation devices. 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 devices, which give adequate flexibility for exercising different implementation strategies, allowing laboratory prototyping.