Longhand Example: Divide by 3

First we define some GENERIC HARDWARE. In this case a mini FPGA with three flip-flops.

          \A s1, s2, s3;

           a = xa1 & s1 | xa2 & ~s1 | xa3 & s2 | xa4 & ~s2 | xa5 & s3 | xa6 & ~s3; 
           na = xa1 & vs1 | xa2 & ~vs1 | xa3 & vs2 | xa4 & ~vs2 | xa5 & vs3 | xa6 & ~vs3; 

           b = xb1 & s1 | xb2 & ~s1 | xb3 & s2 | xb4 & ~s2 | xb5 & s3 | xb6 & ~s3;
           nb = xb1 & vs1 | xb2 & ~vs1 | xb3 & vs2 | xb4 & ~vs2 | xb5 & vs3 | xb6 & ~vs3;

           vs1 = xxxa1 & s1 | xxxa2 & ~s1 | xxxa3 & s2 | xxxa4 & ~s2 | xxxa5 & s3 | xxxa6 & ~s3;
           vs2 = xxxb1 & s1 | xxxb2 & ~s1 | xxxb3 & s2 | xxxb4 & ~s2 | xxxb5 & s3 | xxxb6 & ~s3;
           vs3 = xxxc1 & s1 | xxxc2 & ~s1 | xxxc3 & s2 | xxxc4 & ~s2 | xxxc5 & s3 | xxxc6 & ~s3;

           X(s1) = vs1;
           X(s2) = vs2;
           X(s3) = vs3;

Then we lift some user states from this and give some rules about the user states.

           state1 = a & b; state2 = a & ~b; state3 = ~a & ~b;
           nstate1 = na & nb; nstate2 = na & ~nb; nstate3 = ~na & ~nb;

           // assert that one state or another is always active.
           always state1 | state2 | state3;
           //
           always state1 => nstate2;  always state2 => nstate3;  always state3 => nstate1;

          // eof

This does indeed work. It generates the following