[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] How to prove my "compare" function on 4-bit binary numbers is correct?

I want to prove cmp_bv4 for all 4-bit binary numbers is correct. As seen below, a binary value of 4 bits is represented as a set of functions with domain 0-3 and range 0 and 1. Then, an xor function with domain 0 and 1 that outputs 0 if the two inputs match (or 1 other, otherwise). Finally,  cmp_bv4 takes in two 4-bit binary numbers and uses the xor function to determine if the values match. Why do this and not just use (=) ? In the machine I'm building, a comparator is not available and I need to build one from scratch.
Screen Shot 2022-11-06 at 12.43.42 AM.png

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/bcd0ac97-be4f-4b5e-b91b-d347dde2cb61n%40googlegroups.com.