Reducing k Vertex Cover to SAT (last clause problem)
First of all, the problem of vertex cover asks whether there is a vertex cover with at most $k$ vertices. Fortunately, there is a vertex cover with at most $k$ vertices iff there is one with exactly $k$ vertices, so your choice of looking for a vertex cover of size exactly $k$ is fine.

Second, you need to describe everything as a CNF, that is, a collection of clauses. You can't just include
$$
y_{i,j} \equiv (y_{i-1,j} \land \lnot v_i) \lor (y_{i-1,j-1} \land v_i).
$$
Fortunately, every formula on $t$ variables can be written as a CNF having at most $2^t$ clauses (exercise), so you can turn this formula into a CNF of constant size.

Finally, you say that you "should write $y_{nk}$ in terms of $v_1 \cdots v_k$", but there is no such requirement. An instance of SAT is just a bunch of clauses. You can use whatever variables and clauses you want; the distinction between original variables $v_i$ and extension variables $y_{i,j}$ is all in your head. If you want to force $y_{n,k}$ to be true, you can just add a singleton clause $y_{n,k}$.