Arithmetic - Absolute value

I constructed a circuit that calculates the absolute value of a signed 4-bit number in two's complement

Then the second question of the exercise was to show the correctness of my circuit using the definitions of two's complement representation [.] and the binary representation (.)! With a possibility to use the lemma rule

$$2^n = 1 + \sum_{i=0}^{n-1} 2^i$$

and the definition ¬x = (1 − x).

How am I supposed to verify this circuit using these 2 rules ?

• Looks way too complicated. Why haven't you just draw a truth table and implemented with gates (or muxes, which is easier)? – Eugene Sh. Mar 29 at 20:46
• I know right. I could have done it with truth table and so on but this looked faster to me . The real question is how to use these 2 rules above to prove my circuit ? – Gaston Mar 29 at 21:21
• Maybe a better question is why you want to use these two rules to verify your circuit, instead of using truth tables or even simulations? And can you clarify the little block in the upper left? Where does its input come from? – Elliot Alderson Mar 29 at 22:03
• Ah, so this is a homework problem. We will expect you to do a substantial amount of the work yourself. Then show us all of your work and ask a specific question. – Elliot Alderson Mar 29 at 22:16
• All logic can be tested with a vector table if you can define the truth table. – Tony Stewart EE75 Mar 29 at 22:20