1
$\begingroup$

For some time I tried formulating sr-latch behavior in predicate logic natural language for a university assignment. However there is an issue because we only can use combination logic expressions. We attempted to say that:

for every instant (t) in time it holds that:

  if it holds that:
    exists an instant (t1) in time before t, such that SR was set at t1
    and does not exist an instant (t2) in time after t1 and before t such that SR was reset at t2 
  then it also holds that:
    for every time instant (t3) it holds that:
      if it holds that:
        t3 is before t and after t1
      then it also holds that:
        SR outputs True

  and

  if it holds that:
    exists an instant (t1) in time before t, such that SR was reset at t1
    and does not exist an instant (t2) in time after t1 and before t such that SR was set at t2
  then it also holds that:
    for every time instant (t3) it holds that:
      if it holds that:
        t3 is before t and after t1
      then it also holds that:
        SR outputs False

However I quickly realized that this is a faulty formalization since if a latch would be set, and later reset (or reset, and later set) the implications wouldn't hold. But then I am not sure what I can do since we are dealing with combination logic, and while I can account for a fixed number of pairs by adding more and more parts to conjunction each having different numbers of exists statement, I certainly cant describe a general case in this way.

How can I describe the behavior of set reset latch (essentially a 1 bit memory device) using predicate logic natural language.

P.S. I understand that the format of definition is not common, but to be bluntly fair I'm more interested in overall way to approach this problem, hence i only look for explanation and don't care in which notation it would be.

Update:

I was asked to provide more structured formulation to illustrate the problem. So here is some abstract rust code which i hope clarifies things:


fn flip_flop_output(now: u64) -> bool {
    for t in (now-1)..0 {
        if sr_set_at(t) {
            return true;
        }
        if sr_reset_at(t) {
            return false;
        }
    }
}


In addition because of the way system outside of sr-latch is described it is impossible to have set and reset active at the same time, hence the order of checks does not matter in this case.

$\endgroup$
3
  • $\begingroup$ Methodologically, first, apply a proper notation into the descriptive text to render the matter perspicuous. See what is called pseudocode in computer science as an example in this vein. $\endgroup$ Commented Jun 3, 2022 at 8:20
  • $\begingroup$ @TankutBeygu could you elaborate? Do you want me to provide the formulation in pseudo code? Afaik there are no strict syntax for pseudo code. Would it be ok if i expand the question with some rust code instead? $\endgroup$ Commented Jun 3, 2022 at 8:33
  • $\begingroup$ If you want to convey what you have attempted and where you are stuck easily to many readers (to yourself, too!), use at least widely familiar symbols, etc., like $t_{1} < t_{2}$ instead of 'before' and 'after'. Especially, if you consider that the subject is of electrical-electronics engineering rather than mathematics . . . $\endgroup$ Commented Jun 3, 2022 at 9:07

0

You must log in to answer this question.

Browse other questions tagged .