`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