<mithro>
daveshah: I don't know if you saw the conversation on #vtr-dev -- at the moment vpr doesn't support multifan out carry chain patterns, so I wanted to see if I could work around it at the synthesis stage by converting Figure-B2 into Figure-A2 (see https://docs.google.com/drawings/d/1qREImoaUjWDSsnbimDu-Mig3_M9hTr-6q-zbPd2VPEM/edit)
<mithro>
ZipCPU: Is there a way to prove that my change to the SB_CARRY above is still logically equivalent?
* ZipCPU
scratches his head
<ZipCPU>
Do you have a Verilog description of your designs?
<mithro>
ZipCPU: Yes
<ZipCPU>
Are there FF's in either design, or is it strictly combinatorial?
<daveshah>
mithro: yes, that looks good
<ZipCPU>
I ask, because there's a way of proving equivalence that works for all designs ... but that I've not used (yet). "mode equiv"
<daveshah>
But please don't call it SB_CARRY, even for testing
<ZipCPU>
Ahh ... I'll let daveshah answer your question.
<daveshah>
Call it ICE_CARRY_VPR or something
<mithro>
ZipCPU: Well, I only changed the LUT/CARRY part
<daveshah>
I don't really know the equivalence check well either
<ZipCPU>
If there are no FF's, you can easily set up a proof between the inputs to the outputs.
<daveshah>
Yes
<ZipCPU>
If there are FF's, it gets more complicated--you've got to make certain that the FF states remain identical.
<daveshah>
You can simply assert that the adder works as an adder
<ZipCPU>
That would work.
* ZipCPU
was worried about hidden states within the designs
<daveshah>
No, this is all combinational
<ZipCPU>
Then that's easy.
<mithro>
daveshah: I'm a bit worried about the carry chain input mux
<daveshah>
mithro: that is unrelated to this though, I think?
<ZipCPU>
Set up a parent module, containing both children, and assert that their outputs are identical. Doubt you'd need any assumptions about the inputs.
<daveshah>
Yes, that's exactly what you want.
<mithro>
The carry unit calculates lutff_i/cout = lutff_i/in_1 + lutff_i/in_2 + lutff_(i-1)/cout > 1. In case of i=0, carry_in_mux is used as third input. carry_in_mux can be configured to be constant 0, 1 or the lutff_7/cout signal from the logic tile below.
<daveshah>
mithro: yes
<daveshah>
I know how the ice40 carries work
<mithro>
daveshah: So the CIN value needs to start at either a constant 0 or a constant 1?
<daveshah>
mithro: No, in the current flow CIN can also come from other logic
<ZipCPU>
If you are doing formal proofs, leave your inputs unconstrained
<daveshah>
In that case arachne-pnr and nextpnr insert a feed in SB_CARRY
<mithro>
How do you get CIN from the logic into the CIN pin of the SB_CARRY?
<mithro>
okay, so what does a feed in SB_CARRY look like?
<daveshah>
Either of I0/I1 tied low and CIN tied constant high, then the feed in going to either I0/I1 not tied low
<daveshah>
ie you calculate the carry part of (1+x+0)
<mithro>
daveshah: Ahh yeah - that makes sense
<mithro>
That was the trick I was missing
<daveshah>
You may also need to insert feed out cells, ie a LUT passing I3 to output
<mithro>
Yeah - VPR does that automagically without me needing to do anything
<sorear>
Why not calculate the carry part of (x+x+y), then y is don’t-care so you can start in the middle of a block
<mithro>
daveshah: The SB_CARRY feed through can only be at the bottom?
<daveshah>
Not if you use sorears solution
<mithro>
sorear: This is why I'm asking - I have a lot of holes in my knowledge :-P
digshadow has joined #yosys
<mithro>
sorear: So, with that in1/in2 have to be the same signal?
<sorear>
Yes
<daveshah>
However, I don't know whether the carry chain actually floats when carry is disabled, in which case that could cause weird electrical issues
<daveshah>
I suspect that is why we've stuck to not relying on undefined inputs
<mithro>
I think I'm understanding why all the VPR LUT+CARRY are modelled together as a unit
<daveshah>
Yes, that's much more standard
<daveshah>
That's how the ECP5 does it
<daveshah>
When you use a carry, it is a different mode to the LUT altogether
<daveshah>
It has a hard XOR from the carry chain to the output, IIRC, in that mode
<daveshah>
That is all part of the primitive, instead of the weird I3 thing in the ice40
<sorear>
Seems pretty straightforward to characterize whether a disabled carry floats
<daveshah>
Well the proper solution is to see what the vendor tools do
<mithro>
Worst comes to worst, you can just enable the carry on the tile below, right?
<daveshah>
But then you have to feed something into that...
<mithro>
As the CIN is a "don't care"
<mithro>
Oh, I understand - you need to enable *all* the carry's until you hit the carry_in mux...
<daveshah>
Tbh it's probably safe, but it's also one of those things that would be a pain to debug if it wasn't