This research is on formal analysis of the scheduling problem in high-level synthesis. Problems being addressed are: (1) finding the length of the control step (clock estimation); (2) determining the type of functional unit that will perform each operation (type mapping); (3) computing the lower bound on overall schedule length; and (4) estimating the lower bound on the number of functional units.