FBD (Function Block Diagram) is one of the widely used PLC (Programmable Logic Controller) programming languages in plant automation industry. Many vendors and products have their own forms and formats, which are not compatible with others. Formal verification techniques and tools for FBDs should have provided vendor- and product-specific versions. PLCopen, a vendor/product independent worldwide association, provides a standardized way to define FBDs in an XML format. This paper proposes a CASE tool, FBDtoVerilog, which translates the PLCopen-FBDs into Verilog programs. Verilog is an input programming language for formal verification tools such as VIS (Verification with Interaction and Synthesis). It had been efficiently used as an input front-end of formal verifications, when developing software controllers of nuclear power plants in Korea. We demonstrate its usefulness and effectiveness with a prototype version of FBDs which had developed for APR-1400 nuclear power reactor in Korea.