cucapra / cucapra/protocols

[Monitor] Defer constraint checks till `step` boundaries

Open
#214 0 comments 0 reactions 1 assignee Claimed by @ngernest View on GitHub
enhancement
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.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.