Waylon Cude
a50efdc6c6
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
35 lines
1.1 KiB
Systemverilog
35 lines
1.1 KiB
Systemverilog
`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
|