From afe6960ffe6aa39dff7546be709c3e31d0536388 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 27 Mar 2019 14:45:30 +0100
Subject: [PATCH] Add docs/examples/abstract

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 docs/examples/abstract/README.md | 29 +++++++++++++++++++++++++++++
 docs/examples/abstract/abstr.sby | 16 ++++++++++++++++
 docs/examples/abstract/abstr.sv  | 19 +++++++++++++++++++
 docs/examples/abstract/demo.v    | 19 +++++++++++++++++++
 docs/examples/abstract/props.sby | 25 +++++++++++++++++++++++++
 docs/examples/abstract/props.sv  | 16 ++++++++++++++++
 6 files changed, 124 insertions(+)
 create mode 100644 docs/examples/abstract/README.md
 create mode 100644 docs/examples/abstract/abstr.sby
 create mode 100644 docs/examples/abstract/abstr.sv
 create mode 100644 docs/examples/abstract/demo.v
 create mode 100644 docs/examples/abstract/props.sby
 create mode 100644 docs/examples/abstract/props.sv

diff --git a/docs/examples/abstract/README.md b/docs/examples/abstract/README.md
new file mode 100644
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
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
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
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
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
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 (.*);
-- 
2.30.2