P/poly vs NP separation based on circuit trees instead of DAGs
The class of functions computable by formulas of polynomial size is equivalent to the (nonuniform) class $\mathsf{NC}^1$ of functions computable by (bounded fanin/fanout) circuits of logarithmic depth. Proving the two implications is a nice exercise. In one direction, you can recursively "untangle" each level of a circuit by creating copies of gates. This increases the size by a constant factor for each of the $O(\log n)$ levels of the circuit. The other direction is proven by balancing the tree of the formula.

Also, $\mathsf{NC}^1$ is equivalent, by Barrington's theorem, to width 5 polynomial size branching programs. 

We know  that the uniform version of $\mathsf{NC}^1$ is contained in $\mathsf{L} \subseteq \mathsf{P}$ ($\mathsf{L}$ stands for deterministic logspace). It is not known whether any of these containments is proper AFAIK. Also it is not known whether the non-uniform $\mathsf{NC}^1$ is a proper subset of $\mathsf{P/\text{poly}}$.