Verilog is one of the two most popular high-level hardware description languages. Many libraries of useful designs, such as communication protocols and compression algorithms, are available in Verilog. These designs could be useful to designers of real-time and reactive systems if they could be translated into the languages used for such designs. Synchronous languages are particularly useful for describing the control of real-time embedded systems. Their rigorous mathematical semantics allows programmers to develop critical software faster and more reliably Synchronous languages also enable validation and verification of the developed systems. Veriest is an automatic translator that converts synthesizable Verilog designs into the synchronous language Esterel. The translation into a synchronous language can expose hidden flaws in the original design, including subtle race conditions. In addition, the extensive libraries of verified Verilog designs can now be reused in synchronous designs. Verilog and Esterel have different models and features, complicating the translation. For example, Verilog has flexible data types and operators for dealing with data buses of varying widths; it also supports three-state logic, which has no equivalent in languages not meant to describe hardware. Veriest creates functions in the hosting language (usually C) to represent concisely such features of Verilog that are not native to Esterel.