Symbolic simulation

[kosarev]

Having spent some time on thinking about possible ways to analyse the properties of the transistor net and all the difficulties with rewriting the net as a complete set of proper boolean expressions, it suddenly crossed my mind a few days ago that at least theoretically it should be possible to amend the simulator to just propagate signals in symbolic form rather than concrete ones and zeroes, and thus let the formulas develop themselves as necessary. As unrealistic in practical terms as it sounds, I was actually able to get some practical results by leveraging the power of Z3, which look rather promising and probably deserve a separate ticket.

5b95f12 introduces symbolic simulation mode and does probably the simplest thing -- just assigns pins to symbolic values and then propagates the states of all nodes and then prints the value of the A register:

$ pypy3 ./z80sim.py --symbolic --no-tests
Round 1, 3535 nodes.
Round 2, 7364 nodes.
Round 3, 4976 nodes.
Round 4, 2146 nodes.
Round 5, 1370 nodes.
Round 6, 1232 nodes.
Round 7, 622 nodes.
Round 8, 446 nodes.
Round 9, 392 nodes.
Round 10, 230 nodes.
Round 11, 190 nodes.
Round 12, 142 nodes.
Round 13, 120 nodes.
Round 14, 122 nodes.
Round 15, 164 nodes.
Round 16, 202 nodes.
Round 17, 154 nodes.
Round 18, 36 nodes.
Round 19, 1152 nodes.
Round 20, 28 nodes.
Round 21, 30 nodes.
Round 22, 56 nodes.
Round 23, 68 nodes.
Round 24, 64 nodes.
Round 25, 40 nodes.
Round 26, 46 nodes.
Round 27, 32 nodes.
Round 28, 24 nodes.
Round 29, 72 nodes.
a: 0x55

It takes some minutes to run on my machine, which is much faster compared to what I expected. And more good news is that the process is clearly convergent. So after ~30 rounds the system was able to conclude that no further propagation is necessary, meaning reaching the point where all the new gate state expressions are equivalent to their old ones.

The last line is an indication of that it has been formally proved that the initial value of the register A does not depend on the state of the pins -- something we probably already know, but the formality of the knowledge somehow turns it into something exciting.

The convergence doesn't seem to be an accident; with some further changes (to be committed soon) it was possible to perform the initialisation sequence, the reset sequence and then even execute the ld a, imm instruction where imm was represented in a completely symbolic form, so after two more ticks it showed the imm0...imm7 symbols happily landed in A.

[kosarev]

Interesting enough. On 1e0b455, after the usual reset sequence and even executing a whole nop, some bits of the registers seem to contain (not pull.~clk), which is the level we set to the clock pin during the initial propagation of levels (the --after-updating-all-nodes step). Doesn't look like it depends on the number of ticks we spend on the reset sequence (propagation_delay). I wonder if anything like that can be seen on a real chip.

$ ./z80sim.py --after-reset-and-nop
after-reset-and-nop
f0583d49abb68c8da24d452ae75986422c23e92bab9eeefa96dcb0f16ece567b
...
  reg_l7: 0
  reg_l6: 1
  reg_l5: 0
  reg_l4: 1
  reg_l3: (not pull.~clk)
  reg_l2: 1
  reg_l1: 0
  reg_l0: 1
  reg_a: 55
  reg_f7: (not pull.~clk)
  reg_f6: 1
  reg_f5: 0
  reg_f4: 1
  reg_f3: (not pull.~clk)
  reg_f2: 1
  reg_f1: 0
  reg_f0: 1
...
  reg_ixl3: (not pull.~clk)
...
  reg_z3: (not pull.~clk)
...
  reg_bb1: (not pull.~clk)
...
  reg_dd1: (not pull.~clk)
...

[kosarev]

Removed the mention of Z3 from the title as it was proven to be of little use for our purposes, especially its Python API. We now generate Tseitin form directly from boolean expressions and use PicoSAT for equivalence tests.