Logical characterization of $NC^1$

Question

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?