diff --git a/docs_src/dslx_std.md b/docs_src/dslx_std.md
index 93b8c477ea..6db55e760f 100644
--- a/docs_src/dslx_std.md
+++ b/docs_src/dslx_std.md
@@ -774,20 +774,42 @@ 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>);
+```
+
+Cover properties 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) -> ()
 ```
 
-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.
+Where `name` is a function-unique literal string identifying the cover property
+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.
+
+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). Cover properties can still indicate
+which manually marked paths of a design are exercised in practice.
+
+The name of the cover property 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!`