From 79b1ac9570a72c152e2a0d4b8b750ed5e4d56b8e Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 27 Mar 2019 14:49:35 +0100 Subject: [PATCH] Minor improvements in docs/examples/abstract/abstr.sv Signed-off-by: Clifford Wolf --- docs/examples/abstract/abstr.sv | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/examples/abstract/abstr.sv b/docs/examples/abstract/abstr.sv index 00b1387..954d07e 100644 --- a/docs/examples/abstract/abstr.sv +++ b/docs/examples/abstract/abstr.sv @@ -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 (.*); -- 2.30.2