$\mathsf{NC^1}$ circuit evaluation Is it known if $\mathsf{NC^1}$ circuit evaluation problem is in $\mathsf{NC^1}$? 
  How about $\mathsf{ALogTime}$ (uniform  $\mathsf{NC^1}$)?


We know that circuits of depth $k$ can be evaluated with circuits of depth $k+c$ 
where $c$ is a universal constant. 
This means circuits of depth $k\lg n + o(\lg n)$ can be evaluated by 
a circuit of depth $O(\lg n)$.
However $O(\lg n)$ doesn't contain a function that eventually dominates all functions in $O(\lg n)$.

We know that formula evaluation problem is in $\mathsf{ALogTime}$. Every $\mathsf{NC^1}$ circuit is equivalent to a Boolean formula. Can't we compute the extended connection representation of an equivalent Boolean formula from that of a given $\mathsf{NC^1}$ circuit in $\mathsf{ALogTime}$?

The extended connection representation of a circuit includes 


the number of gates in the circuit, 
the type of each gate, and 
for every gate $g$ and every path $\pi$ in the DAG of the circuit the gate reached from $g$ following path $\pi$.


A path is given by a 0/1 sequence where 0 represents moving to the left parent and 1 represents moving to the right parent. Note that the number of paths is polynomial: the length of the paths is bounded by the depth of the circuit.
As far as I know, $\mathsf{NC^1}$ evaluation is not known to be in $\mathsf{NC^1}$, and is conjectured to be outside $\mathsf{NC^1}$. See 


Emil Jerabek, "On theories of bounded arithmetic for $\mathsf{NC^1}$",  Ann. Pure Appl. Logic 2011