Open kosarev opened 2 years ago
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)
...
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.
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:
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 whereimm
was represented in a completely symbolic form, so after two more ticks it showed theimm0
...imm7
symbols happily landed in A.