diff --git a/SDVD.xpr b/SDVD.xpr
index f793fd9..4b23b13 100644
--- a/SDVD.xpr
+++ b/SDVD.xpr
@@ -44,7 +44,7 @@
-
+
@@ -60,7 +60,7 @@
-
+
@@ -91,20 +91,6 @@
-
-
-
-
-
-
-
-
-
-
-
-
-
-
@@ -154,6 +140,22 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -184,6 +186,13 @@
+
+
+
+
+
+
+
@@ -206,6 +215,7 @@
+
@@ -250,15 +260,16 @@
-
+
-
+
+
@@ -283,6 +294,7 @@
+
@@ -365,9 +377,7 @@
-
- Default settings for Implementation.
-
+
@@ -379,128 +389,124 @@
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
-
-
+
-
- Default settings for Implementation.
-
+
@@ -512,122 +518,120 @@
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
-
-
+
diff --git a/design/audio/audio_buffer.sv b/design/audio/audio_buffer.sv
index eb7efe2..f0467a4 100644
--- a/design/audio/audio_buffer.sv
+++ b/design/audio/audio_buffer.sv
@@ -1,4 +1,6 @@
-`include "sdvd_defs.sv"
+`ifdef VERILATOR
+ `include "sdvd_defs.sv"
+`endif
import sdvd_defs::SPEED;
//this interfaces with block ram
diff --git a/design/debouncer.sv b/design/debouncer.sv
index 88a2c95..abd162c 100644
--- a/design/debouncer.sv
+++ b/design/debouncer.sv
@@ -1,27 +1,22 @@
//NOTE: you should drive this with a slow clock to actually debounce input
-module debouncer(input logic clk, input reset, input source, output wire out);
+module debouncer(input logic clk, input reset, input source, output logic out);
logic pressed;
-assign out = pressed;
always_ff @(posedge clk) begin
if (reset)
pressed <= 0;
- else if (!pressed && source)
- pressed <= 1;
- else if (pressed && !source)
- pressed <= 0;
- else if (pressed && source)
- pressed <= 0;
- else if (!pressed && !source)
+ if (!source) begin
pressed <= 0;
+ out <= 0;
+ end
+ else
+ if (pressed)
+ out <= 0;
+ else begin
+ pressed <= 1;
+ out <= 1;
+ end
end
-
-//always_ff (@posedge clk) begin
-//
-//end
-
-
-
endmodule
diff --git a/design/low_freq_clock_gen.sv b/design/low_freq_clock_gen.sv
index ff28149..86363a7 100644
--- a/design/low_freq_clock_gen.sv
+++ b/design/low_freq_clock_gen.sv
@@ -1,4 +1,6 @@
-`include "sdvd_defs.sv"
+`ifdef VERILATOR
+ `include "sdvd_defs.sv"
+`endif
import sdvd_defs::SPEED;
// Takes in a 100MHz clock and generates the very low freq signals needed
// for driving the control logic
diff --git a/design/nexys_a7_top.sv b/design/nexys_a7_top.sv
index ec3042c..8537b0e 100644
--- a/design/nexys_a7_top.sv
+++ b/design/nexys_a7_top.sv
@@ -1,4 +1,6 @@
-`include "sdvd_defs.sv"
+`ifdef VERILATOR
+ `include "sdvd_defs.sv"
+`endif
import sdvd_defs::SPEED;
module nexys_a7_top(
input logic CLK100MHZ, CPU_RESETN,
diff --git a/design/playback_controller.sv b/design/playback_controller.sv
index 6483330..0b4aae8 100644
--- a/design/playback_controller.sv
+++ b/design/playback_controller.sv
@@ -9,7 +9,9 @@
*
* */
-`include "sdvd_defs.sv"
+`ifdef VERILATOR
+ `include "sdvd_defs.sv"
+`endif
import sdvd_defs::SPEED;
module playback_controller(
diff --git a/lib/assertion_error.sv b/lib/assertion_error.sv
new file mode 100644
index 0000000..1c24578
--- /dev/null
+++ b/lib/assertion_error.sv
@@ -0,0 +1,5 @@
+// A global error counter, useful for when we're tracking error counts from
+// assertions
+package assertion_error;
+ int errors;
+endpackage : assertion_error
diff --git a/design/sdvd_defs.sv b/lib/sdvd_defs.sv
similarity index 100%
rename from design/sdvd_defs.sv
rename to lib/sdvd_defs.sv
diff --git a/verification/audio/audio_buffer_tb.sv b/verification/audio/audio_buffer_tb.sv
index 91559de..070d498 100644
--- a/verification/audio/audio_buffer_tb.sv
+++ b/verification/audio/audio_buffer_tb.sv
@@ -1,4 +1,6 @@
-`include "sdvd_defs.sv"
+`ifdef VERILATOR
+ `include "sdvd_defs.sv"
+`endif
import sdvd_defs::SPEED;
module audio_buffer_tb;
diff --git a/verification/debouncer_assertions.sv b/verification/debouncer_assertions.sv
new file mode 100644
index 0000000..82eab14
--- /dev/null
+++ b/verification/debouncer_assertions.sv
@@ -0,0 +1,34 @@
+`ifdef VERILATOR
+ `include "assertion_error.sv"
+`endif
+module debouncer_assertions(input logic clk, reset,source, out);
+
+// Check that no matter how long the button is held down, output will only be
+// high once
+property only_one_per_press_p;
+ (source && out) |=> (source |-> ((!out) throughout (source[+])));
+endproperty
+only_one_per_press_a: assert property (@(posedge clk) only_one_per_press_p)
+ else assertion_error::errors++;
+
+// Check that the output is never high two cycles in a row
+property out_not_high_consecutively_p;
+ out |=> !out;
+endproperty
+out_not_high_consecutively_a: assert property (@(posedge clk) out_not_high_consecutively_p)
+ else assertion_error::errors++;
+
+// Check that the output always turns off if the button is depressed
+property off_if_depressed_p;
+ !source |-> !out;
+endproperty
+off_if_depressed_a: assert property (@(posedge clk) off_if_depressed_p)
+ else assertion_error::errors++;
+
+// Check that the output activates if the button is pressed
+property on_if_pressed_p;
+ !source |=> (source |-> out);
+endproperty
+on_if_pressed_a: assert property (@(posedge clk) on_if_pressed_p);
+
+endmodule
diff --git a/verification/debouncer_tb.sv b/verification/debouncer_tb.sv
index 24ea02e..8b9afeb 100644
--- a/verification/debouncer_tb.sv
+++ b/verification/debouncer_tb.sv
@@ -1,12 +1,18 @@
`timescale 1ns / 1ps
+
+`ifdef VERILATOR
+ `include "assertion_error.sv"
+`endif
+import assertion_error::errors;
module debouncer_tb;
+parameter TESTCYCLES=1000;
+
logic clk,reset,source;
wire out;
-int errors;
-
debouncer Dut (.*);
+bind debouncer debouncer_assertions AssertDut (.*);
initial begin
clk = 0;
@@ -14,12 +20,15 @@ initial begin
end
initial begin
+ // Turn assertions off during reset
+ $assertoff;
$display("Testing debouncer");
reset = 1;
source = 0;
@(posedge clk);
@(posedge clk);
reset = 0;
+ $asserton;
@(posedge clk);
source = 1;
#1;
@@ -42,6 +51,7 @@ initial begin
$error("Output not brought high during second press");
errors++;
end
+ @(posedge clk);
source = 0;
@(posedge clk);
#1;
@@ -50,8 +60,16 @@ initial begin
errors++;
end
+ $display("Generating random input to test assertions");
+ for (int i=0; i