Bibliography

One reference list for the whole project. Author mentions in the layer documents link here; each entry carries an anchor (#key) for that purpose. Organised by topic, roughly in stack order.

On the identifiers. Every entry carries a link. DOIs were resolved against the DOI registry and their returned metadata — title, container, year — checked against the entry rather than recalled; a plausible-looking DOI pointing at the wrong paper is worse than none. Where a DOI names a reissue rather than the original printing, the entry says so. Two works have no DOI (Mock's Boole Press monograph; Makino & Berz's IJPAM paper, whose journal predates DOI registration) and are linked to a catalogue or index record instead. Software and standards link to their project or issuing-body page.

Semiconductor device equations

  • Markowich, P. A. (1986). The Stationary Semiconductor Device Equations. Springer. doi:10.1007/978-3-7091-3678-2
  • Markowich, P. A., Ringhofer, C. A. & Schmeiser, C. (1990). Semiconductor Equations. Springer. doi:10.1007/978-3-7091-6961-2
  • Jüngel, A. (2009). Transport Equations for Semiconductors. Lecture Notes in Physics 773, Springer. doi:10.1007/978-3-540-89526-8
  • Mock, M. S. (1983). Analysis of Mathematical Models of Semiconductor Devices. Boole Press. (Stationary existence; earlier results in Comm. Pure Appl. Math. 25, 1972.) Open Library
  • Gajewski, H. (1985). "On existence, uniqueness and asymptotic behavior of solutions of the basic equations for carrier transport in semiconductors". ZAMM 65(2), 101–108. doi:10.1515/9783112547182-007
  • Gajewski, H. & Gröger, K. (1986). "On the basic equations for carrier transport in semiconductors". J. Math. Anal. Appl. 113(1), 12–35. (Transient existence; the free-energy structure.) doi:10.1016/0022-247x(86)90330-6

Elliptic problems and regularity

  • Grisvard, P. (1985). Elliptic Problems in Nonsmooth Domains. Pitman; reissued as SIAM Classics in Applied Mathematics 69 (2011). (Corner singularity exponents.) doi:10.1137/1.9781611972030
  • Kellogg, R. B. (1974). "On the Poisson equation with intersecting interfaces". Applicable Analysis 4(2), 101–129. (Transmission problems with piecewise-constant coefficients.) doi:10.1080/00036817408839086
  • Gröger, K. (1989). "A W¹,ᵖ-estimate for solutions to mixed boundary value problems for second order elliptic differential equations". Math. Ann. 283, 679–687. doi:10.1007/bf01442860
  • Ern, A. & Vohralík, M. (2015). "Polynomial-degree-robust a posteriori estimates in a unified setting for conforming, nonconforming, discontinuous Galerkin, and mixed discretizations". SIAM J. Numer. Anal. 53(2), 1058–1081. (Guaranteed a posteriori FEM bounds via equilibrated flux.) doi:10.1137/130950100
  • Nakao, M. T., Plum, M. & Watanabe, Y. (2019). Numerical Verification Methods and Computer-Assisted Proofs for Partial Differential Equations. Springer. doi:10.1007/978-981-13-7669-6
  • Pólya, G. & Szegő, G. (1951). Isoperimetric Inequalities in Mathematical Physics. Princeton University Press. (Rigorous capacity bounds.) doi:10.1515/9781400882663
  • Driscoll, T. A. & Trefethen, L. N. (2002). Schwarz–Christoffel Mapping. Cambridge University Press. doi:10.1017/CBO9780511546808

Electromagnetics and quasistatics

  • Haus, H. A. & Melcher, J. R. (1989). Electromagnetic Fields and Energy. Prentice-Hall. (The careful EQS/MQS treatment.) MIT OpenCourseWare (full text)
  • Ammari, H., Buffa, A. & Nédélec, J.-C. (2000). "A justification of eddy currents model for the Maxwell equations". SIAM J. Appl. Math. 60(5), 1805–1823. doi:10.1137/s0036139998348979
  • Raviart, P.-A. & Sonnendrücker, E. (1996). "A hierarchy of approximate models for the Maxwell equations". Numer. Math. 73, 329–372. (The Darwin model justified.) doi:10.1007/s002110050196
  • Alonso Rodríguez, A. & Valli, A. (2010). Eddy Current Approximation of Maxwell Equations. Springer. doi:10.1007/978-88-470-1506-7
  • Bossavit, A. (1998). Computational Electromagnetism: Variational Formulations, Complementarity, Edge Elements. Academic Press. (Whitney forms; networks as discrete Maxwell.) doi:10.1016/B978-0-12-118710-1.X5000-4
  • Tonti, E. (2013). The Mathematical Structure of Classical and Relativistic Physics. Birkhäuser. (The classification diagrams behind the cell method.) doi:10.1007/978-1-4614-7422-7
  • Ruehli, A. E. (1974). "Equivalent circuit models for three-dimensional multiconductor systems". IEEE Trans. Microwave Theory Tech. 22(3), 216–221. (PEEC / partial inductance.) doi:10.1109/tmtt.1974.1128204
  • Kamon, M., Tsuk, M. J. & White, J. K. (1994). "FASTHENRY: a multipole-accelerated 3-D inductance extraction program". IEEE Trans. Microwave Theory Tech. 42(9), 1750–1758. doi:10.1109/22.310584

Device physics, compact models, and variability

  • Sze, S. M. & Ng, K. K. (2007). Physics of Semiconductor Devices, 3rd ed. Wiley. doi:10.1002/0470068329
  • Miller, J. M. (1919). "Dependence of the input impedance of a three-electrode vacuum tube upon the load in the plate circuit". Scientific Papers of the Bureau of Standards 15(351), 367–385. (The Miller effect: feedback-capacitance multiplication; commonly cited as 1920.) doi:10.6028/nbsscipaper.024
  • Chen, P., Kirkpatrick, D. A. & Keutzer, K. (2000). "Miller factor for gate-level coupling delay calculation". IEEE/ACM ICCAD 2000. (The coupling switching factor for delay, and the correction to the naive 0–2× range.) doi:10.1109/iccad.2000.896453
  • Chynoweth, A. G. (1958). "Ionization rates for electrons and holes in silicon". Phys. Rev. 109, 1537–1540. doi:10.1103/physrev.109.1537
  • Troutman, R. R. (1986). Latchup in CMOS Technology: The Problem and Its Cure. Kluwer. doi:10.1007/978-1-4757-1887-4
  • Black, J. R. (1969). "Electromigration — a brief survey and some recent results". IEEE Trans. Electron Devices 16(4), 338–347. doi:10.1109/t-ed.1969.16754
  • Gildenblat, G. et al. (2006). "PSP: an advanced surface-potential-based MOSFET model for circuit simulation". IEEE Trans. Electron Devices 53(9), 1979–1993. doi:10.1109/ted.2005.881006
  • Caughey, D. M. & Thomas, R. E. (1967). "Carrier mobilities in silicon empirically related to doping and field". Proc. IEEE 55(12), 2192–2193. doi:10.1109/proc.1967.6123
  • Masetti, G., Severi, M. & Solmi, S. (1983). "Modeling of carrier mobility against carrier concentration in arsenic-, phosphorus-, and boron-doped silicon". IEEE Trans. Electron Devices 30(7), 764–769. doi:10.1109/t-ed.1983.21207
  • Ando, T., Fowler, A. B. & Stern, F. (1982). "Electronic properties of two-dimensional systems". Rev. Mod. Phys. 54, 437–672. (Inversion-layer quantisation.) doi:10.1103/revmodphys.54.437
  • Kirton, M. J. & Uren, M. J. (1989). "Noise in solid-state microstructures: a new perspective on individual defects, interface states and low-frequency (1/f) noise". Adv. Phys. 38(4), 367–468. (RTN.) doi:10.1080/00018738900101122
  • Asenov, A. (1998). "Random dopant induced threshold voltage lowering and fluctuations in sub-0.1 µm MOSFETs: a 3-D 'atomistic' simulation study". IEEE Trans. Electron Devices 45(12), 2505–2513. doi:10.1109/16.735728
  • Demir, A., Mehrotra, A. & Roychowdhury, J. (2000). "Phase noise in oscillators: a unifying theory and numerical methods for characterisation". IEEE Trans. Circuits Syst. I 47(5), 655–674. doi:10.1109/81.847872

Kinetic theory, many-body theory, and quantum foundations

  • Kato, T. (1951). "Fundamental properties of Hamiltonian operators of Schrödinger type". Trans. Amer. Math. Soc. 70, 195–211. doi:10.1090/s0002-9947-1951-0041010-x
  • Dyson, F. J. & Lenard, A. (1967). "Stability of matter. I". J. Math. Phys. 8, 423–434. doi:10.1063/1.1705209
  • Lieb, E. H. & Thirring, W. E. (1975). "Bound for the kinetic energy of fermions which proves the stability of matter". Phys. Rev. Lett. 35, 687–689. doi:10.1103/PhysRevLett.35.687
  • Lieb, E. H. & Seiringer, R. (2010). The Stability of Matter in Quantum Mechanics. Cambridge University Press. doi:10.1017/cbo9780511819681
  • Glimm, J. & Jaffe, A. (1987). Quantum Physics: A Functional Integral Point of View, 2nd ed. Springer. (What constructive QFT can and cannot do.) doi:10.1007/978-1-4612-4728-9
  • Aizenman, M. & Duminil-Copin, H. (2021). "Marginal triviality of the scaling limits of critical 4D Ising and φ⁴₄ models". Ann. of Math. 194(1), 163–235. doi:10.4007/annals.2021.194.1.3
  • Erdős, L. & Yau, H.-T. (2000). "Linear Boltzmann equation as the weak coupling limit of a random Schrödinger equation". Comm. Pure Appl. Math. 53(6), 667–735. doi:10.1002/(sici)1097-0312(200006)53:6<667::aid-cpa1>3.0.co;2-5
  • Erdős, L., Salmhofer, M. & Yau, H.-T. (2008). "Quantum diffusion of the random Schrödinger evolution in the scaling limit". Acta Math. 200, 211–277. doi:10.1007/s11511-008-0027-2
  • Gérard, P., Markowich, P. A., Mauser, N. J. & Poupaud, F. (1997). "Homogenization limits and Wigner transforms". Comm. Pure Appl. Math. 50, 323–379. doi:10.1002/(sici)1097-0312(199704)50:4<323::aid-cpa4>3.0.co;2-c
  • Poupaud, F. (1991). "Diffusion approximation of the linear semiconductor Boltzmann equation: analysis of boundary layers". Asymptotic Anal. 4(4), 293–317. doi:10.3233/asy-1991-4402
  • Golse, F. & Poupaud, F. (1992). "Limite fluide des équations de Boltzmann des semi-conducteurs pour une statistique de Fermi–Dirac". Asymptotic Anal. 6(2), 135–160. doi:10.3233/asy-1992-6202
  • Ben Abdallah, N. & Degond, P. (1996). "On a hierarchy of macroscopic models for semiconductors". J. Math. Phys. 37(7), 3306–3333. (Energy-transport limits.) doi:10.1063/1.531567
  • Catto, I., Le Bris, C. & Lions, P.-L. (1998). The Mathematical Theory of Thermodynamic Limits: Thomas–Fermi Type Models. Oxford University Press. doi:10.1093/oso/9780198501619.001.0001
  • Cancès, É., Deleurence, A. & Lewin, M. (2008). "A new approach to the modelling of local defects in crystals: the reduced Hartree–Fock case". Comm. Math. Phys. 281, 129–177. doi:10.1007/s00220-008-0481-x
  • Zurek, W. H. (2003). "Decoherence, einselection, and the quantum origins of the classical". Rev. Mod. Phys. 75, 715–775. doi:10.1103/revmodphys.75.715
  • Caldeira, A. O. & Leggett, A. J. (1981). "Influence of dissipation on quantum tunneling in macroscopic systems". Phys. Rev. Lett. 46, 211–214. doi:10.1103/physrevlett.46.211
  • Devoret, M. H., Martinis, J. M. & Clarke, J. (1985). "Measurements of macroscopic quantum tunneling out of the zero-voltage state of a current-biased Josephson junction". Phys. Rev. Lett. 55, 1908–1911. doi:10.1103/physrevlett.55.1908

Dynamical systems, control, and certificates

  • Prajna, S. & Jadbabaie, A. (2004). "Safety verification of hybrid systems using barrier certificates". HSCC 2004, LNCS 2993, 477–492. doi:10.1007/978-3-540-24743-2_32
  • Parrilo, P. A. (2003). "Semidefinite programming relaxations for semialgebraic problems". Math. Program. 96, 293–320. doi:10.1007/s10107-003-0387-5
  • Prajna, S., Papachristodoulou, A. & Parrilo, P. A. (2002). "Introducing SOSTOOLS: a general purpose sum of squares programming solver". CDC 2002. doi:10.1109/cdc.2002.1184594 · SOSTOOLS
  • Harrison, J. (2007). "Verifying nonlinear real formulas via sums of squares". TPHOLs 2007, LNCS 4732, 102–118. doi:10.1007/978-3-540-74591-4_9
  • Martin-Dorel, É. & Roux, P. (2017). "A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations". CPP 2017. (ValidSDP.) doi:10.1145/3018610.3018622
  • Blanchini, F. (1999). "Set invariance in control". Automatica 35(11), 1747–1767. doi:10.1016/s0005-1098(99)00113-2
  • Lohmiller, W. & Slotine, J.-J. E. (1998). "On contraction analysis for non-linear systems". Automatica 34(6), 683–696. doi:10.1016/s0005-1098(98)00019-3
  • Jiang, Z.-P., Teel, A. R. & Praly, L. (1994). "Small-gain theorem for ISS systems and applications". Math. Control Signals Syst. 7, 95–120. doi:10.1007/bf01211469
  • Dashkovskiy, S., Rüffer, B. S. & Wirth, F. R. (2007). "An ISS small gain theorem for general networks". Math. Control Signals Syst. 19, 93–122. doi:10.1007/s00498-007-0014-8
  • Benveniste, A., Caillaud, B., Nickovic, D., Passerone, R., Raclet, J.-B., Reinkemeier, P., Sangiovanni-Vincentelli, A., Damm, W., Henzinger, T. A. & Larsen, K. G. (2018). Contracts for System Design. Foundations and Trends in EDA 12(2–3). doi:10.1561/9781680834031
  • Marino, L. R. (1981). "General theory of metastable operation". IEEE Trans. Computers C-30(2), 107–115. (Metastability provably unavoidable.) doi:10.1109/tc.1981.6312173
  • Kinniment, D. J. (2007). Synchronization and Arbitration in Digital Systems. Wiley. doi:10.1002/9780470517147

Validated numerics and computer-assisted proof

  • Rump, S. M. (1999). "INTLAB — INTerval LABoratory". In Developments in Reliable Computing, Kluwer, 77–104. doi:10.1007/978-94-017-1247-7_7 · INTLAB
  • Johansson, F. (2017). "Arb: efficient arbitrary-precision midpoint-radius interval arithmetic". IEEE Trans. Computers 66(8), 1281–1292. doi:10.1109/tc.2017.2690633
  • Kapela, T., Mrozek, M., Wilczak, D. & Zgliczyński, P. (2021). "CAPD::DynSys: a flexible C++ toolbox for rigorous numerical analysis of dynamical systems". Commun. Nonlinear Sci. Numer. Simul. 101, 105578. doi:10.1016/j.cnsns.2020.105578 · CAPD
  • Nedialkov, N. S. (2006). VNODE-LP — a validated solver for initial value problems in ordinary differential equations. Tech. Rep. CAS-06-06-NN, McMaster University. VNODE-LP
  • Nedialkov, N. S. & Pryce, J. D. (2005). "Solving differential-algebraic equations by Taylor series (I): computing Taylor coefficients". BIT 45, 561–591. (DAETS.) doi:10.1007/s10543-005-0019-y
  • Pryce, J. D. (2001). "A simple structural analysis method for DAEs". BIT 41(2), 364–394. (The Σ-method.) doi:10.1023/a:1021998624799
  • de Figueiredo, L. H. & Stolfi, J. (2004). "Affine arithmetic: concepts and applications". Numerical Algorithms 37, 147–158. doi:10.1023/b:numa.0000049462.70970.b6
  • Makino, K. & Berz, M. (2003). "Taylor models and other validated functional inclusion methods". Int. J. Pure Appl. Math. 4(4), 379–456. Semantic Scholar (author copy at bt.pa.msu.edu)
  • Tucker, W. (2002). "A rigorous ODE solver and Smale's 14th problem". Found. Comput. Math. 2, 53–117. doi:10.1007/s002080010018
  • Immler, F. (2018). "A verified ODE solver and the Lorenz attractor". J. Autom. Reason. 61, 73–111. (HOL-ODE-Numerics.) doi:10.1007/s10817-017-9448-y
  • Boldo, S., Clément, F., Filliâtre, J.-C., Mayero, M., Melquiond, G. & Weis, P. (2013). "Wave equation numerical resolution: a comprehensive mechanized proof of a C program". J. Autom. Reason. 50(4), 423–456. doi:10.1007/s10817-012-9255-4
  • Zgliczyński, P. (1997). "Computer assisted proof of chaos in the Rössler equations and in the Hénon map". Nonlinearity 10, 243–252. (Covering relations; interval Poincaré maps.) doi:10.1088/0951-7715/10/1/016
  • Galias, Z. (2001). "Interval methods for rigorous investigations of periodic orbits". Int. J. Bifurcation Chaos 11(9), 2427–2450. doi:10.1142/s0218127401003516

Reachability and formal analog verification

  • Girard, A. (2005). "Reachability of uncertain linear systems using zonotopes". HSCC 2005, LNCS 3414, 291–305. doi:10.1007/978-3-540-31954-2_19
  • Althoff, M. (2015). "An introduction to CORA 2015". ARCH 2015, 120–151. doi:10.29007/zbkv · CORA
  • Althoff, M. & Krogh, B. H. (2014). "Reachability analysis of nonlinear differential-algebraic systems". IEEE Trans. Autom. Control 59(2), 371–383. doi:10.1109/tac.2013.2285751
  • Chen, X., Ábrahám, E. & Sankaranarayanan, S. (2013). "Flow*: an analyzer for non-linear hybrid systems". CAV 2013, LNCS 8044, 258–263. doi:10.1007/978-3-642-39799-8_18 · Flow*
  • Bogomolov, S., Forets, M., Frehse, G., Potomkin, K. & Schilling, C. (2019). "JuliaReach: a toolbox for set-based reachability". HSCC 2019, 39–44. doi:10.1145/3302504.3311804 · JuliaReach
  • Greenstreet, M. R. & Mitchell, I. (1999). "Reachability analysis using polygonal projections". HSCC 1999, LNCS 1569, 103–116. (Verified toggle element; projectagons.) doi:10.1007/3-540-48983-5_12
  • Dang, T., Donzé, A. & Maler, O. (2004). "Verification of analog and mixed-signal circuits using hybrid system techniques". FMCAD 2004, LNCS 3312, 21–36. doi:10.1007/978-3-540-30494-4_3
  • Zaki, M. H., Tahar, S. & Bois, G. (2008). "Formal verification of analog and mixed signal designs: a survey". Microelectronics Journal 39(12), 1395–1404. doi:10.1016/j.mejo.2008.05.013
  • Estévez Schwarz, D. & Tischendorf, C. (2000). "Structural analysis of electric circuits and consequences for MNA". Int. J. Circuit Theory Appl. 28(2), 131–162. (Index of MNA DAEs.) doi:10.1002/(sici)1097-007x(200003/04)28:2<131::aid-cta100>3.0.co;2-w

Reliability and probabilistic verification

  • von Neumann, J. (1956). "Probabilistic logics and the synthesis of reliable organisms from unreliable components". In Automata Studies (Shannon & McCarthy, eds.), Princeton University Press, 43–98. doi:10.1515/9781400882618-003
  • Hamming, R. W. (1950). "Error detecting and error correcting codes". Bell Syst. Tech. J. 29(2), 147–160. doi:10.1002/j.1538-7305.1950.tb00463.x
  • Mukherjee, S. S., Weaver, C., Emer, J., Reinhardt, S. K. & Austin, T. (2003). "A systematic methodology to compute the architectural vulnerability factors for a high-performance microprocessor". MICRO-36, 29–40. doi:10.1109/micro.2003.1253181
  • Ibe, E., Taniguchi, H., Yahagi, Y., Shimbo, K. & Toba, T. (2010). "Impact of scaling on neutron-induced soft error in SRAMs from a 250 nm to a 22 nm design rule". IEEE Trans. Electron Devices 57(7), 1527–1538. (Multi-cell upset scaling.) doi:10.1109/ted.2010.2047907
  • Kwiatkowska, M., Norman, G. & Parker, D. (2011). "PRISM 4.0: verification of probabilistic real-time systems". CAV 2011, LNCS 6806, 585–591. doi:10.1007/978-3-642-22110-1_47 · PRISM
  • Dehnert, C., Junges, S., Katoen, J.-P. & Volk, M. (2017). "A Storm is coming: a modern probabilistic model checker". CAV 2017, LNCS 10427, 592–600. doi:10.1007/978-3-319-63390-9_31 · Storm
  • Hölzl, J. (2017). "Markov chains and Markov decision processes in Isabelle/HOL". J. Autom. Reason. 59(3), 345–387. doi:10.1007/s10817-016-9401-5

Hardware formal verification

  • Bryant, R. E. (1984). "A switch-level model and simulator for MOS digital systems". IEEE Trans. Computers C-33(2), 160–177. (MOSSIM II; channel-connected components.) doi:10.1109/tc.1984.1676408
  • Melham, T. F. (1993). Higher Order Logic and Hardware Verification. Cambridge Tracts in Theoretical Computer Science 31, CUP. doi:10.1017/cbo9780511569845
  • Clarke, E. M. & Emerson, E. A. (1981). "Design and synthesis of synchronization skeletons using branching time temporal logic". Logics of Programs, LNCS 131, 52–71. (The birth of model checking; 2007 Turing Award with Sifakis.) doi:10.1007/BFb0025774
  • Hunt, W. A., Jr. (1989). "Microprocessor design verification". J. Automated Reasoning 5(4), 429–460. (FM8501.) doi:10.1007/BF00243132
  • Bevier, W. R., Hunt, W. A., Jr., Moore, J S. & Young, W. D. (1989). "An approach to systems verification". J. Automated Reasoning 5(4), 411–428. (The CLI verified stack.) doi:10.1007/BF00243131
  • Cohn, A. (1989). "The notion of proof in hardware verification". J. Automated Reasoning 5(2), 127–139. (What Viper's "verified" could and could not mean; this book's cautionary ancestor.) doi:10.1007/BF00243000
  • Brock, B. & Hunt, W. A., Jr. (1997). "The DUAL-EVAL hardware description language and its use in the formal specification and verification of the FM9001 microprocessor". Formal Methods in System Design 11(1), 71–104. (FM9001 was fabricated as a CMOS ASIC.) doi:10.1023/A:1008685826293
  • Edelman, A. (1997). "The mathematics of the Pentium division bug". SIAM Review 39(1), 54–67. doi:10.1137/S0036144595293959
  • Moore, J S., Lynch, T. W. & Kaufmann, M. (1998). "A mechanically checked proof of the correctness of the kernel of the AMD5K86 floating-point division program". IEEE Trans. Computers 47(9), 913–926. doi:10.1109/12.713311
  • Beyer, S., Jacobi, C., Kroening, D., Leinenbach, D. & Paul, W. (2006). "Putting it all together — formal verification of the VAMP". STTT 8(4–5), 411–430. (Verisoft's processor, ISA to gates in PVS.) doi:10.1007/s10009-006-0204-6
  • Klein, G. et al. (2009). "seL4: formal verification of an OS kernel". SOSP 2009, 207–220. doi:10.1145/1629575.1629596
  • Lööw, A., Kumar, R., Tan, Y. K., Myreen, M. O., Norrish, M., Abrahamsson, O. & Fox, A. (2019). "Verified compilation on a verified processor". PLDI 2019, 1041–1053. (The Silver stack.) doi:10.1145/3314221.3314622
  • Lööw, A. (2021). "Lutsig: a verified Verilog compiler for verified circuit development". CPP 2021, 46–60. doi:10.1145/3437992.3439916
  • Burch, J. R. & Dill, D. L. (1994). "Automatic verification of pipelined microprocessor control". CAV 1994, LNCS 818. (Flushing as the abstraction function.) doi:10.1007/3-540-58179-0_44
  • Fox, A. (2003). "Formal specification and verification of ARM6". TPHOLs 2003, LNCS 2758. (A commercial ISA against a real pipeline, in HOL4.) doi:10.1007/10930755_2
  • Kuehlmann, A., Paruthi, V., Krohm, F. & Ganai, M. K. (2002). "Robust Boolean reasoning for equivalence checking and functional property verification". IEEE Trans. CAD 21(12), 1377–1394. doi:10.1109/tcad.2002.804386
  • Brand, D. (1993). "Verification of large synthesized designs". ICCAD 1993, 534–537. doi:10.1109/iccad.1993.580110
  • Kaufmann, D., Biere, A. & Kauers, M. (2019). "Verifying large multipliers by combining SAT and computer algebra". FMCAD 2019, 28–36. (PAC certificates.) doi:10.23919/fmcad.2019.8894250
  • Leroy, X. (2009). "Formal verification of a realistic compiler". Comm. ACM 52(7), 107–115. (CompCert; the verified-pass vs validated-pass calculus.) doi:10.1145/1538788.1538814
  • Armstrong, A. et al. (2019). "ISA semantics for ARMv8-A, RISC-V, and CHERI-MIPS". POPL 2019. (The Sail language.) doi:10.1145/3290384
  • Bauereiss, T. et al. (2022). "Verified security for the Morello capability-enhanced prototype Arm architecture". ESOP 2022, LNCS 13240, 174–201. doi:10.1007/978-3-030-99336-8_7

Standards, data sheets, and artifacts

  • JEDEC (2006). JESD89A: Measurement and Reporting of Alpha Particle and Terrestrial Cosmic Ray-Induced Soft Errors in Semiconductor Devices. (The standard terrestrial flux reference.) JEDEC
  • UC Berkeley BSIM Group. BSIM4 MOSFET Model — Technical Manual. (What E1 actually asserts; the SKY130 models are BSIM4.) BSIM Group
  • Synopsys. Liberty Library Modeling Reference (the .lib format specification). (What the PDK tables assert.) Synopsys TAP-in
  • SkyWater Technology / Google. SKY130 Open Source PDK Documentation. (Layer stack, model cards, DRC deck — the data register's D3/D4 sources.) skywater-pdk docs
  • Asanović, K., et al. The Rocket Chip Generator (UCB/EECS-2016-17). The core generator's technical report; with the rocket-chip repository and the Chipyard framework as the living artifacts.
  • The FIRRTL Specification. The intermediate representation's written semantics — L3/04's anchor. Spec; Izraelevitz et al., Reusability is FIRRTL Ground (ICCAD 2017) for the design rationale.
  • SiFive / CHIPS Alliance. TileLink Specification. The interconnect protocol L5/02's contract restricts. Spec
  • RISC-V International. RISC-V Debug Specification (v0.13 lineage). The debug module's imported register model (L3/06).
  • RISC-V International. sail-riscv: the ratified formal specification of the RISC-V ISA. Repository; exports to Coq/Isabelle/HOL4/Lean. GitHub