\setlength{\unitlength}{0.00083333in}
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
{\renewcommand{\dashlinestretch}{30}
\begin{picture}(2108,687)(0,-10)
\path(12,660)(2096,660)(2096,12)
	(12,12)(12,660)
\path(79,481)(2035,481)(2035,58)
	(79,58)(79,481)
\put(994,314){\makebox(0,0)[lb]{{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}HOL}}}
\put(124,115){\makebox(0,0)[lb]{{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}$\TURNST\ \DEF{InfRise}\ \mE{clk} \IMP (\mE{Cir} \FIMP \DEF{Dev}\ f)$}}}
\put(1017,538){\makebox(0,0)[lb]{{\SetFigFont{7}{8.4}{\sfdefault}{\mddefault}{\updefault}PC}}}
\end{picture}
}