Logical characterization of $NC^1$ Morioka in his 2005 dissertation [1] referenced "On Uniformity within $NC^1$" by 
Barrington, Immerman, and Straubing. Using the following statement:


  Every $\mathbf{NC^1}$-predicate is computed by a Dlogtime-uniform family of polynomial-size propositional formulas


This sentence is essential to defining a reduction from an $\mathbf{NC^1}$ function to the $\Sigma_1^q$-witnessing problem for $G_0$, however I'm not able to understand how this statement was reached from the original paper, either I'm missing something important here or my expertise in circuit complexity is just not enough, can someone intuitively explain how this sentence came to be?
Morioka considers uniform versions of his circuit classes:


  Throughout this paper we write $\mathbf{NC^1}$ to mean $\mathbf{Dlogtime}$-uniform $\mathbf{NC^1}$, which is equivalent to the class $\mathbf{Alogtime}$ of languages accepted by an alternating Turing machine in $O(\log n)$ time.


The paper you mention should imply the equivalence of these two definitions. The statement you quote, however, is just true by definition.