[SMT] Parse SMT bitvector width as signed

[TaoBi22]

Fixes an issue where SMT bitvector widths being parsed as unsigned meant that e.g. !smt.bv<-1> would wrap around and be interpreted as a 18446744073709551615-wide bitvector. The downside of this fix is that the error messages for bitvectors that are too wide become a little less clear (see the updated test) - does this still look like an ok fix to you @maerhart? Let me know if I should also drop the code that's emitting that error in the RepeatOp verifier, don't think it can be triggered after this but I may have missed a case.

[maerhart]

It might be cleaner to write a custom parser that avoids the implicit conversion (basically parsing an APInt and doing the necessary checks before converting it to uint64_t).
When creating this type in C++ you probably give it an unsigned int, so the implicit conversion to a signed int could be a bit annoying there (but also only in corner cases).
But this approach is also fine for me.

I assume something like #8062 can still happen after this change (just the bitwidth to trigger it would be smaller)?

[TaoBi22]

It might be cleaner to write a custom parser that avoids the implicit conversion (basically parsing an APInt and doing the necessary checks before converting it to uint64_t).

Agreed that would be nicer - I'll merge this for now (once CI has passed) so we have a fix in but I'll try and come back and fix it up properly at a later date. I'll make a tracking issue to remind me once this is merged (edit: #8064).

I assume something like #8062 can still happen after this change (just the bitwidth to trigger it would be smaller)?

Yes, after this fix circt-opt spits out:

hw.module @ImplicitOverflow() {
  %0 = smt.bv.constant #smt.bv<1> : !smt.bv<9223372036854775803>
}

as:

module {
  hw.module @ImplicitOverflow() {
    %c1_bv4294967291 = smt.bv.constant #smt.bv<1> : !smt.bv<4294967291>
    hw.output
  }
}