Removed WIP designator for now: these properties do not correctly handle cores with an asynchronous reset, but this can be added later.

Back to draft again: the current reset handling is probably broken so I'll want to fix this and address #4 at the same time.

#4 has been fixed but all this needs review before merging.

One more thing - per this convo with Strike we could use default values for optional signals in places where it makes sense (not sure where that might be tho). I did verify this works in Yosys.

@awygle Addressing your global comments:

• "We don't have anything in here for interconnect, which we probably should at some point." Properties for that type of thing are tracked in Create AXI-Stream processing core properties #6, and example cores (such as an actual interconnect) are tracked in Write example AXI-Stream cores #5. The properties in this PR are for isolated interfaces, and I believe properties spanning multiple interfaces (e.g. interconnect properties) should be written separately.
• "We should include "AXI4" and "Version 1.0 Revision A" somehow, for tracking purposes." Added in e19f039.
• "We should actually verify some IP with this, and correspondingly, we should have another state in our README state machine for 'we wrote properties but haven't verified anything with them yet' (and then this PR should update the README to put AXI-Stream in that state)." README has been updated, and writing example cores is tracked in Write example AXI-Stream cores #5. I also have some simple cores locally that I've been using to test these properties, but they aren't in a state that's ready to be pushed to GitHub yet.

Comments from Echo on the Discord (@dicta):

hey, just wanted to poke you with a couple thoughts regarding your AXI4-Stream properties PR:

• There's some fun interactions with the tlast signal and tid/tdest: If tlast is being used by a master, tid/tdest can change after 1) a reset, or 2) after tlast has been asserted during a clock when data has been transferred, but otherwise must remain steady over the duration of a packet. This is section 2.5 of the standard. Slaves, on the other hand, are supposed to be able to deal with streams being interleaved so there's not a matching requirement there. I think the best way to reason about this is to create a flag indicating whether it's acceptable for a new packet to be started, and require that the master's tid/tdest be stable in all other cases.
• I'm not sure if you're just looking at verifying individual modules or looking at a bus as a whole (including interconnects), but there's some important bus properties that probably should be included. The easy one is that (again for packetized interfaces using tkeep), the number of clocks at the master where tready && tvalid && tkeep must be equal to the number of clocks at the slave where tready && tvalid && tkeep: i.e. nothing in the middle of the bus is allowed to merge/split packets. The harder one to define properties for is that transfers must not arrive out-of-order. [I guess maybe time to go look at some AXI4/AXI4-Lite properties and see how that's done there...]

As stated on one of the code reviews earlier, I plan to focus on isolated interfaces first and then create a combined property set in a separate PR that includes stuff like the second bullet point. The first bullet point is something I'll need to recheck and to add to the property set if it's missing.