I simply do not believe you

For the former it's useful when there's already a well-defined contract at some interface, like "this bus interface follows these basic AHB5 manager rules" or "if x_valid is asserted, it remains asserted until x_ready is asserted, and the other x_foobar are stable during that time" or "a FIFO is never both empty and full".

Simple properties + exhaustive checking is good bang-for-buck because it often teases out subtle tangential issues without having to write checks for implementation details. This isn't "formal verification" per se but using formal checks in a lightweight way to help find bugs and inconsistencies in your design.

If you're familiar with the Z3 Python API, you'll find the CVC5 one familiar.

Caveat: I mostly do logic design, maybe there are some software verification tasks where Z3 comes out ahead. I've never seen one though.

...Why? That advice is universal for a reason. The side adventure with Claude Code strikes me as a distraction from the fact that there is a hard thing you want to do but are avoiding because it's hard.

Wrt inference servers: sure, it's not cost-effective to have such a huge CPU die and a bunch of media accelerators on the GPU die if you just care about raw compute for inference and training. Apple SoCs are not tuned for that market, nor do they sell into it. I'm not building a datacentre, I'm trying to run inference on my home hardware that I also want to use for other things.

v6-M doesn't (e.g. Cortex-M0+). v7-M and v8-M do allow unaligned access on Normal memory but not on Device memory.

Unfortunately you would not be able to repurpose the LSB of jalr targets as an "x86 bit" à la Thumb because the standard requires you to ignore that bit, though of course you could enable that behaviour with a custom CSR.

T32 is a pretty good encoding but far from perfect. If they had the chance to redo it I doubt they would spend a full 1/32nd of the encoding space on asrs, for example.

If stdlib div() were promoted to a builtin one day (it currently is not in GCC afaict), and its implementation were inlined, then the compiler would recognise the common case of one side of the struct being dead, and you'd still end up with a single div/rem instruction.

The div/rem one is odd because I saw it suggested in the ISA manual, but I have yet to ever see that pattern crop up in compiled code. Usually it's just in library functions like C stdlib `div()` which returns a quotient and remainder, but why on earth are you calling that library function on a processor that has a divide instruction?

> The whole premise of fusion is predicated on the idea that it is valid for a core to transform code similar to the branchy code on the left into code similar to the branch-free code on the right.

The idea of Zicond afaict is that the compiler transforms select sequences into (usually multiple) Zicond instructions, and cores with more register ports available can fuse Zicond compounds into more complex select macro-ops. It's a 2R1W vocabulary for describing selects which require more than 2 read ports.

As an aside I evaluated Zicond on my scalar 3-stage implementation and found that at 1 CPI for ALU ops and 2-cycle taken branch cost, the branchless sequences GCC produced for Zicond were never better and sometimes worse than the equivalent branching sequence. It really does seem to be targeting bigger cores, or constant-time execution

P adds instructions like integer multiply-accumulate, which have a third register read (for rd). So, they're taking the opportunity to add a few forms of 3-register select instructions:

   MVM     Move Masked
           for each bit i:  X(rd)[i] = X(rs2)[i] ? X(rs1)[i] : X(rd)[i]

   MVMN    Move Masked Not
           for each bit i:  X(rd)[i] = X(rs2)[i] ? X(rd)[i]  : X(rs1)[i]

   MERGE   Merge
           for each bit i:  X(rd)[i] = X(rd)[i]  ? X(rs2)[i] : X(rs1)[i]

...but it's a plastic panel? I don't understand how this helps with EMC.