The HILECOP methodology is a process for the design of critical digital systems. In HILECOP, Petri Net (PN) models are used as a high-level formalism to specify the behavior of the designed systems. VHDL (VHSIC Hardware Description Language) code is then automatically generated from PN models to implement the digital system on Field Programmable Gate Array (FPGA) circuits. The goal of this work is to formally verify that through this model-to-text transformation, the behavior described by a PN model is preserved in the produced VHDL code, knowing that the transformed PN models are synchronously executed on the target. As a first step toward the achievement of this goal, we present our implementation of HILECOP's PN structure and semantics , which has been formalized using the Coq proof assistant. We also describe a token player program for these PNs, which has been proved sound and complete with respect to HILECOP's PN semantics.