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:
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).
Currently, the monitor checks whether a constraint that arises from an assignment
DUT.input := aholds 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 toDUT.inputis followed by aDontCareassignmentDUT.input := X, the net-effect at the end of the cycle is that there are no constraints onDUT.input:However, our monitor does not reflect this behavior as it eagerly checks whether the constraint
trace(DUT.input) == 5holds when it encounters the first assignmentDUT.input := 5, and it doesn't take into account the latterDontCareassignment that overwrites it.To fix this, overwriting assignments should update the monitor's
constraintsmap (i.e.DUT.input := Xwould cause the constraintDUT.input == 5to be removed), and we should defer constraint checks to the monitor only when we reach astep()boundary. (This is currently done inbibut not in themonitor.)This would cause the monitor behavior to be more in-line with the interpreter, which also defers checks for conflicting assignments till
stepboundaries (#165).