assertion checks should have knowledge of rwire/creg internals

[quark17]

The following example produces Verilog with a RDY signal defined as 1:

interface Ifc;
  method Bit#(8) m();
endinterface

(* synthesize *)
module sysAlwaysReadyThroughWire(Ifc);
  Wire#(Bit#(8)) w <- mkWire;

  (* fire_when_enabled *)
  rule set_wire;
    w <= 0;
  endrule

  method m = w;
endmodule

However, if we add an always_ready attribute to the module, BSC reports that the method is not always ready:

Error: "AlwaysReadyThroughWire.bsv", line 7, column 8: (G0006)
  Method(s) not always ready: m

This is because the RDY signal depends on a port from the wire submodule, and BSC treats that submodule as a black box (at that point). Later, BSC inlines wires before generating Verilog, which exposes that the value is always True.

For any module that BSC knows how to inline, it would be reasonable for BSC to also consider its internals when doing assertion checks / proof obligations, like always_ready. BSC creates an SMT context containing the signal definitions; it can also include definitions for combination outputs from inline-able primitive modules (like rwire and creg).

This is bug 968 in Bluespec Inc's pre-GitHub bug database.

[mieszko]

do you remember why this check is happening before rwire inlining and not after? is it for historical reasons because it happened in the dark ages when rwires were not being inlined?

conversely it seems that the inlining happens after astate, which seems like a pretty intentional place to do this; does it have to go after that?

[quark17]

Inlining happens in the Verilog backend (which starts with astate). We perform the assertion check before the backend split, because we want to perform the check when generating Bluesim as well.

In the early days, the check for always_ready was to look at the expression for the RDY signal and see that it is the constant 1. This only worked if BSC's optimization rules were powerful enough to reduce the expression to 1 (which it wasn't always able to do). (And we might even have done this only in the Verilog backend and not for Bluesim.) Now we use an SMT solver, and ask it whether the expression is implied to be always True by what we know of the design. (And this is a query that we can do right after scheduling.) The SMT solver is quite powerful, so it is not necessary to wait until later in BSC when optimizations may simplify the expression. However, the SMT solver doesn't have information about the internal connections of wire modules, which inlining would expose. It should be easy to provide to the SMT solver -- this isn't a big project.

I don't think that inlining can be brought forward, to before the backend split, because Bluesim operates on the design in terms of modules and rules. The astate stage converts from rules into the wires that implement them. Inlining happens afterward because it is just creating a wire assignment RDY_out = EN_in (and also out = in for the data). The astate stage has created the EN signals, as a combination of the conditions (CAN_FIRE) of rules that write to the module and the scheduling logic (WILL_FIRE). The RDY signal from wire is only discovered to be 1 when the enable signal is 1, which is when the combination of rule conditions and scheduling are brought together and simplify to 1. Fortunately, the SMT solver is doing this, but it's doing it at the abstraction level of rule conditions. It just needs to know the internal connections of wire/creg modules, which should be easy to provide.

[mieszko]

ah right, i totally forgot about bluesim. and i guess bluesim needs this b/c it can't turn the rwire inside out and make it into an expression, which i guess is kinda the whole point of an rwire? hmm.

are you thinking of specialcasing this in the SMT generation (which would need to match the InlineWires code), or an annotation (or rewriting rule?) that would be common to both?

[quark17]

I was going to add special knowledge about the primitive modules RWire, RWire0, BypassWire, BypassWire0, CrossingBypassWire, CRegN5, CRegUN5, and CRegA5 to the code that translates an ASyntax module into SMT equations. Yes, this would need to be kept in sync with the various other pieces that implement these primitives, such as the import-BVI, the Verilog module, and the inlining code. I don't have any ideas on how to unify these from a common source, but I don't think my proposal prevents doing that in the future if we figure out how. (An import-BVI already specifies pairs of in/out ports that have a combinational path; maybe that could be extended to optionally specify the exact logic along the path. Note, though, that for CReg and registers, there's of course more to inlining than just combinational paths --- reg, always block, initial block, etc.)

I do think that we'll want to allow users to specify additional information that they know about a design, to the SMT solver, to use in analysis (including scheduling). (For example, things like: two input ports never have the same value.) I have no idea what that would look like, but I wonder if this info about primitive submodules could be represented using that feature, if it existed. Here, again, I don't think that my proposal prevents doing that in the future.

[mieszko]

IIRC Verilog-imported modules have a combinational path annotation that is used to detect combinational loops; I was musing that perhaps that could be extended to capture this as well. I guess the objectives are different, though: if you had some expression syntax you could convert to SMT, then in one case you'd be prepared to underapproximate and in the other to overapproximate (to stay conservative in each case), so maybe not?

But yeah I agree hacking it in for now as you suggest is the right thing to do; the issue is pretty ugly when one runs into it, and I think wires are probably the main use case anyway.