Verifying the correctness of DNA strand displacement cascades that implement synthetic biological neural network classifiers (winner-take-all, loser-take-all) built on the seesaw architecture is experimentally costly, and existing modelling tools either lack the flexibility to explore translation-scheme parameters or are not fit for modelling the pairwise annihilation reactions present in these circuits. We developed DISCO (DISplacement cascade COmpiler), a pipeline for assembling signal-processing circuits using a modular, parametrized translation scheme that enables systematic in silico validation and verification of design variants through reaction enumeration (Peppercorn), simulation, and checking formal equivalence to a high-level specification. We derived the timescale-separation parameters required for correct annihilation modelling and, since these inevitably create transient complexes that dominate verification complexity in larger circuits, devised a local-toehold assignment scheme that substantially reduces this complexity without significantly affecting simulation results.
|
