|
I'm trying to write a bus-width narrower and I'm having trouble getting the provisos to line up.? My write request struct and a stripped down version of my "narrower" are as follows:
?
typedef struct {
? ?Bit#(awidth) addr; // must be aligned, ie the low `size` bits must be 0.
? ?Bit#(TLog#(TAdd#(TLog#(dbytes),1))) size;
? ?Vector#(dbytes, Bit#(8)) data;
} WriteReq#(numeric type awidth, numeric type dbytes) deriving (Bits, FShow);
?
interface Narrower#(numeric type awidth, numeric type dbytes_wide, numeric type dbytes_narrow);
? ?interface Put#(WriteReq#(awidth, dbytes_wide)) wide;
? ?interface Get#(WriteReq#(awidth, dbytes_narrow)) narrow;
endinterface
?
module mkNarrower(Narrower#(awidth, dbytes_wide, dbytes_narrow))
? ?provisos (Mul#(dbytes_narrow, max_beats, dbytes_wide),
? ? ? ? ? ? ?NumAlias#(TExp#(log2_wide), dbytes_wide),
? ? ? ? ? ? ?NumAlias#(TExp#(log2_narrow), dbytes_narrow),
? ? ? ? ? ? ?Add#(a__, log2_wide, awidth),
? ? ? ? ? ? ?Add#(b__, TLog#(TAdd#(TLog#(TExp#(log2_narrow)), 1)),
? ? ? ? ? ? ? ? ? ? ? ?TLog#(TAdd#(TLog#(TExp#(log2_wide)), 1)))
? ? ? );
? ? ...
endmodule
?
The provisos involving a__ and b__ were suggested to bsc to get the module to typecheck.? I added the other provisos to give names to various quantities.? This typechecks.? But when I try to instantiate it with concrete parameters:
?
Narrower#(32, 128, 32) n <- mkNarrower;
?
I get the following errors:
?
Error: "Narrowing.bsv", line 73, column 8: (T0031)
? The provisos for this expression could not be resolved because there are no
? instances of the form:
? ? Mul#(TExp#(a__), b__, TExp#(c__))
? The proviso was implied by expressions at the following positions:
? ? "Narrowing.bsv", line 74, column 32
Error: "Narrowing.bsv", line 73, column 8: (T0031)
? The provisos for this expression could not be resolved because there are no
? instances of the form:
? ? Add#(d__, c__, 32)
? The proviso was implied by expressions at the following positions:
? ? "Narrowing.bsv", line 74, column 32
Error: "Narrowing.bsv", line 73, column 8: (T0031)
? The provisos for this expression could not be resolved because there are no
? instances of the form:
? ? Add#(e__, TLog#(TAdd#(TLog#(TExp#(a__)), 1)), TLog#(TAdd#(TLog#(TExp#(c__)), 1)))
? The proviso was implied by expressions at the following positions:
? ? "Narrowing.bsv", line 74, column 32
Error: "Narrowing.bsv", line 73, column 8: (T0131)
? The numeric types `TExp#(c__)' and `128' could not be shown to be equal.
? This equality was required at the following position:
? ? "Narrowing.bsv", line 74, column 32
Error: "Narrowing.bsv", line 73, column 8: (T0131)
? The numeric types `TExp#(a__)' and `32' could not be shown to be equal.
? This equality was required at the following position:
? ? "Narrowing.bsv", line 74, column 32
?
It looks like the root problem is that bsc doesn't recognize that 32 and 128 are exact powers of two and hence a__ and c__ have to be 5 and 7 (the last two errors).? (I used NumAlias#(TExp#(_),_) instead of Log#(_,_) because I only want widths that are an exact powers of two.)? But I haven't been able to figure out any other formulation of the provisos that let bsc discover what it needs to know.
?
Any suggestions would be greatly appreciated.
?
-William
?
|
I figured out something that works but I'm not 100% happy with it.? I defined an extend/truncate function like I've seen discussed in other posts:
?
function x#(n) ext_trunc(x#(m) val)
? ?provisos (BitExtend#(m, TAdd#(n,m), x),
? ? ? ? ? ? ?BitExtend#(n, TAdd#(n,m), x));
? ?x#(TAdd#(n,m)) temp = extend(val);
? ?return truncate(temp);
endfunction
?
Then after replacing all my calls to truncate() with ext_trunc(), the need for most of the provisos disappeared and I could just use:
?
provisos (Mul#(dbytes_narrow, max_beats, dbytes_wide),
? ? ? ? ? Log#(dbytes_wide, log2_wide),
? ? ? ? ? Log#(dbytes_narrow, log2_narrow));
?
This no longer disallows non-power-of-two widths at typecheck time, and I liked having assumptions like that statically checked.? But I guess there is no real loss moving the checking from typecheck-time to Assert::staticAssert() elaboration time.
?
-William
?
?
?
?
|
Sorry that you've had difficulty with provisos!? There are a few issues here, but a core one is this: ? NumAlias#(TExp#(log2_wide), dbytes_wide),
BSC can only work forward from what it knows in the context.? The context fills in the base types for the function or module, which in the case of "mkNarrower" are the types "awidth", "dbytes_wide", and "dbytes_narrow".? Any new variables introduced in the provisos need to be computable from the base types, aka dependencies of the base types.? BSC should be good about telling you if you've written a proviso which is ambiguous because a variable can't be worked out (isn't a dependency).? For example, "Log#(n, awidth)" would not be accepted, because "n" is not uniquely determined just by knowing "awidth".? This is expressed in the declaration for a typeclass, using the "dependencies" clause, and "Log#(a,b)" is declared as "b" depending on "a" (not the other way around).
In your NumAlias proviso, "dbytes_wide" is known and "log2_wide" is a new variable which needs to be computed.? This only works if BSC considers the variable of TExp to dependent on the return type.? It's possible that there is a bug there -- for example, there are open bugs #311 and #312 which are about the fact that BSC doesn't reduce or unify some type constructors.
My suggestion is to avoid using TExp (or any type constructor) to compute backwards.? Instead, use the related typeclass.? In this case, that's Log, which doesn't by itself enforce a power of two.? Instead, you'd need to add an additional proviso to assert that.? For example:
Log#(dbytes_wide, log2_wide), Log#(TAdd#(dbytes_wide,1), TAdd#(log2_wide,1)), Log#(dbytes_narrow, log2_narrow), Log#(TAdd#(dbytes_narrow,1),TAdd#(log2_narrow,1))
If I replace the NumAlias with that, BSC figures it out.
However, I'm still concerned about this field of the struct: ? Bit#(TLog#(TAdd#(TLog#(dbytes),1))) size;
Why is this field take the log of a log?? Shouldn't there be just one log? ?(Also, TLog is defined as the ceiling, so do you need to be adding one?)
As for the provisos:
Add#(a__, log2_wide, awidth),
Add#(b__, TLog#(TAdd#(TLog#(TExp#(log2_narrow)), 1)),
? ? ? ? ? TLog#(TAdd#(TLog#(TExp#(log2_wide)), 1)))
It would help to know what expression caused BSC to recommend these provisos.
The first one is probably because you are taking a value of size "log2_wide" and extending it in some way into a value of size "awidth".? BSC knows that "log2_wide" is less than "dbytes_wide", but there seems to be nothing about how "awidth" is related to anything else.? So a proviso of some kind would be needed, to indicate that "log2_wide" will fit in "awidth", if you have a subexpression that is attempting to do that.
The second proviso is very odd, though, and I would suggest that you not just blindly add a proviso that BSC says is needed, but figure out why it thinks it needs it and whether there's some better way of expressing it.? I would guess that this proviso is coming from an expression using the "size" field of WriteReq, because it has the same double log.? There's no reason to write "TExp#(TLog#(t))", you can just replace it with "t", I would assume.? This proviso really just seems to be saying that "log2_narrow" is equal to or less than "log2_wide", so I'd replace it with a proviso that says that, "Add#(_diff, log2_narrow, log2_wide)" and see if that's sufficient.
However, I'd guess that you are extending a narrow "size" field to get a wide "size" field, which is why the proviso was requested, and specifically BSC needs to know what number of bits of difference there is between the two sizes (the "b__" variable), because it would need to create the padding of that size (probably).? Provisos are used both to (1) put a requirement on the caller and to (2) figure out sizes that are needed internally in constructing the logic.? BSC is good at discharging provisos of the first kind, because it can use the SMT solver to check that provisos with no free variables are satisfiable.? But when a proviso is being used to discover a size (like "b__"), that's a free variable, and BSC currently has a limitation that the SMT solver can't be used to learn new values (just answer yes/no questions about solvability).? There is a proposal of how to improve BSC to do this, though, which is filed as GitHub Issue #318.? The limitation just means that BSC needs extra provisos to specified, that it should be able to work out for itself, so it's just about verbosity.
Does any of that help?? It sounds like you might have two separate issues: the extend/truncate and the power of two, and hopefully the Log/Add provisos that I showed above should indicate how to solve the power-of-two question.? For the extend issues: One, note that the "BUtils" library in BSC should already have a function like your "ext_trunc" (like "cExtend").? But, two, I would avoid using it if your code really is implying a size relationship between "awidth" and "log2_wide", and just put an appropriate Add proviso on the module.
J
|
Oh, three thoughts I had after:
One, I was wrong when I said that TExp#(TLog#(n)) is just n. That's only true if n is a power of two.
Two, it would be a reasonable enhancement request to add a IsPowerOfTwo#(n) typeclass, which you could use in place of the Log/Add proviso.? Or, perhaps the right thing is to add an Exp#(m,n) typeclass, where dependencies go in both directions and which implies that n is a power of two.
Three, it's possible that BSC's rules for numeric provisos is just missing a rule for NumAlias#(TExp#(m),n) when n is a known power of two, that learns that m equals TLog#(n).? That would be easy to add for constant values of n, like 128, in "genNumEqInsts" in "src/comp/StdPrel.hs".? More general rules could be added if Exp#(m,n) or IsPowerOfTwo#(n) existed, where the NumAlias would discharge by being replaced by instances of those (and possibly learning that m equals TLog#(n)).
Julie
|
Here is some code for a PowerOfTwo type class.? I find it useful for many modules where bit width requires this assumption.
Ed.
//////////////////////////////////////////////////////////////////////////////// /// Power of 2 typeclass
////////////////////////////////////////////////////////////////////////////////
typeclass PowerOfTwo#(numeric type n);
endtypeclass
?
instance PowerOfTwo#(1); endinstance
instance PowerOfTwo#(n)
? ?provisos( Mul#(x,2,n), PowerOfTwo#(x) );
endinstance?
Oh, three thoughts I had after:
One, I was wrong when I said that TExp#(TLog#(n)) is just n. That's only true if n is a power of two.
Two, it would be a reasonable enhancement request to add a IsPowerOfTwo#(n) typeclass, which you could use in place of the Log/Add proviso.? Or, perhaps the right thing is to add an Exp#(m,n) typeclass, where dependencies go in both directions and which implies that n is a power of two.
Three, it's possible that BSC's rules for numeric provisos is just missing a rule for NumAlias#(TExp#(m),n) when n is a known power of two, that learns that m equals TLog#(n).? That would be easy to add for constant values of n, like 128, in "genNumEqInsts" in "src/comp/StdPrel.hs".? More general rules could be added if Exp#(m,n) or IsPowerOfTwo#(n) existed, where the NumAlias would discharge by being replaced by instances of those (and possibly learning that m equals TLog#(n)).
Julie
|
Thanks, Ed!? Making a built-in typeclass would still have some benefits, it's worth noting.? The SMT solver won't know anything about your user-defined typeclass, so it won't be able to use that knowledge to resolve provisos and might require you to explicitly include them.? And error messages might be able to be reported better.
Here is some code for a PowerOfTwo type class.? I find it useful for many modules where bit width requires this assumption.
Ed.
//////////////////////////////////////////////////////////////////////////////// /// Power of 2 typeclass
////////////////////////////////////////////////////////////////////////////////
typeclass PowerOfTwo#(numeric type n);
endtypeclass
?
instance PowerOfTwo#(1); endinstance
instance PowerOfTwo#(n)
? ?provisos( Mul#(x,2,n), PowerOfTwo#(x) );
endinstance?
?
|
Thank you the detailed response!? It has greatly enhanced my understanding of how BSC actually leverages provisos.? The key bit was this:
?
BSC can only work forward from what it knows in the context.
?
I had been assuming something much more magic: that it would collect all the provisos and the constraints imposed by type checking and solve them simultaneously.? (At some time in the past, I tried implementing such an SMT enhanced type-checker but never figured out how I could get useful error messages out of its "unsat" result.)? If I'm interpreting what you said correctly, BSC just works incrementally one provisos at a time to solve for unknown type variables and uses the SMT engine just to verify that polymorphic instantiations are possible with the provisos in the context but doesn't use the SMT engine to solve round-about inter-dependencies between multiple provisos.
?
Bit#(TLog#(TAdd#(TLog#(dbytes),1))) size;
?
Why is this field take the log of a log?? Shouldn't there be just one log? ?(Also, TLog is defined as the ceiling, so do you need to be adding one?)
?
My bus is dbytes wide.? An individual transaction can utilize 1..dbytes (inclusive) bytes.? That gives us the first log and the +1 to cover the inclusive.? But I only allow power of two transactions, so size holds the log2 of the number of bytes--hence the second TLog.? My design using the real thing from which I extracted this example has a 128 bit memory bus and a 32 bit peripheral bus.? For the 128 bit bus, size can be log2(1)...log2(16) aka 0..4 (inclusive) and needs log2(4+1)=3 bits.? Similarly, the 32 bit bus can have sizes from log2(1)...log2(4) aka 0..2 and needs 2 bits.? (Same as AXI's size fields.)
?
The first one [Add#(a__, log2_wide, awidth)] is probably because you are taking a value of size "log2_wide" and extending it in some way into a value of size "awidth"
?
It is indeed exactly as you conjectured.? I was using log2_wide to determine the number of low bits in the address to use when selecting the relevant byte lanes.? I was surprised that BSC was mixing address constraints with data constraints, but when I looked at the code that BSC referenced (something like addr[log2_wide-1:0]), it made sense.??
?
The second proviso [Add#(b__, TLog#(TAdd#(TLog#(TExp#(log2_narrow)), 1)), TLog#(TAdd#(TLog#(TExp#(log2_wide)), 1)))] is very odd, though, and I would suggest that you not just blindly add a proviso that BSC says is needed, but figure out why it thinks it needs it and whether there's some better way of expressing it.? I would guess that this proviso is coming from an expression using the "size" field of WriteReq, because it has the same double log.? There's no reason to write "TExp#(TLog#(t))", you can just replace it with "t", I would assume.? This proviso really just seems to be saying that "log2_narrow" is equal to or less than "log2_wide", so I'd replace it with a proviso that says that, "Add#(_diff, log2_narrow, log2_wide)" and see if that's sufficient.
?
This was a direct result of assigning truncate(wide_size) to narrow_size.? If the transaction on the wide bus fit on the narrow bus, the size gets forwarded unchanged.? If the transaction doesn't fit, it gets split into size_in_bytes/dbytes_narrow transactions.? The second and third term of that Add#() are exactly the argument and result types of that truncate.? I did try some provisos along the lines of Add#(dbytes_narrow, ___, dbytes_wide)--which I'm pretty sure implies that more complicated provisos--but BSC wasn't able to leverage them to discharge the truncate requirements.? (And indeed, I never blindly copy provisos from BSC output because I've had way too many cases of my actual problem being a typo (e.g. bytes vs dbytes) in a type variable and BSC's suggestions were based on the unwarranted assumption that the preceding provisos were sound.)
?
For the extend issues: One, note that the "BUtils" library in BSC should already have a function like your "ext_trunc" (like "cExtend").? But, two, I would avoid using it if your code really is implying a size relationship between "awidth" and "log2_wide", and just put an appropriate Add proviso on the module.
?
So that is where it was hiding!? I knew I had seen it somewhere but since it was easy enough to replicate I didn't look very hard.? And yeah, I wasn't happy with the sloppiness/hackiness of just disabling the static type safety of the original.
?
Thank you again for your response.
?
-William
?
?
?
|
Julie Schwartz