This contribution presents a new method for the formal verification of

register binding in the high-level synthesis process. The approach combines

the well-known methods model checking and symbolic simulation. By model

checking an abstraction of the design, possible conflicts are identified at an

preliminary stage. Whether the supposed conflicts can occur during a

computation or if they are only devoted on logically impossible paths, is

checked by means of symbolic simulation. The verification is performed

automatically and independent of the applied procedure of register binding.

Moreover this essay supplies a framework for combining model checking with

symbolic simulation.