Assertions are useful for specifying (and checking) invariants in your code. For example, in the sw_btn_led.rp example, we have a module like this:
module logistic_map(bits<64> x, bit x_valid) -> (bits<64> out, bit out_valid);
which has a couple invariants: x_valid must only assert for one cycle, and may not assert again until out_valid asserts, and x must be held constant for the same period of time.
We can have an assert statement that watches for this behaviour during unit tests (see #8). For example, to assert that x_valid is never asserted two cycles in a row:
assert(!(x_valid[t] && x_valid[t-1]));
checking that it doesn't assert until out_valid asserts is slightly more tricky. But, to start with, the user can define custom logic to check for that:
bit x_valid_lockout;
if out_valid[t] {
x_valid_lockout[t] = 0;
} else if x_valid[t] {
x_valid_lockout[t] = 1;
assert(!x_valid_lockout[t-1]);
}
and in the future maybe we can find a better syntax.
At simulation time, asserts should always be simulated and checked. If they trigger, we should log which assert flagged, and on which cycle it flagged.
Assertions are useful for specifying (and checking) invariants in your code. For example, in the
sw_btn_led.rpexample, we have a module like this:which has a couple invariants:
x_validmust only assert for one cycle, and may not assert again untilout_validasserts, andxmust be held constant for the same period of time.We can have an assert statement that watches for this behaviour during unit tests (see #8). For example, to assert that
x_validis never asserted two cycles in a row:checking that it doesn't assert until
out_validasserts is slightly more tricky. But, to start with, the user can define custom logic to check for that:and in the future maybe we can find a better syntax.
At simulation time, asserts should always be simulated and checked. If they trigger, we should log which assert flagged, and on which cycle it flagged.