enabled_when_ready (in .bs)?

[rossc719g]

I was sniffing round the source code, and was excited to see that "enabled_when_ready" was an option, but cannot seem to get it to accept it in my bs classic code? Does it actually exist, or maybe just in bsv?

[quark17]

The feature is not documented and not really tested, so in that respect it doesn't exist.

The BSV parser does accept it and BSC does do something when it sees that attribute, but it's probably not the right behavior or the full behavior. So some work would be needed.

The one file in the test suite that has this attribute is bsc.bluesim/to_systemc/getput/GetPutTest.bsv, so you can compile that and see what the behavior is. I believe that what BSC does is, when generating a module that has an enabled_when_ready attribute, to generate Verilog that uses the RDY signal anywhere it would normally use the EN signal, and to still generate the EN port, but it is unused; there is no check that submodules with such methods are always enabled when they are ready.

I believe that BSC would need to be fixed up to (1) not generate the unused EN port, (2) extend the information that is recorded about synthesized modules (what you can specify in import-BVI and what BSC internally generates for synthesized modules) to support "enabled_when_ready" as a property of action methods, and (3) have BSC check this property on submodules. And I guess also: (4) support the pragma in BH, (5) add tests to the suite, and (6) add it to the BH and BSV reference guides.

For reference, you could see how always_enabled is handled: any reference to the EN signal is replaced by True, the port is not generated, the property is recorded in the scheduling info for the synthesized module, and a check is performed in any parent module that instantiates that submodule.

The check is performed after elaboration and scheduling, in the stage AAddScheduleDefs.hs. It both checks the scheduling attributes and generates the replacements for EN signals. You can see that it is already generating the replacement, in the function handleEnableWhenReady (here). But that is applying to the top-level interface of the module being synthesized; there is no check being performed on the submodule instantiations. You'll note that handleEnableWhenReady is returning a mapping from the EN signal to its replacement expression, and it is returning has an empty list of proof obligations -- meaning that there is nothing for the SMT solver to check, unlike always_ready which requires a check that the RDY expression is always satisfied as True. For always_enabled, there is also no check needed at the top-level interface; the check occurs for the submodule instantiations, where BSC needs to check that the expression provided to the submodule EN signal will always evaluate to True. Those checks are created by handleSubmodAlwaysEnabled. A similar function will be needed for enabled_when_ready that asks the SMT solver if the RDY signal being True implies that the EN signal is True. (I guess we may want to check that it is exactly equal to the RDY signal, because we don't want the signal being asserted when not ready; but that may be unnecessary extra work, since BSC should be correctly creating the signal, and we're not doing any such check for other methods.)

The removal of the port happens later. For Verilog, that is possibly in AState, which is the start of the Verilog backend, when the internal representation of the package as rules is converted into a representation purely of signals (ports, wires, submodules). You can see that the creation of the list of input ports excludes those for which isAlwaysEn returns True. For Bluesim, the ports are dropped in a function in SimExpand, which does consider both isAlwaysEn and isEnWhenRdy! So I would guess that Bluesim does properly generate code without the EN port (and it's no surprise that the only test case is a SystemC-wrapped Bluesim example). There is also a function in SimPackage that produces the ports for a method, and that also ignores the EN signal for always-enabled and enabled-when-ready methods -- but I see that it only calls isEnWhenRdy, relying on the fact that always-enabled methods are of course also enabled-when-ready because the ready signal must always be True.

So that might be a key to how to represent this attribute in the scheduling information. Right now, the way that always-enabled is recorded is by indicating that the EN port is inhigh (see VPinhigh in VModInfo.hs). The check performed by handleSubmodAlwaysEnabled is that the signal connected to this port is always True. We could created a new attribute inrdy, say, and the check for that would be that the signal equals the associated RDY signal. But I don't think there's a need. We could instead continue to use inhigh and reinterpret it to mean that it is equivalent to the RDY signal. The function handleSubmodAlwaysEnabled is already generating a proof obligation ProveEq, that says that the enable expression must be proven equal to True; we can just change that to ProveEq of the enable expression and the RDY signal.

Anyway, adding support in BH should be trivial. And fixing up the rest of the behavior should also be easy.

[rossc719g]

Wow, incredibly thorough!

It's good to know, but I think I have an acceptable workaround for now.
In my current designs, it is easy to get a similar assurance with something that boils down to this:

  rules
    {-# ASSERT fire when enabled #-}
    "Foo": when True ==> do
      ... call my "enabled_when_ready" method here ...

At least, I think this results in the method being always enabled when ready.
At least, assuming that I have no other implicit conditions in the do other than the ones that come from the method's ready... but I am not sure how to assert that.
(Does this thinking seem right?)

As long as I am disciplined about only ever calling that method in this type of context, I should be okay.
It certainly would be nice to be able to get the extra layer of assurance from the compiler, but missing this feature is not blocking me from implementing what I need to implement... it is just making it slightly less safe. Which I think I am okay with for now.

Maybe we can mark this as a feature request somewhere, and let it go for now?

[quark17]

Maybe we can mark this as a feature request somewhere, and let it go for now?

Sounds good. I have opened Issue #607 for this. Thank you for noticing it in the code and bringing it up!