Fixed up debouncer and added some assertions

I moved around where packages are. I couldn't find any evidence of where
other people put them, but for now they are in the `lib/` folder. Other
infrastructure changes are that all the weird includes we need to make
the linter happy are gated behind ifdefs, so they don't mess with
vivado.

I kinda can't believe concurrent assertions work because there's so
little info about them, good to ssee they actually do something

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;

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

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<TESTCYCLES; i++) begin
+        source = $urandom;
+        @(posedge clk);
+    end
+
     if (errors == 0)
         $display("Found no errors while testing debouncer");
+    else
+        $display("ERROR: Found %0d errors while testing debouncer", errors);
 
     $finish;
 

verification/playback_controller_tb.sv

@@ -6,7 +6,9 @@
 * @date: [unsure of due date]
 *
 * */
-`include "sdvd_defs.sv"
+`ifdef VERILATOR
+    `include "sdvd_defs.sv"
+`endif
 import sdvd_defs::SPEED;
 
 module playback_controller_tb;