smt2: abits must be min 1

[ghost]

Fixes #2577.

I first explored trying to do away with the address line related stuff entirely here, changing the state from (Array (_ BitVec <abits>) (_ BitVec <width>)) to just (_ BitVec <width>) where abits == 0, drop the unnecessary (select ...) and (store ...) etc., but then ran into trouble where smtbmc interacts with related entities.

It would be neater to use a single-member sort for the key (is there a "Unit" equivalent?) instead of (_ BitVec 1) where we only use the #b0 index and not #b1, but this does get things working with minimally invasive changes.

Tested with regular stat, --stdt, and --stbv; it looks like there's another latent stbv bug (probably similar to #525) I noted while testing. I think it's because we makebits() for the "#final" memstate variant at both lines 1245 and 801.

[jix]

We do have a pass clean_zerowidth which is supposed to remove all zero width signals for backends which do not support them. I noticed that this does not work for smt2, as clean_zerowidth changes ABITS to 1 but leaves SIZE at 1 and smt2 computes abits as int abits = ceil_log2(mem->size) which ends up as 0 again. I'm not sure if changing this to max(1, ceil_log2(mem->size)) would make it work again or produce broken smt2 output (I only checked that it doesn't hit an assertion so far), although in that case that might point to a general issue with handling SIZE != 1 << ABITS memories in the smt2 backend.

That issue can also be avoided by running clean_zerowidth; memory_map -formal r:SIZE=1 which turns memories with only a single word into a single $ff cell, resulting in something like the first approach you described would produce without causing any trouble with smtbmc.

I would slightly prefer requiring clean_zerowidth (or automatically running it as part of write_smt2 as write_verilog does) and either fixing write_smt2 to support the output of it or alternatively requiring clean_zerowidth; memory_map -formal r:SIZE=1 (or maybe an equivalent option for clean_zerowidth) over having a check for zero every time abits is used in the smt2 backend.

I haven't run into any zero-width signals/memories so far (is that even possible with the verilog frontend?) so I might also be missing some downsides of my proposed alternatives.

[ghost]

I'm not sure if changing this to max(1, ceil_log2(mem->size)) would make it work again or produce broken smt2 output (I only checked that it doesn't hit an assertion so far), although in that case that might point to a general issue with handling SIZE != 1 << ABITS memories in the smt2 backend.

This is kinda essentially what this PR does anyway — I'm forcing a minimum of 1 (which means it uses a 1-length bitvector for the address line) and then always using 0 for the index.

I've investigated trying this instead, and you know what? It works perfectly, and does exactly what I was trying to do here but with that much less code.

Because abits == 1, the generated logic uses a (_ BitVec 1) for the address line, same as I do. Without anything extra, we'd still assert, but because we call addr_sig.extend_u0(abits) in all cases before attempting get_bv(addr_sig), the signal gets padded with a constant S0, meaning the logic for the address line calculation is written out as #b0:

yosys/backends/smt2/smt2.cc

Lines 375 to 381 in 8b2a001

	if (sig[i].wire == nullptr) {
	while (i+j < GetSize(sig) && sig[i+j].wire == nullptr) j++;
	subexpr.push_back("#b");
	for (int k = i+j-1; k >= i; k--)
	subexpr.back() += sig[k] == RTLIL::State::S1 ? "1" : "0";
	continue;
	}

I've tested this with my test cases, and the generated logic is the same as this PR currently is (modulo slightly different comments), and it works correctly:

(define-fun |in_fifo_m:R0A storage| ((state |in_fifo_s|)) (_ BitVec 1) #b0) ; 1'0
; ...
(define-fun |in_fifo_m:W0A storage| ((state |in_fifo_s|)) (_ BitVec 1) #b0) ; 1'0

Given how simple this fix is, and how the code seems to already anticipate(/expect!) it with the zero-padding already being done, I'm inclined to suggest this is probably the fix.

I'm not sure if clean_zerowidth angle would end up being more maintainable going forward — likewise, I can't foretell the implications of the memory_map call and how it might interact with various modes of write_smt2 (i.e. default vs stbv vs stdv).

I haven't run into any zero-width signals/memories so far (is that even possible with the verilog frontend?) so I might also be missing some downsides of my proposed alternatives.

I'm a bit of a noob so take my observations with a grain of salt, but quite possibly not! The ultimate cause of this is a memory [...] size 1, which has no address given it only has a single entry. It is therefore barely a memory and probably has no real representation in input Verilog; it's being generated from a FIFO in Amaranth and so things would change a lot in how it all gets synthesised once I bump up the size there.

[ghost]

I've force-pushed this PR to have the suggested fix; it's at least strictly better than what it was.