Skip to content

Commit

Permalink
Update bit4counter_assertions.sv
Browse files Browse the repository at this point in the history
  • Loading branch information
ruwayd99 committed Jan 18, 2024
1 parent 330dedb commit f2569b8
Showing 1 changed file with 15 additions and 18 deletions.
33 changes: 15 additions & 18 deletions bit4counter_assertions.sv
Original file line number Diff line number Diff line change
Expand Up @@ -9,32 +9,29 @@ module bit4counter_assertions (
// Property declarations

// Property to check if reset resets the counter
property reset_resets_counter;
@(posedge clk) disable iff (!reset)
counter == 4'b0000;
property p_reset;
@(posedge clk)
reset |-> ##1 (counter == 4'b0000 && overflow == 0);
endproperty

// Property to check if the counter increments by 1
property combined_property;
@(posedge clk) disable iff (reset || counter == 4'b1111)
(
counter == $past(counter) + 1 &&
overflow == 0
);
endproperty
property p_increment;
@(posedge clk)
(!reset && $past(counter) != 4'b1111) |-> ##1 (counter == $past(counter) + 4'b0001 && overflow == 0);
endproperty

// Property to check if the counter overflows
property counter_overflow;
@(posedge clk) disable iff (reset || counter != 4'b1111)
overflow == 1;
endproperty

property p_overflow;
@(posedge clk)
(!reset && $past(counter) == 4'b1111) |-> ##1 (counter == 4'b0000 && overflow == 1);
endproperty
// Assertion block to check the properties
initial begin
// Apply the properties in simulation
assert property (reset_resets_counter) else $fatal("Assertion reset_resets_counter failed");
assert property (combined_property) else $fatal("Assertion combined_property failed");
assert property (counter_overflow) else $fatal("Assertion counter_overflow failed");
assert property (p_counter) else $fatal("Assertion reset_resets_counter failed");
assert property (p_property) else $fatal("Assertion combined_property failed");
assert property (p_overflow) else $fatal("Assertion counter_overflow failed");
end

endmodule: bit4counter_assertions

0 comments on commit f2569b8

Please sign in to comment.