• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
        • Vwsim-users-guide
          • Vwsim-tutorial
            • Vwsim-tutorial-2
            • Vwsim-tutorial-3
            • Vwsim-tutorial-1
            • Vwsim-output
            • Vwsim-input
            • 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-tutorial

    Vwsim-tutorial-1

    VWSIM tutorial: Simulating a simple circuit.

    In this tutorial, we demonstrate how to use VWSIM to simulate and analyze a simple RC (resistor-capacitor) circuit.

    Preparing VWSIM

    Prior to analyzing models with VWSIM, see vwsim-build-and-setup for build instructions. To simulate a circuit, start ACL2 and then load the simulator:

    (ld "driver.lsp")

    Read and Simulate the Circuit Description

    We will simulate a simple RC circuit with the following SPICE description. This circuit is composed of three primitives: a voltage source (VVS1) that is initially zero (volts), and it rises linearly to one volt in one second, a one Ohm resistor (RR1), and a one Farad capacitor (CC1).

    * RC Circuit
    
    VVS1 vs1 gnd pwl (0 0 1 1V)
    RR1  vs1 vc1 1
    CC1  vc1 gnd 1
    
    .tran .1 1 0

    A copy of this description can be found in "Testing/test-circuits/cirs/rc-circuit.cir".

    VWSIM can simulate the RC circuit using the following command:

    (vwsim "Testing/test-circuits/cirs/rc-circuit.cir")
    The command above reads the specified VWSIM circuit model, and attempts to parse, flatten, initialize, and simulate the RC model. If there is any processing error, VWSIM will stop the process at that point.

    Inspect Simulation Results

    As the RC circuit model is simulated, VWSIM stores the simulation values for each time step. Upon completion, we can request specific simulation results. Using the vw-output-command, we can fetch the voltage values across the resistor and capacitor, for all time steps, and place them in the global variable rc-voltages.

    (vw-output '((DEVV . RR1) (DEVV . CC1)) :save-var 'rc-voltages)
    The output result is an alistp. We can access the voltage-time values (across RR1) in the ACL2 loop by executing the vw-assoc-command:
    (vw-assoc '(DEVV . RR1) (@ rc-voltages))

    Save and Plot Simulation Results

    Using the vw-output-command, we can write the voltages across resistor RR1 and capacitor CC1 to a comma-separated values (CSV) file. A time-value graph of signal values can be plotted; e.g., using gnuplot.

    (vw-output '((DEVV . RR1) (DEVV . CC1))
               :output-file "Testing/test-circuits/csvs/rc-voltages.csv")
    VWSIM provides the vw-plot-command to run gnuplot from the ACL2 prompt. Here, we plot the voltage across RR1 and CC1 with respect to time.
    (vw-plot '((DEVV . RR1) (DEVV . CC1))
             "Testing/test-circuits/csvs/rc-voltages.csv")

    Analyze Simulation Results

    At this point, it is up to the user to view the plotted results to determine whether the desired results were achieved. In another tutorial example, we demonstrate how to write an ACL2 program to analyze a simulation result.

    Next: Simulating a Josephson Transmission Line