Add docs/examples/abstract

Signed-off-by: Clifford Wolf <clifford@clifford.at>

diff --git a/docs/examples/abstract/README.md b/docs/examples/abstract/README.md
new file mode 100644 (file)
index 0000000..b13f74c
--- /dev/null
+++ b/docs/examples/abstract/README.md
@@ -0,0 +1,29 @@
+A simple example for using abstractions
+=======================================
+
+Consider the design in `demo.v` and the properties in `props.sv`. Obviously the
+properties are true, but that is hard to prove because it would take thousands of
+cycles to get from the activation of one output signal to the next.
+
+This can be solved by replacing counter with the abstraction in `abstr.sv`.
+
+In order to do this we must first prove that the abstraction is correct. This is
+done with `sby -f abstr.sby`.
+
+Then we apply the abstriction by assuming what we have just proven and otherwise
+turn `counter` into a cutpoint. See `props.sby` for details.
+
+Running `sby -f props.sby prv` proves the properties and `sby -f props.sby cvr`
+produces a cover trace that shows the abstraction in action.
+
+Suggested exercises:
+
+- Make modifications to `abstr.sv` and/or `demo.v`. Make a prediction if the
+  change will make `sby -f abstr.sby` or `sby -f props.sby prv` fail and test your
+  prediction.
+
+- What happens if we remove `abstr.sv` from `props.sby`, but leave the `cutpoint`
+  command in place?
+
+- What happens if we remove the `cutpoint` command from `props.sby`, but leave
+  `abstr.sv` in place?

diff --git a/docs/examples/abstract/abstr.sby b/docs/examples/abstract/abstr.sby
new file mode 100644 (file)
index 0000000..a2d6ce0
--- /dev/null
+++ b/docs/examples/abstract/abstr.sby
@@ -0,0 +1,16 @@
+[options]
+mode prove
+
+[engines]
+smtbmc
+
+[script]
+read -verific
+read -define demo_counter_abstr_mode=assert
+read -sv abstr.sv
+read -sv demo.v
+prep -top demo
+
+[files]
+abstr.sv
+demo.v

diff --git a/docs/examples/abstract/abstr.sv b/docs/examples/abstract/abstr.sv
new file mode 100644 (file)
index 0000000..00b1387
--- /dev/null
+++ b/docs/examples/abstract/abstr.sv
@@ -0,0 +1,19 @@
+module demo_counter_abstr (
+       input clock, reset,
+       input [19:0] counter
+);
+       default clocking @(posedge clock); endclocking
+       default disable iff (reset);
+
+       // make sure the counter doesnt jump over all "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
+       `demo_counter_abstr_mode property (counter != 20'hfffff |=> $past(counter) < counter);
+       `demo_counter_abstr_mode property (counter == 20'hfffff |=> !counter);
+endmodule
+
+bind demo demo_counter_abstr demo_counter_abstr_i (.*);

diff --git a/docs/examples/abstract/demo.v b/docs/examples/abstract/demo.v
new file mode 100644 (file)
index 0000000..9e5ed2b
--- /dev/null
+++ b/docs/examples/abstract/demo.v
@@ -0,0 +1,19 @@
+module demo (
+       input clock,
+       input reset,
+       output A, B, C, D
+);
+       reg [19:0] counter = 0;
+
+       always @(posedge clock) begin
+               if (reset)
+                       counter <= 0;
+               else
+                       counter <= counter + 1;
+       end
+
+       assign A = counter == 123456;
+       assign B = counter == 234567;
+       assign C = counter == 345678;
+       assign D = counter == 456789;
+endmodule

diff --git a/docs/examples/abstract/props.sby b/docs/examples/abstract/props.sby
new file mode 100644 (file)
index 0000000..9c2a5e8
--- /dev/null
+++ b/docs/examples/abstract/props.sby
@@ -0,0 +1,25 @@
+[tasks]
+cvr
+prv
+
+[options]
+cvr: mode cover
+prv: mode prove
+
+[engines]
+cvr: smtbmc
+prv: abc pdr
+
+[script]
+read -verific
+read -define demo_counter_abstr_mode=assume
+read -sv abstr.sv
+read -sv props.sv
+read -sv demo.v
+prep -top demo
+cutpoint demo/counter
+
+[files]
+abstr.sv
+props.sv
+demo.v

diff --git a/docs/examples/abstract/props.sv b/docs/examples/abstract/props.sv
new file mode 100644 (file)
index 0000000..056f006
--- /dev/null
+++ b/docs/examples/abstract/props.sv
@@ -0,0 +1,16 @@
+module demo_props (
+       input clock, reset,
+       input A, B, C, D
+);
+       default clocking @(posedge clock); endclocking
+       default disable iff (reset);
+
+       assert property (A |-> !{B,C,D} [*] ##1 B);
+       assert property (B |-> !{A,C,D} [*] ##1 C);
+       assert property (C |-> !{A,B,D} [*] ##1 D);
+       assert property (D |-> !{A,B,C} [*] ##1 A);
+
+       cover property (A ##[+] B ##[+] C ##[+] D ##[+] A);
+endmodule
+
+bind demo demo_props demo_props_i (.*);