[Monitor] Defer constraint checks till `step` boundaries
- Dominant language
- Rust
- Stars
- 15
- Forks
- 0
- Avg merge
- 6h 20m
- Merged PRs (30d)
- 15
Description
Currently, the monitor checks whether a constraint that arises from an assignment `DUT.input := a` holds eagerly, when it encounters the assignment statement.
However, in the interpreter, assignments can be overwritten. The semantics of overwriting assignments say that if in the same cycle, a concrete (non-`X`) assignment to `DUT.input` is followed by a `DontCare` assignment `DUT.input := X`, the net-effect at the end of the cycle is that there are no constraints on `DUT.input`:
```rust
DUT.input := 5;
DUT.input := X;
step(); // No constraint on `DUT.input` here
...
```
However, our monitor does not reflect this behavior as it eagerly checks whether the constraint `trace(DUT.input) == 5` holds when it encounters the first assignment `DUT.input := 5`, and it doesn't take into account the latter `DontCare` assignment that overwrites it.
To fix this, overwriting assignments should update the monitor's `constraints` map (i.e. `DUT.input := X` would cause the constraint `DUT.input == 5` to be removed), and we should defer constraint checks to the monitor only when we reach a `step()` boundary. (This is currently done in `bi` but not in the `monitor`.)
This would cause the monitor behavior to be more in-line with the interpreter, which also defers checks for conflicting assignments till `step` boundaries (#165).
Contributor guide
No contributing guide indexed for this repository
Assessment
This issue has not been assessed yet.