Relationship between circuit size and formula size in Sipser text

Question

The Sipser text (3rd edition) contains a proof that 3-SAT is NP-Complete based on Boolean circuits. Part of the proof contains the remark that the reduction from the circuit to the Boolean formula can be done in polynomial time.

First question: is it correct to say that if a circuit C of polynomial size exists, then there must exist a formula $\varphi$ of polynomial size where C is satisfiable if and only if $\varphi$ is satisfiable?

Second question: is the Boolean formula $\varphi$ still of polynomial size if C is of polynomial size and C is derived from a deterministic Turing machine M? This seems to be described in the proof of the earlier theorem in Sipser where (by building C from a tableau of M) it is shown that if $\mbox{A $\in$ TIME$(t(n))$ for $t(n) \geq n$ and $n \in \mathbb{N}$}$ then A has circuit complexity $O(t^2(n))$.

Answer 1

Yes, that's correct. See the Tseitin transform, which describes how. It doesn't matter how the circuit $C$ was constructed.