[patch] Probes Section cleanup

spec.md

@@ -822,7 +822,7 @@ Both `Probe`{.firrtl} and `RWProbe`{.firrtl} may be read from using the `read`{.
 `RWProbe`{.firrtl} may also be forced using the `force`{.firrtl} and `force_initial`{.firrtl} commands (see [@sec:force-and-release]).
 However, when forcing is not needed, the `Probe`{.firrtl} allows more aggressive optimization.
 
-Probes can be passed through ports using the `define`{.firrtl} statement (see [@sec:define]).
+Probes can be passed through ports using the `define`{.firrtl} statement (see [@sec:the-define-statement]).
 
 Probe types may be specified as part of an external module (see [@sec:externally-defined-modules]), with the resolved referent for each specified using `ref`{.firrtl} statements.
 
@@ -2023,18 +2023,47 @@ cover(clk, pred, en, "X equals Y when Z is valid") : optional_name
 
 # Probes
 
-Probe references are created with `probe`{.firrtl} expressions, routed through the design using the `define`{.firrtl} statement, read using the `read`{.firrtl} expression (see [@sec:reading-probe-references]), and forced and released with `force`{.firrtl} and `release`{.firrtl} statements.
+Probes are a feature which facilitate graybox testing of FIRRTL modules.
 
-These statements are detailed below.
+Probes allow modules to expose circuit components contained inside of them.
+Given a probe, you can use it to read the value of the circuit component it references.
+For read-writeable probes, you can also force it, causing it to take on a specified value.
 
-## Define
+Since they are intended for verification, ports with a probe type do not necessarily result in physical hardware.
 
-Define statements are used to route references through the design, and may be used wherever is most convenient in terms of available identifiers -- their location is not significant other than scoping, and do not have last-connect semantics.
-Every sink-flow probe must be the target of exactly one of these statements.
+## Types
 
-The define statement takes a sink-flow static reference target and sets it to the specified reference, which must either be a compatible probe expression or static reference source.
+There are two probe types, `Probe<T>`{.firrtl} is a read-only variant and `RWProbe<T>`{.firrtl} is a read-write variant.
+(See [@sec:probe-types]).
 
-Example:
+Examples:
+
+``` firrtl
+Probe<UInt<8>>
+RWProbe<UInt<8>>
+```
+
+A `RWProbe<T>`{.firrtl} will be implicitly cast to a `Probe<T>`{.firrtl} whenever an expression of type `RWProbe<T>`{.firrtl} is assigned to a port with type `Probe<T>`{.firrtl}.
+
+While `RWProbe<T>`{.firrtl} is strictly more powerful, `Probe<T>`{.firrtl} allows for more aggressive optimization.
+You should consider using `Probe`{.firrtl} whenever you know you don't need to ability to force (see [@sec:forcing]).
+
+## The `probe`{.firrtl} and `rwprobe`{.firrtl} Expressions
+
+Given a reference to a circuit component, you can capture it in a probe with `probe`{.firrtl} for a read-only probe or with `rwprobe`{.firrtl} for a read-writeable probe.
+
+## The `define`{.firrtl} Statement
+
+Since neither `Probe<T>`{.firrtl} nor `RWProbe<T>`{.firrtl} is a connectable type ([@sec:connectable-types]), circuit components with these types cannot be connected to.
+Instead, we use the `define`{.firrtl} statement to route probes through a FIRRTL circuit.
+
+The `define`{.firrtl} statements works similarly to `connect`{.firrtl}, but it has special interactions with conditional statements ([@sec:conditionals]).
+`define`{.firrtl} statements may appear within conditional blocks, and when they do, they may connect circuit components defined in a local scope.
+However, `define`{.firrtl} are not subject to last connect semantics, and the `define`{.firrtl} statement is always and unconditionally in effect.
+
+All probes in a module definition must be initialized with a `define`{.firrtl} statement.
+
+Here is an example of a module which uses `define`{.firrtl} to pass a number of probes to its ports:
 
 ``` firrtl
 module Refs:
@@ -2053,12 +2082,12 @@ module Refs:
   define d = probe(clock)
 ```
 
-The target is not required to be only an identifier, it may be a field within a bundle or other statically known sub-element of an aggregate, for example:
+The target may also be a subcomponent of a circuit component:
 
 ``` firrtl
 module Foo:
   input x : UInt
-  output y : {x: UInt, p: Probe<UInt>}
+  output y : { x: UInt, p: Probe<UInt> }
   output z : Probe<UInt>[2]
 
   wire w : UInt
@@ -2070,103 +2099,20 @@ module Foo:
   define z[1] = probe(w)
 ```
 
-`RWProbe`{.firrtl} references to ports are not allowed on public-facing modules.
-
-Define statements can set a `Probe`{.firrtl} to either a `Probe`{.firrtl} or `RWProbe`{.firrtl}, but a `RWProbe`{.firrtl} cannot be set to a `Probe`{.firrtl}.
-The inner types of the two references must (recursively) be identical or identical with the destination containing uninferred versions of the corresponding element in the source type.
-See [@sec:type-inference] for details.
-
-### Probes and Passive Types
-
-While `Probe`{.firrtl} inner types are passive, the type of the probed static reference is not required to be:
-
-``` firrtl
-module Foo :
-  input x : {a: UInt, flip b: UInt}
-  output y : {a: UInt, flip b: UInt}
-  output xp : Probe<{a: UInt, b: UInt}> ; passive
-
-  wire p : {a: UInt, flip b: UInt} ; p is not passive
-  define xp = probe(p)
-  connect p, x
-  connect y, p
-```
-
-### Probes and Const Types
+## The `read`{.firrtl} Expressions
 
-Probe types may target `const`{.firrtl} signals, but cannot use `rwprobe`{.firrtl} with a constant signal to produce a `RWProbe<const T>`{.firrtl}.
+Both `Probe`{.firrtl} and `RWProbe`{.firrtl} may be read from using the `read`{.firrtl} expression.
 
-### Exporting References to Nested Declarations
+Keep in mind that probes are intended for verification and aren't intended to be synthesizable.
+A `read`{.firrtl} expression can reach arbitrarily far into the module hierarchy to read from a distant circuit component, which is arguably unphysical at worst and potentially expensive at best.
 
-Nested declarations (see [@sec:nested-declarations]) may be exported:
+## Forcing
 
-``` firrtl
-module RefProducer :
-  input a : UInt<4>
-  input en : UInt<1>
-  input clk : Clock
-  output thereg : Probe<UInt>
+A `RWProbe`{.firrtl} may be forced using the `force`{.firrtl} and `force_initial`{.firrtl} commands.
+When you force a component, it will ignore all other drivers and take on the value supplied by the force statement instead.
+The `release`{.firrtl} and `release_initial`{.firrtl} statements end the forcing, reconnecting the circuit component to its usual driver.
 
-  when en :
-    reg myreg : UInt, clk
-    connect myreg, a
-    define thereg = probe(myreg)
-```
-
-### Forwarding References Upwards
-
-Define statements can be used to forward a child module's reference further up the hierarchy:
-
-``` firrtl
-module Foo :
-  output p : Probe<UInt>
-  ; ...
-
-module Forward :
-  output p : Probe<UInt>
-
-  inst f of Foo
-  define p = f.p
-```
-
-Define statements may narrow a probe of an aggregate to a sub-element using static expression:
-
-``` firrtl
-module Foo :
-  output p : Probe<UInt[2]>[2]
-  ; ...
-
-module Forward :
-  output p : Probe<UInt>
-
-  inst f of Foo
-  define p = f.p[0][1]
-```
-
-### Forwarding References Downwards
-
-Define statements can also be used to forward references down the hierarchy using input reference-type ports, which are allowed but should be used carefully as they make it possible to express invalid reference paths.
-
-See [@sec:input-probe-references] for more details, a small example is given below:
-
-``` firrtl
-module UnusedInputRef :
-  input r : Probe<UInt<1>>
-
-module ForwardDownwards :
-  input in : UInt<1>
-
-  inst u of UnusedInputRef
-  define u.r = probe(in)
-```
-
-## Force and Release
-
-To override existing drivers for a `RWProbe`{.firrtl}, the `force`{.firrtl} statement is used, and released with `release`{.firrtl}.
-Force statements are simulation-only constructs and may not be supported by all implementations.
-They are similar to the verification statements (e.g., `assert`{.firrtl}) in this regard.
-
-These are two variants of each, enumerated below:
+Like `read`{.firrtl}, the force statements are verification constructs.
 
   -------------------------------------------------------------------------------------------------------------------
   Name              Arguments                      Argument Types
@@ -2320,139 +2266,52 @@ module DUT :
   connect y, p
 ```
 
-## Input Probe References
-
-Probe references are generally forwarded up the design hierarchy, being used to reach down into design internals from a higher point.
-As a result probe-type references are most often output ports, but may also be used on input ports internally, as described in this section.
-
-Input probe references are allowed on internal modules, but they should be used with care because they make it possible to express invalid or multiple reference paths.
-When probe references are used to access the underlying data (e.g., with a `read`{.firrtl} or `force`{.firrtl}), they must target a statically known element at or below the point of that use, in all contexts.
-Support for other scenarios are allowed as determined by the implementation.
-
-Input probe references are not allowed on public-facing modules: e.g., the top module and external modules.
-
-Examples of input probe references follow.
-
-### U-Turn Example
-
-``` firrtl
-module UTurn:
-  input in : Probe<UInt>
-  output out : Probe<UInt>
-  define out = in
-
-module RefBouncing:
-  input x: UInt
-  output y: UInt
-
-  inst u1 of UTurn
-  inst u2 of UTurn
-
-  node n = x
-  define u1.in = probe(n)
-  define u2.in = u1.out
+## Probes and Layers
 
-  connect y, read(u2.out) ; = x
-```
-
-In the above example, the probe of node `n`{.firrtl} is routed through two modules before its resolution.
-
-### Invalid Input Reference
+`Probe`{.firrtl} and `RWProbe`{.firrtl} types may be associated with a layer (see [@sec:layers]).
+When associated with a layer, the reference type may only be driven from that layer.
 
-When using a probe reference, the target must reside at or below the point of use in the design hierarchy.
-Input references make it possible to create designs where this is not the case, and such upwards references are not supported:
+For example:
 
 ``` firrtl
-module Foo:
-  input in : Probe<UInt>
-  output out : UInt
-
-  connect out, read(in)
+Probe<UInt<8>, A.B>     ; A.B is a layer
+RWProbe<UInt<8>, A.B>
 ```
 
-Even when the target resolves at or below, the path must be the same in all contexts so a single description of the module may be generated.
-
-The following example demonstrates such an invalid use of probe references:
-
-``` firrtl
-circuit:
-  public module Top:
-    input in : UInt<4>
-    output out : UInt
-
-    inst ud1 of UpDown
-    connect ud1.in, in
-    define ud1.in_ref = ud1.r1
-
-    inst ud2 of UpDown
-    connect ud2.in, in
-    define ud2.in_ref = ud2.r2
+For details on how probes are lowered, see the FIRRTL ABI Specification.
 
-    connect out, add(ud1.out, ud2.out)
-
-  module UpDown:
-    input in : UInt<4>
-    input in_ref : Probe<UInt<4>>
-    output r1 : Probe<UInt<4>>
-    output r2 : Probe<UInt<4>>
-    output out : UInt
-
-    ; In ud1, this is UpDown.n1, in ud2 this is UpDown.n2 .
-    ; However, this is not supported as it cannot be both at once.
-    connect out, read(in_ref)
-    node n1 = and(in, UInt<4>(1))
-    node n2 = and(in, UInt<4>(3))
-    define r1 = probe(n1)
-    define r2 = probe(n2)
-```
+## External Modules
 
-### IO with references to endpoint data
+Probe types may be specified as part of an external module (see [@sec:externally-defined-modules]), with the resolved referent for each specified using `ref`{.firrtl} statements.
 
-A primary motivation for input probe references is that in some situations they make it easier to generate the FIRRTL code.
-While output references necessarily capture this design equivalently, this can be harder to generate and so is useful to support.
+## Limitations
 
-The following demonstrates an example of this, where it's convenient to use the same bundle type as both output to one module and input to another, with references populated by both modules targeting signals of interest at each end.
-For this to be the same bundle type -- input on one and output on another -- the `Probe` references for each end should be output-oriented and accordingly are input-oriented at the other end.
-It would be inconvenient to generate this design so that each has output probe references only.
+### `RWProbe`{.firrtl} with Aggregate Types
 
-The `Connect` module instantiates a `Producer` and `Consumer` module, connects them using a bundle with references in both orientations, and forwards those references for inspection up the hierarchy.
-The probe targets are not significant, here they are the same data being sent between the two, as stored in each module.
+Probes of aggregates do not working under all ABI versions.
+In these cases, it is recommended that if you have a need to probe a bundle, you instead use a bundle of probes, each targeting an individual subcomponent.
 
-``` firrtl
-module Consumer:
-  input in : {a: UInt, pref: Probe<UInt>, flip cref: Probe<UInt>}
-  ; ...
-  node n = in.a
-  define in.cref = probe(n)
+For more information on the how probes are lowered, see the FIRRTL ABI Specification.
 
-module Producer:
-  output out : {a: UInt, pref: Probe<UInt>, flip cref: Probe<UInt>}
-  wire x : UInt
-  define out.pref = probe(x)
-  ; ...
-  connect out.a, x
+### No `RWProbe`{.firrtl}s of Ports on Public Modules
 
-module Connect:
-  output out : {pref: Probe<UInt>, cref: Probe<UInt>}
+Conceptually, in order to force a value onto a circuit component, you need to be able to disconnect it from its former driver.
+However, the driver of a port is another port in some other module.
+And so, to force a port, you must have control over both "ends" of a port.
 
-  inst a of Consumer
-  inst b of Producer
+Trouble arises with ports on a public module ([@sec:public-modules]).
+Since we don't control the remote side of ports (since they might live in another FIRRTL file), we cannot force these ports either.
+For this reason, it is an error to use `rwprobe`{.firrtl} on any port on a public module.
 
-  ; Producer => Consumer
-  connect a.in.a, b.out.a
-  define a.in.pref = b.out.pref
-  define b.out.cref = a.in.cref
+### Input Ports
 
-  ; Send references out
-  define out.pref = b.out.pref
-  define out.cref = a.in.cref
+FIRRTL allows probes to be passed through ports.
+However, due to the limitations of Verilog, there is an important restriction on where they may be used.
 
-module Top:
-  inst c of Connect
+A module which only sends probes up towards its parent via output ports have no restriction.
+However, when a module receives a probe from its parent through an input port, it may not use it in a `read`{.firrtl} expression nor may it force it if the circuit component it references does not live in a module that is a descendent of the current module.
 
-  node producer_debug = read(c.out.pref); ; Producer-side signal
-  node consumer_debug = read(c.out.cref); ; Consumer-side signal
-```
+For more information on the how probes are lowered, see the FIRRTL ABI Specification.
 
 # Expressions
 
@@ -2633,7 +2492,6 @@ Read operations can be used anywhere a signal of the same underlying type can be
 ```
 
 The source of the probe must reside at or below the point of the `read`{.firrtl} expression in the design hierarchy.
-See [@sec:invalid-input-reference] for an example of an invalid `read`{.firrtl} of an input reference.
 
 ## Probe