Add "cover" mode

docs/examples/quickstart/.gitignore

@@ -1,3 +1,4 @@
 demo
 memory
 prove
+cover

docs/examples/quickstart/cover.sby

@@ -0,0 +1,12 @@
+[options]
+mode cover
+
+[engines]
+smtbmc
+
+[script]
+read_verilog -formal cover.v
+prep -top top
+
+[files]
+cover.v

docs/examples/quickstart/cover.v

@@ -0,0 +1,13 @@
+module top (
+	input clk,
+	input [7:0] din
+);
+	reg [31:0] state = 0;
+
+	always @(posedge clk) begin
+		state <= ((state << 5) + state) ^ din;
+	end
+
+	cover property (state == 'd 12345678);
+	cover property (state == 'h 12345678);
+endmodule

docs/source/index.rst

@@ -8,7 +8,7 @@ formal tasks:
 
    * Bounded verification of safety properties (assertions)
    * Unbounded verification of safety properties
-   * Generation of test benches from cover statements [TBD]
+   * Generation of test benches from cover statements
    * Verification of liveness properties [TBD]
    * Formal equivalence checking [TBD]