How can i model something with persistent state in coq?

Question

In our university assignment we were asked to model the object of our choice in predicate and propositional logic. My group went for the 555 timer integrated circuit. We currently face the issue of modeling the behavior of the said object, the sr-latch part in particular.

The issue seem to originate from the fact that sr-latch is not describable using combinational logic.

We are not sure if the task at hand is possible and were hoping to get some advice whether its possible and, if so, on the techniques used in such cases.

Our description so far is like so:

Require Import BenB.

(* time elapsed from some point in past in microseconds as real numbers *)
Definition T := R.

(* durations in microseconds as real numbers *)
Definition D := R.

(* some arbitrary constant duration time-delta representing the oscialltion period / 2 *)
Variable td: D.

(* a type representing the io pins of the 555 IC *)
Inductive Pin: Type :=
    | output : Pin
    | voltage : Pin
    | trigger : Pin
    | threshold : Pin
    | reset : Pin
    | ground : Pin
    | control : Pin
    | discharge : Pin
.
(* predicate representing the logical state of the pin at certain time *)
Variable isHigh : T -> Pin -> Prop.


(* represents the if the current can flow through the 555 IC *)
Definition ICPowered (t:T) :=
    (isHigh t voltage)
    /\
    ~(isHigh t ground)
.

Definition srLatch (t: T) := 
    (isHigh t reset) 
    /\
    
.

Definition initialConditions := 
   ICPowered
.

(* Definition describing the expected oscillating behaviour of the output signal *)
Definition oscillationObligation :=
forall t: T,
    ((isHigh t output) -> ~(isHigh (t+d) output))
    /\
    (~(isHigh t output) -> (isHigh (t+d) output))
.


Definition correctnessTheorem := 
    initialConditions -> oscillationObligation
.

P.S. We assume that we are allowed to use forums as learning resource, and without a doubt will mention all the sources used in the work including any answer we may recive.