// This Jazz&Rhythm&Blues tutorial provides an example 
// of (virtual) circuit design, simulation and test. 
// Chosen example is the sec/mn counter in a digital watch.
import jazz.circuit.*;
import jazz.circuit.Net.*;

// Put 2 devices on a test board:  gen1net and babylon.

device gen1net {
  output incr:Net;       // communication between devices thru wire incr
  // Jazz synthesizes sequencial logic from periodic binary sequences
  incr = constant(#1011001111110(1)); // input test sequence, reasonable here
}
// This device is compiled into the netlist gen1net.jzn
export gen1net();

// gen1net can generates input for a single input devices, such as cm60.
// the name of the single input on the other device must also be incr,
// if we want to simulate both together: connections between devices
// for the Blues simulator are made thru the names given to external IOs.

device babylon {
  input incr:Net;
  output u4:Net[4], d4:Net[4], // decimal coded binary
         u7:Net[7], d7:Net[7],   // 7 segments display
   incr59:Net;  // counter will reset to 0 on next cycle
  (u4, d4, incr9, incr59) = cm60(incr); // count mod 60
  u7 = decode7segs(u4);
  d7 = decode7segs(d4);
  // although net incr9 is not an output from the device, we
  // want to see its values, while debugging thru simulation
  @Debug.probe(incr9, "incr9");
}
// This device is compiled into the netlist babylon.jzn
export babylon();

// counter modulo 60, from the Babylonians
fun cm60(incr:Net) = (u:Net[4], d:Net[4], // Decimal Coded Binary
      incr9:Net,                   //   u=9, and incr
      incr59:Net)             //   u+10d=59, and incr
{
  (u, incr9) = countMod(10)(incr);  // counter modulo 10
  (d', incr59)= countMod(6)(incr9);  // counter modulo 6
  d[0..2]=d'; d[3]=constant(0);      // extend to 4 bits
}

// Binary n bit counter
fun counter(n:int)(incr:Net) = (sum:Net[n], ovfl:Net){ 
  for (k<n)         // n half-adders, and sum registers
    (sum[k], carry[k+1]) = (reg(sum[k]^carry[k]), sum[k]&carry[k]);
  ovfl = carry[n]; // incr when Sum=2**n-1
  carry[0] = incr; 
}

fun even(p) = (0 == p.bit(0));
fun odd(p)  = (1 == p.bit(0));

// Counter modulo m
fun countMod(m:int)(incr:Net) = (sum:Net[], ovfl:Net)
{
  assert(m>1);       // Counters modulo 0 or 1 are not allowed
  if (m==2)                             // a counter, modulo 2,
  (sum, ovfl) = counter(1)(incr);  // is a 1 bit binary counter
  else if (even(m)) {                   // to count modulo 2m',
    (sum[0..0], c1) = counter(1)(incr);      // count modulo 2,
    (sum[1..], ovfl) = countMod(m div 2)(c1);  // and modulo m'
  } else {                  // count modulo an odd number 1+2m'
    n = (m-1).prefixLength();      // number of bits in counter
    (sum, _) = reset(counter(n)(incr), ovfl);     // reset to 0
    // when the counter gets incremented from the value sum=m-1.
    ovfl = incr & subset(m-1)(sum);             
  }
  // Test if sum(s[k]2**k) is equal to n
  fun subset(n:int)(s:Net[]) = result:Net
  { // result = AND{s[k]: n##k=1} = 1 iff n subset S
    result = (n==1) ? s[0] : even(n) ? r2 : s[0] & r2;
    r2 = subset(n div 2)(s[1..]);
  }
}

// This circuit was obtained thru BDD synthesis from Truth Tables
fun decode7segs(b:Net[4]) = s:Net[7] 
{
  // Shared expressions, over 1 bit input b[0]
  z = constant(0);           // (0)
  u = constant(-1);          // (1)
  n = ~ b[0];                // 10   = ~ b[0]
  // Shared expressions, over 2 bits input b[0..1]
  d1 = mux(b[1],z,n);        // 1000 = ~(b[0] | b[1])
  d2 = mux(b[1],n,u);        // 1110 = ~(b[0] & b[1])
  d3 = mux(b[1],n,z);        // 0010 = ~ b[0] & b[1]
  d4 = mux(b[1],u,n);        // 1011 = ~ b[0] | b[1]
  d5 = mux(b[1],n,b[0]);     // 0110 =   b[0] ^ b[1]
  d6 = mux(b[1],b[0],u);     // 1101 = ~ b[1] | b[0]
  d7 = mux(b[1],b[0],n);     // 1001 = ~(b[0] ^ b[1])
  d8 = mux(b[1],u,b[0]);     // 0111 =   b[0] | b[1]
  // Shared expressions, over 3 bits input b[0..2]
  t1 = mux(b[2],d2,d1);      // 1000 1110 
  t2 = mux(b[2],d2,b[1]);    // 0011 1110 
  t3 = mux(b[2],d5,d4);      // 1011 0110 
  t4 = mux(b[2],u,d6);       // 1101 1111 
  t5 = mux(b[2],d7,u);       // 1111 1001 
  t6 = mux(b[2],d8,d4);      // 1011 0111 
  t7 = mux(b[2],d3,n);       // 1010 0010
  // 7 segments output from decoder, with truth tables
  s[0] = mux(b[3],u,t1);     // 10001110 11111111
  s[1] = mux(b[3],u,t2);     // 00111110 11111111
  s[2] = t7;                 // 10100010 10100010
  s[3] = mux(b[3],u,t3);     // 10110110 11111111
  s[4] = mux(b[3],u,t4);     // 11011111 11111111
  s[5] = mux(b[3],u,t5);     // 11111001 11111111
  s[6] = mux(b[3],u,t6);     // 10110111 11111111
}