PDA accepting all words not of the form $b^na^n$ I am studying Automata theory. DFAs and NFAs seem pretty straightforward to me, but I don't quite understand how to design push-down automata for context-free languages.
If I have context-free language where the
input  alphabet is $\{a,b\}$
$L = \{w \text{ where }w\text{ is NOT of the form }b^n a^n\}$
How would I design a push-down automata for it? What are the steps I would need to take, and what would it look like (formal description)?
The PDA has two main states:

No $a$ has been encountered.
Some $a$ has been encountered.

While in the first state, it pushes $B$ onto the stack for any $b$ it encounters. It moves to the second state when encountering an $a$, at which point it removes $B$ from the stack for any $a$ it encounters (including the first $a$). If it ever realizes that it has seen more $a$s than $b$s, or if it encounters $b$ again, it can immediately accept (depending on your model, you might have to read the remainder of the input). After finishing reading the entire input, if the stack contains at least one $B$ then it accepts, and otherwise it rejects. You can implement this by requiring the PDA to pop at least one $B$ before accepting.
Formally describing this PDA depends on the exact definition of PDAs in your class, and in any case, it is an exercise which is best for you to do on your own.