P/poly vs NP separation based on circuit trees instead of DAGs there are various theorems that relate major complexity class separations to circuit family DAGs sizes, in particular for P/poly vs NP. in contrast,


  are there theorems/conjectures that relate P/poly vs NP separation to the size of circuit trees (aka formulas)?


note of course that CNF/SAT is a boolean formula. an example in this form would be something like if a CNF circuit family $C_n$ requires size $\Omega(g(n))$ clauses to compute function $f$ (alternately, can compute $f'$ in $O(g'(n))$ clauses) then NP $\not\subset$ P/poly, but the question is not limited to CNF &amp; is asking about formulas in general. ([1] is a somewhat related question) 

[1] Complexity of converting a boolean circuit to a boolean formula
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}}$.