$display and registers

[RyanGlScott]

Consider this simple BH program:

package Top where

mkTop :: Module Empty
mkTop =
  module
    r :: Reg (UInt 32) <- mkReg 0

    rules
      "rule1": when (res == noReset) ==>
        $display "Hello, World"

      "rule2": when True ==>
        $display "The value of r is: %0d" r

This has two rules, both of which should run on every clock cycle. Let's compile this and simulate it for two clock cycles:

$ bsc -sim -g mkTop -u Top.bs && bsc -sim -e mkTop -o mkTop && ./mkTop -m 2
checking package dependencies
compiling Top.bs
code generation for mkTop starts
Elaborated module file created: mkTop.ba
All packages are up to date.
Bluesim object created: mkTop.{h,o}
Bluesim object created: model_mkTop.{h,o}
Simulation shared library created: mkTop.so
Simulation executable created: mkTop
Hello, World
Hello, World
The value of r is: 0

This produces some counter-intuitive results: rule1 produces two lines of output, but rule2 only produces one line of output. The only difference between the two rules is that rule2 references a register value, but rule1 does not.

If I look at the compiled Verilog output, I see this code:

  // synopsys translate_off
  always@(negedge CLK)
  begin
    #0;
    $display("Hello, World");
    if (RST_N != `BSV_RESET_VALUE)
      $display("The value of r is: %0d", $unsigned(r));
  end
  // synopsys translate_on

Which suggests that this distinction is deliberate. Is there a reason why this happens?

[mieszko]

looking at the RTL* it looks like for some reason register reads in $display at least are not allowed when the circuit is in reset:

  always@(negedge CLK)
  begin
    #0;
    $display("Hello, World");
    if (RST_N != `BSV_RESET_VALUE)   //    <--------
      $display("The value of r is: %0d", $unsigned(r));
  end

presumably there's a rationale (maybe not generating junk during reset? idk) but it looks like it's deliberate.

*after changing the first rule predicate to True, otherwise it doesn't compile

[quark17]

I think there are a couple things at play here: what BSC does when a rule has no clock/reset; and how reset is implemented, in the code generation for rules. A rule has an associated clock domain and resets, which are determined by the state that the rule touches. BSC collects the clocks and resets of all the called methods and, for example, reports an error if clocks from different domains are found. A rule that only contains $display has no method calls, so it is a degenerate case without any clocks or resets. BSC could have rejected the rule (and required the user to explicitly specify the clock and resets), but the current behavior is to pick the default clock of the module. A principle of BSC's clock support was that the common case should be easy, and that users who aren't writing multi-clock designs don't even necessarily need to know that it exists (or how it works). This is why you don't have to mention a clock or reset when writing a module, even though it does have both by default. That may be why BSC silently picks the default clock as the associated clock for a rule with only $display. I tried to see if I could find an old document from when the current clock support was added (in 2004 to 2006-ish, internally referred to as MCD), describing the design choices, but I can't find much -- and it doesn't discuss reset, probably because only enough was added to get started and it was considered a later project to come back to and get right. Rules must be associated with a clock, but they are not required to be associated with a reset. A rule can have zero, one, or multiple resets -- and if there are multiple, BSC will warn that the user needs to be sure that they know what they're doing (as we'll see). So in this case with only $display, BSC has left the rule as associated with no reset, rather than also assigning it the default reset (along with the default clock). So this is maybe a case where the single-clock/reset user is being exposed to the larger MCD/Reset capabilities, and maybe it would be better to pick the default reset for them, but I'm not sure that's the right thing to do either. At best, maybe there should be a warning about degenerate rules (that can be silenced with a flag, or we can introduce syntax for explicitly giving a clock/reset to a rule that doesn't touch state). [You can also get a rule without a reset if it only uses state without a reset, like "mkRegU"; it may even be worth warning users in that case (similar to multi-reset), particularly if the rule calls system tasks or foreign functions.] I believe the idea with reset is that a rule should not execute if the state it touches is in reset. One way this could be implemented is to have the reset signal be part of the RDY of the methods. I believe it was decided that this would introduce too much logic in the Verilog; instead, it was decied that the rule logic would still construct the EN and input signals as usual, but the submodule would just ignore the method call when in reset. If you look at the Verilog "RegN" module, for example, the register is always assigned the init value when reset, and only consults the EN/D_IN when not in reset. [This is why BSC warns when a rule has multiple resets: if some state is in reset and other state is not, part of the action will execute without the rest, which is not correct for "atomic" actions. This would not be a problem if the reset was part of the RDY, I think.] This choice to implement the reset by ignoring the EN input (rather than including in the RDY output) means that we have to do something about the system tasks (and foreign functions) that a rule calls. A rule that writes a register will appear to not fire during reset of the register, because the register won't update; but if the rule also has $display, the implementation needs to disable that display. BSC does this by adding the reset of the rule to the condition on the $display: the $display is already conditional on WILL_FIRE of the rule that it appears in, but now its WILL_FIRE && !RST. (Essentially implementing the reset-in-the-RDY implementation, but only for tasks.) (If there are multiple resets, they are all included in the condition. If a module has an internal reset that is not exported, that's tricky, but you at least get a warning or error that the module has a method on a reset that is not exported.) In your example, "rule2" has a reset, because it touches state ("r") that has a reset, and so the $display is guaraded (that is, the rule doesn't appear to execute when its state is in reset). In contrast, "rule1" has no reset, so it is free to execute on every clock cycle -- just because a reset is being asserted on some other part of the system, doesn't mean this rule needs to react to it. (And, of course, the rules execute on the edges of CLK -- not because rules in a module are just always on the module's clock, but because "rule2" uses state on that clock and is therefore associated with it, and because "rule1" has no associated clock and was therefore silently given the default clock of the module.) As I said, just enough reset support was added to make MCD work when it was added, with the intention of some day doing a proper think about reset methodology and how to support it in BSC. I doubt that ever happened, so I think we're still living with the initial good-enough support. So it's possible that BSC could be doing a lot more to check that users are making proper use of reset. If someone wanted to think on this and propose something, that'd be welcome. (While BSC could do more checking, on the other hand, that might require more explicit declarations from the user, which would be contrary to wanting to keep the common case simple. So I don't know if there are easy answers.) One thing that this discussion makes me wonder about is designs that use "mkReg" and "mkRegU": in a sense, that's mixing two different resets (RST and no reset), and BSC doesn't warn (even though, when a rule writes to both, some state will update while other state is in reset -- but at least, this is a property of the register that a user knew when they declared it). System tasks and foreign functions are like method calls with no associated reset, so maybe there's some way to unify their handling. FYI, here's some of the documents I could find on MCD, but mostly they leave out any discussion of reset: - Paper at MEMOCODE'08 on the design choice, "Reliable Design with Multiple Clock Domains": https://web.ece.ucsb.edu/its/bluespec/training/BSV/papers/Memocode06.pdf - BSV training lecture on MCD: https://github.com/BSVLang/Main/blob/master/Tutorials/BSV_Training/Reference/Lec12_Multiple_Clock_Domains.pdf

[quark17]

It's also worth noting that when you link via BSC, it drives the design with a main.v that provides a clock and a reset, and the reset signal is asserted for the first clock period. So there's an initial clock edge where rule1 is able to execute while rule2 does not (while in reset).

[RyanGlScott]

Thanks for the detailed answer! Is this an accurate summary of why the original program behaves the way it does?

1. In the first clock cycle, r is in reset, which means that rule2 (which depends on r) won't fire.
2. The reset is off on all subsequent clock cycles, so rule2 is free to fire on those cycles.
3. rule1 has no reset, and therefore can fire on the first clock cycle.
4. If I wanted to make rule1 not fire on the first clock cycle, I would need to indicate this explicitly (perhaps by setting up an explicit reset for that rule).

[quark17]

Is this an accurate summary

Yes. But note that for 4, there's no attribute or "reset_by" syntax to add a reset. The only way to do that currently is to insert the use a method with an associated reset, somewhere in the rule (that won't optimize away) -- like Mieszko showed below, by adding a read or write of a register.

Also, if I were being nit-picky, I might object to saying "r is in reset". When BSC analyzes a rule (at compile time), it is specifically looking at the method calls in the rule (the ones on synthesized submodules, that are left after elaboration). Here, rule2 includes a use of r._read, and it's the reset associated with that method which BSC picks up. A module can have multiple input and output resets, and each method can be associated with those (or with no reset at all). For mkReg, there is only one reset port, and both methods (_read and _write) are both associated with that reset, so "r is in reset" is understood.

Every synthesized module has a set of additional info that pairs with it, and that info includes information such as the resets that are associated with each method of the interface. This info is hand-written for primitive modules in the BSC libraries and BSC derives it for each module that it synthesizes; and when the user wants to import a module, they have to provide this information. So if you look at the import-BVI syntax in BSV, for importing Verilog modules, you can see all the kinds of information that can be specified. That's the info that BSC uses to do all of its analysis, so understanding the kinds of info might help in understanding BSC.

Anyway, the analysis of resets is done statically during compilation. BSC figures out all the reset signals for methods used by a rule, and that becomes part of the implicit condition of the rule, although in practice it is only used to guard the system tasks (like $display).

[mieszko]

Yeah, except I think in this case it's not the rule suddenly having a reset, it's the $display (b/c it reads a register that is in reset and its value is unavailable).

You can check this on a slight variant of your example:

mkTop =
  module
    r :: Reg (UInt 32) <- mkReg 0
    t :: Reg (UInt 32) <- mkRegU

    rules
      "rule1": when True ==> do
        $display "Hello, World"
        t := t + 1

      "rule2": when True ==>
        $display "The value of r is: %0d" r

This generates the RTL below:

  always@(posedge CLK)
  begin
      if (RST_N == `BSV_RESET_VALUE)
      begin
          r <= `BSV_ASSIGNMENT_DELAY 32'd0;
      end
      else
      begin
          if (r$EN) r <= `BSV_ASSIGNMENT_DELAY r$D_IN;
      end
  if (t$EN) t <= `BSV_ASSIGNMENT_DELAY t$D_IN;
  end

You can see that the $display is guarded but the assignment to t is not because t has no reset. You can also try to make t read r, and it still won't be guarded by a reset (I think quite reasonably).

So I guess rules are not guaranteed to be atomic under reset if they have a $display inside. Perhaps it's worth having a close look at what one would like the $display semantics to be, as Julie suggested above.

[quark17]

I think in this case it's not the rule suddenly having a reset, it's the $display

No, it's the rule.

I'm having trouble relating what you say in the text to the code that you quoted. For example, you said this:

You can see that the $display is guarded but the assignment to t is not

But the display that's in the same rule as the assignment to t is not guarded (the "Hello World" display):

always@(negedge CLK)
begin
  #0;
  $display("Hello, World");
  if (RST_N != `BSV_RESET_VALUE)
    $display("The value of r is: %0d", $unsigned(r));
end

If you want to make a code example to test the hypothesis about whether the guard on a display is only for uses by the display or if the guard includes resets from elsewhere in the rule, then you'd need to add, to the rule with "Hello World", an action that actually carries a reset -- you added a use of t, which is mkRegU and therefore has no reset. But if we change t to be mkReg 0, then we do see the display picks up the guard:

if (RST_N != `BSV_RESET_VALUE) $display("Hello, World");

So I guess rules are not guaranteed to be atomic under reset if they have a $display inside.

That doesn't follow. But, as I mentioned in my comment, using mkRegU with mkReg does lead to non-atomic behavior during reset (but the user has indicated, by picking mkRegU, that they are OK with the state element having any value when the system comes out of reset).

[mieszko]

Sorry I mistyped the example. It should be:

    rules
      "rule1": when True ==>
        $display "Hello, World"

      "rule2": when True ==> do
        $display "The value of r is: %0d" r
        t := r + 1

Then if rule2 is always fully atomic then one would expect both the $display and the assignment to t to be guarded, right? And if one were to expect the read of r to confer this dependency on reset, then one would expect that to be guarded as well.

But what you get is the $display in rule2 being executed only if out of reset:

  always@(negedge CLK)
  begin
    #0;
    $display("Hello, World");
    if (RST_N != `BSV_RESET_VALUE)
      $display("The value of r is: %0d", $unsigned(r));    // <---- guarded by ~RST_N
  end

and the update to t being carried out no matter what:

  always@(posedge CLK)
  begin
    if (RST_N == `BSV_RESET_VALUE)
      begin
        r <= `BSV_ASSIGNMENT_DELAY 32'd0;
      end
    else
      begin
        if (r$EN) r <= `BSV_ASSIGNMENT_DELAY r$D_IN;
      end
    if (t$EN) t <= `BSV_ASSIGNMENT_DELAY t$D_IN;     // <---- not dependent on RST_N
  end

So it's seems that it's not the full rule that is guarded by reset?

[quark17]

So it's seems that it's not the full rule that is guarded by reset?

Yes, see my original comment. A design choice is being made as to how to implement reset in the generated Verilog. One way to do this would be for the RST to become part of the rule condition (or the method RDY), and that would guard all the actions of the rule by feeding RST in to the EN signals of the action methods that it calls. But it was decided that this would introduce too much logic or long paths into the design; instead, each submodule would handle the reset by combining its RST with the EN input (essentially ignoring the method call when in reset). This alternate code generation only works if all the submodules have access to the same RST signal, for their methods; that's why BSC gives a warning if it discovers that a rule has method calls associated with multiple resets. (If all submodules have the same RST, then the rule condition would only pick up one RST, and so AND'ing the external RST into all of the EN signals is the same as AND'ing the local RST into the EN inside each module.) But, as you and I are noticing, if some methods have a RST and some methods have "no reset", then that is also a "multiple reset" situation, in some sense.

No $display is needed to create that situation. Consider a rule that writes to mkReg and mkRegU:

"ruleA": when True ==> do
  t := t + 1
  r := r + 1

This rule is considered as having one reset -- the RST of r -- because BSC allows "no reset" methods to be called alongside methods with a reset. Rather than implementing this rule by (a) having mkReg include RST in the expression for RDY__write or by having BSC manually insert RST into the CAN_FIRE or WILL_FIRE of r, and thus (b) having the EN__write to both submodules include RST in its expression ... we instead expect each module to enforce this by locally applying its own RST with the EN__write port coming in. This works for mkReg which has a RST port, but doesn't for mkRegU which has no reset port to include.

But that's the whole point of mkRegU: The user is OK with any value being in the register while other parts of the system are being reset. The user could have instantiated mkReg, but they want to improve the logic/routing, and they know that it is OK to use mkRegU, because logic that does get reset will initiate eventual writing of a good value. This isn't something that BSC can currently check, so some methodology is needed, if you do this (and maybe BSC or BSC tools could do more to help in this case -- for example, outputting proof obligations for the designer to check).

(As an aside, I would use the keyword action instead of do. I don't think there's a chance of type ambiguity here, so it doesn't matter, unless maybe it helps naive syntax highlighters.)

[mieszko]

I understand why there is no reset on the assignment to t, and I think the design decision there is right in terms the synthesizable RTL one wants to generate (like in your example).

But I think the behaviour is inconsistent with the semantics as explained. You wrote that

a rule should not execute if the state it touches is in reset

so let's try that out.

There are two ways to interpret "touches":

1. If "touches" means writes (or anything -> Action), then having t := r + 1 unguarded is expected because r is only being read. But then $display is not writing r either.

2. If touches means reads as well (any method), then the guarded $display behaviour is fine, but then t := r + 1 is unexpected.

In any case, I think the practical issue is that the overall behaviour is unexpected: some $displays show up and others don't, and it requires some mental gymnastics to figure out what is happening (evidenced by this discussion).

I wonder if it wouldn't be be more reasonable™ to define behaviour based on $display itself, for example either

• allow all $displays to fire during reset regardless of what they inspect, or

• prevent all $displays from firing during any reset of the module.

As I said I personally think it's worth thinking about the semantics of things like $display.

[quark17]

Of the two definitions for "touches", the one that BSC uses is the second one: BSC collects the reset of every method (both values and actions) in the rule.

As you say, for that definition, the behavior of $display is fine: system tasks execute when and only when the rule executes. It is just the write to the mkRegU module that is not behaving as you expect, because you say it breaks atomicity. But I don't think we have to view it that way.

Whatever formalism you use to model the reset value for mkReg -- say, an internal rule which, on reset, fires after any write and overwrites the written value with the reset value -- that same formalism can be applied to mkRegU: It is a module that, on reset, is witten with a non-deterministic value. (The fact that the internals of the module implement that by using the value coming in on the D_IN port is just an optimization.)

And I think that model jibes with the intuition we have when we use it: we instantiated mkRegU because we don't care what value it has during reset.

(If for some reason you want a module that does preserve its value during reset, but doesn't have an initial value, you could define a new module, mkRegU2, that does that, in the always-block inside the primitive; but I doubt that's often what anyone wants.)

[mieszko]

Of the two definitions for "touches", the one that BSC uses is the second one: BSC collects the reset of every method (both values and actions) in the rule.

But then if that is the case then the t := r + 1 also reads r but is not guarded in the RTL.

I think your argument for that is that writing t := r + 1 doesn't matter because writing that to t makes no difference because the value of t at reset is undefined anyway, right?

So let's instead make our own module and see if a method it has gets called with the value of r during reset. If reading r induces gating by reset, then we would expect the method to not be called, right? (The module will also have a reset, although if we only care about reading r then that doesn't matter; but in any case it has a reset unlike mkRegU.)

mkTop =
  module
    r :: Reg (UInt 32) <- mkReg 0
    t :: Reg (UInt 32) <- mkRegU
    pr <- mkPrinter
    pt <- mkPrinter

    rules
      "rule1": when True ==> do
        $display "r via display: %0d" r
        pr.put r

      "rule2": when True ==> do
        $display "t via display: %0d" t
        pt.put t

{-# synthesize mkPrinter #-}
mkPrinter :: Module (Put (UInt 32))
mkPrinter = module
    interface
        put val = $display "via method: %0d" val

So what happens?

• reset asserted:
  • r is not shown with the$display in mkTop
  • put is called and the $display inside shows r
• reset deasserted:
  • r is shown with the$display in mkTop
  • put is called and the $display inside shows r
• t is always shown via both

I don't think this behaviour is explained by the gated-by-reset property being "inherited" from reading r.

Whatever formalism you use to model the reset value for mkReg -- say, an internal rule which, on reset, fires after any write and overwrites the written value with the reset value -- that same formalism can be applied to mkRegU: It is a module that, on reset, is witten with a non-deterministic value.

OK, let's say we imagine mkRegU is something like mkReg _ (ignoring for the moment the 0xaaa... etc business with _). Then one expect these rules:

      "rule1": when True ==> do
        $display "The value of t is: %0d" t

      "rule2": when True ==> do
        $display "The value of r is: %0d" r

to print both values or print neither, because, after all, we assumed they're the same modulo the initialization value being deterministic.

But what you call an "optimization" actually changes semantics, and the generated RTL sometimes only prints one of them:

  always@(negedge CLK)
  begin
    #0;
    $display("The value of t is: %0d", $unsigned(t));
    if (RST_N != `BSV_RESET_VALUE)
      $display("The value of r is: %0d", $unsigned(r));
  end

So, at least in the case of $display, mkRegU does not have the same behaviour as mkReg with an undetermined value.

In any case, I think what we actually potentially disagree about is whether the $display behaviour is fine or not as is. I don't like it because (a) the semantics are tricky, and (b) I don't think it's very usable if one has to think about all this.