• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
        • Vwsim-users-guide
          • Vwsim-tutorial
          • Vwsim-output
          • Vwsim-input
            • Vwsim-hdl
              • Vwsim-term
              • Vwsim-constants
              • Vwsim-spice
              • Vwsim-input-source-waveforms
              • Vwsim-names
            • Vwsim-build-and-setup
            • Vwsim-commands
        • Isar
        • Wp-gen
        • Dimacs-reader
        • Pfcs
        • Legacy-defrstobj
        • Proof-checker-array
        • Soft
        • C
        • Farray
        • Rp-rewriter
        • Instant-runoff-voting
        • Imp-language
        • Sidekick
        • Leftist-trees
        • Java
        • Taspi
        • Bitcoin
        • Riscv
        • Des
        • Ethereum
        • X86isa
        • Sha-2
        • Yul
        • Zcash
        • Proof-checker-itp13
        • Regex
        • ACL2-programming-language
        • Json
        • Jfkr
        • Equational
        • Cryptography
        • Poseidon
        • Where-do-i-place-my-book
        • Axe
        • Bigmems
        • Builtins
        • Execloader
        • Aleo
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Vwsim-hdl

    Vwsim-constants

    The constants used by the VWSIM simulator.

    The VWSIM simulator defines several constants to perform simulations of electrical circuits.

    Unit Prefixes

    (defconst *kilo*   1000)
    (defconst *mega*   1000000)
    (defconst *giga*   1000000000)
    (defconst *tera*   1000000000000)
    (defconst *peta*   1000000000000000)
    
    (defconst *milli*  1/1000)
    (defconst *micro*  1/1000000)
    (defconst *nano*   1/1000000000)
    (defconst *pico*   1/1000000000000)
    (defconst *femto*  1/1000000000000000)

    Mathematical Constants

    Function: f*pi*

    (defun f*pi* nil
      "Half the distance around a unit circle"
      (declare (xargs :guard t))
      (if *use-josim-constants* (/ 3141592653589793238463
                                   1000000000000000000000)
        (/ 3141592653589793 1000000000000000)))

    Function: f*e*

    (defun f*e* nil
      "Euler's number"
      (declare (xargs :guard t))
      (/ 2718281828459045 1000000000000000))

    Fundamental Physical Constants

    Function: f*h*

    (defun f*h* nil
      "Planck's Constant (Joules * seconds)"
      (declare (xargs :guard t))
      (/ 662607015 (expt 10 42)))

    Function: f*h_bar*

    (defun f*h_bar* nil
      "Planck's Constant divided by two pi"
      (declare (xargs :guard t))
      (if *use-josim-constants* (* 10545718001391127 (expt 10 -50))
        (/ (f*h*) (* 2 (f*pi*)))))

    Function: f*e_c*

    (defun f*e_c* nil
      "Charge of an electron in Coulumbs"
      (declare (xargs :guard t))
      (if *use-josim-constants* (* 16021766208 (expt 10 -29))
        (* 16021766341 (expt 10 -29))))

    Function: f*k_b*

    (defun f*k_b* nil
      "Boltzmann's constant (Joules/Kelvin)"
      (declare (xargs :guard t))
      (/ 1380649 (expt 10 29)))

    Rapid Single Flux Quantum Constants

    Function: f*deltav*

    (defun f*deltav* nil
      "deltaV determines the size of the JJ transition region"
      (declare (xargs :guard t))
      (/ 1 10000))

    Function: f*phi0*

    (defun f*phi0* nil
      "phi0 is the magnetic flux quantum"
      (declare (xargs :guard t))
      (if *use-josim-constants* (* 2067833831170082 (expt 10 -30))
        (/ (f*h*) (* 2 (f*e_c*)))))

    Function: f*icfact*

    (defun f*icfact* nil
      "ratio of JJ critical current to quasiparticle step height"
      (declare (xargs :guard t))
      (/ (f*pi*) 4))