# 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

• netlist
• and simulation.

Big. Every state of the hardware has been forced to be a valid state of system. Nothing makes the states disjoint!

• Home.           SRG Talk. 12 March 2003. DJ Greaves. www.cl.cam.ac.uk.