Minor improvements in docs/examples/abstract/abstr.sv
authorClifford Wolf <clifford@clifford.at>
Wed, 27 Mar 2019 13:49:35 +0000 (14:49 +0100)
committerClifford Wolf <clifford@clifford.at>
Wed, 27 Mar 2019 13:49:35 +0000 (14:49 +0100)
Signed-off-by: Clifford Wolf <clifford@clifford.at>
docs/examples/abstract/abstr.sv

index 00b13872e7355b58c16c5065b76c8e4d07624fe9..954d07eb8c3bbaec799b028dadb560f7f8551dd0 100644 (file)
@@ -5,15 +5,15 @@ module demo_counter_abstr (
        default clocking @(posedge clock); endclocking
        default disable iff (reset);
 
-       // make sure the counter doesnt jump over all "magic values"
+       // make sure the counter doesn't jump over any of the "magic values"
        `demo_counter_abstr_mode property ((counter < 123456) |=> (counter <= 123456));
        `demo_counter_abstr_mode property ((counter < 234567) |=> (counter <= 234567));
        `demo_counter_abstr_mode property ((counter < 345678) |=> (counter <= 345678));
        `demo_counter_abstr_mode property ((counter < 456789) |=> (counter <= 456789));
 
-       // only allow overflow by visiting the max value
+       // strictly increasing, only allow overflow by visiting the max value
        `demo_counter_abstr_mode property (counter != 20'hfffff |=> $past(counter) < counter);
-       `demo_counter_abstr_mode property (counter == 20'hfffff |=> !counter);
+       `demo_counter_abstr_mode property (counter == 20'hfffff |=> counter == 20'h00000);
 endmodule
 
 bind demo demo_counter_abstr demo_counter_abstr_i (.*);