docs: clarify DSLX cover! as SystemVerilog cover property

docs_src/dslx_std.md

@@ -774,8 +774,17 @@ fn main(x: u32) -> u32 {
     source (i.e., iverilog). See
     [google/xls#436](https://github.com/google/xls/issues/436).
 
-The `cover!` built-in tracks how often some condition is satisfied. It desugars
-into SystemVerilog cover points. Its signature is:
+The `cover!` built-in tracks how often some condition is satisfied. In generated
+SystemVerilog it is emitted as a named concurrent `cover property` sampled on
+the positive edge of the module clock, of the form:
+
+```
+<label>: cover property (@(posedge <clk>) <condition>);
+```
+
+Coverpoints are a SystemVerilog-only feature: they are omitted when generating
+plain Verilog, and they require a clock in the generated module. Its signature
+is:
 
 ```
 fn cover!<N: u32>(name: u8[N], condition: bool) -> ()
@@ -784,10 +793,23 @@ fn cover!<N: u32>(name: u8[N], condition: bool) -> ()
 Where `name` is a function-unique literal string identifying the coverpoint and
 `condition` is a boolean element. When `condition` is true, a counter with the
 given name is incremented that can be inspected upon program termination.
-Coverpoints can be used to give an indication of code "coverage", i.e., to see
-what paths of a design are exercised in practice. The name of the coverpoint
-must begin with either a letter or underscore, and its remainder must consist of
-letters, digits, underscores, or dollar signs.
+
+This is targeted **assertion-based coverage**: you place `cover!` at specific
+conditions of interest and the simulator counts how often those properties hold.
+It is not automatically generated, fully-instrumented **code coverage**
+(statement, branch, toggle, and similar). Coverpoints can still indicate which
+manually marked paths of a design are exercised in practice.
+
+The name of the coverpoint must begin with either a letter or underscore, and
+its remainder must consist of letters, digits, underscores, or dollar signs.
+
+Further coverage-related work is tracked in
+[google/xls#2139](https://github.com/google/xls/issues/2139) (DSLX interpreter
+code coverage reports),
+[google/xls#1126](https://github.com/google/xls/issues/1126) (collecting
+coverage in the interpreter/JIT), and
+[google/xls#499](https://github.com/google/xls/issues/499) (Cover op support in
+the JIT).
 
 ### `gate!`