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

*From*: Amjad Ali <amjad.hamdi.ali@xxxxxxxxx>*Date*: Sat, 5 Nov 2022 22:57:27 -0700 (PDT)

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.

--

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.

**Follow-Ups**:

- Prev by Date:
**Re: [tlaplus] Represent an arbitrary 32 bit number in binary form** - Next by Date:
**Re: [tlaplus] How to prove my "compare" function on 4-bit binary numbers is correct?** - Previous by thread:
**Re: [tlaplus] Represent an arbitrary 32 bit number in binary form** - Next by thread:
**Re: [tlaplus] How to prove my "compare" function on 4-bit binary numbers is correct?** - Index(es):