Reachability analysis of nonlinear analog circuits through iterative reachable set reduction

Seyed Nematollah Ahmadyan, Shobha Vasudevan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We propose a methodology for reachability analysis of nonlinear analog circuits to verify safety properties. Our iterative reachable set reduction algorithm initially considers the entire state space as reachable. Our algorithm iteratively determines which regions in the state space are unreachable and removes those unreachable regions from the over approximated reachable set. We use the State Partitioning Tree (SPT) algorithm to recursively partition the reachable set into convex polytopes. We determine the reachability of adjacent neighbor polytopes by analyzing the direction of state space trajectories at the common faces between two adjacent polytopes. We model the direction of the trajectories as a reachability decision function that we solve using a sound root counting method. We are faithful to the nonlinearities of the system. We demonstrate the memory efficiency of our algorithm through computation of the reachable set of Van der Pol oscillation circuit.

Original languageEnglish (US)
Title of host publicationProceedings - Design, Automation and Test in Europe, DATE 2013
Pages1436-1441
Number of pages6
StatePublished - 2013
Event16th Design, Automation and Test in Europe Conference and Exhibition, DATE 2013 - Grenoble, France
Duration: Mar 18 2013Mar 22 2013

Other

Other16th Design, Automation and Test in Europe Conference and Exhibition, DATE 2013
CountryFrance
CityGrenoble
Period3/18/133/22/13

Fingerprint

Analog circuits
Circuit oscillations
Trajectories
Acoustic waves
Data storage equipment

ASJC Scopus subject areas

  • Engineering(all)

Cite this

Ahmadyan, S. N., & Vasudevan, S. (2013). Reachability analysis of nonlinear analog circuits through iterative reachable set reduction. In Proceedings - Design, Automation and Test in Europe, DATE 2013 (pp. 1436-1441). [6513739]

Reachability analysis of nonlinear analog circuits through iterative reachable set reduction. / Ahmadyan, Seyed Nematollah; Vasudevan, Shobha.

Proceedings - Design, Automation and Test in Europe, DATE 2013. 2013. p. 1436-1441 6513739.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Ahmadyan, SN & Vasudevan, S 2013, Reachability analysis of nonlinear analog circuits through iterative reachable set reduction. in Proceedings - Design, Automation and Test in Europe, DATE 2013., 6513739, pp. 1436-1441, 16th Design, Automation and Test in Europe Conference and Exhibition, DATE 2013, Grenoble, France, 3/18/13.
Ahmadyan SN, Vasudevan S. Reachability analysis of nonlinear analog circuits through iterative reachable set reduction. In Proceedings - Design, Automation and Test in Europe, DATE 2013. 2013. p. 1436-1441. 6513739
Ahmadyan, Seyed Nematollah ; Vasudevan, Shobha. / Reachability analysis of nonlinear analog circuits through iterative reachable set reduction. Proceedings - Design, Automation and Test in Europe, DATE 2013. 2013. pp. 1436-1441
@inproceedings{30f26c2e8c1e420386cb85f64ce92dd7,
title = "Reachability analysis of nonlinear analog circuits through iterative reachable set reduction",
abstract = "We propose a methodology for reachability analysis of nonlinear analog circuits to verify safety properties. Our iterative reachable set reduction algorithm initially considers the entire state space as reachable. Our algorithm iteratively determines which regions in the state space are unreachable and removes those unreachable regions from the over approximated reachable set. We use the State Partitioning Tree (SPT) algorithm to recursively partition the reachable set into convex polytopes. We determine the reachability of adjacent neighbor polytopes by analyzing the direction of state space trajectories at the common faces between two adjacent polytopes. We model the direction of the trajectories as a reachability decision function that we solve using a sound root counting method. We are faithful to the nonlinearities of the system. We demonstrate the memory efficiency of our algorithm through computation of the reachable set of Van der Pol oscillation circuit.",
author = "Ahmadyan, {Seyed Nematollah} and Shobha Vasudevan",
year = "2013",
language = "English (US)",
isbn = "9783981537000",
pages = "1436--1441",
booktitle = "Proceedings - Design, Automation and Test in Europe, DATE 2013",

}

TY - GEN

T1 - Reachability analysis of nonlinear analog circuits through iterative reachable set reduction

AU - Ahmadyan, Seyed Nematollah

AU - Vasudevan, Shobha

PY - 2013

Y1 - 2013

N2 - We propose a methodology for reachability analysis of nonlinear analog circuits to verify safety properties. Our iterative reachable set reduction algorithm initially considers the entire state space as reachable. Our algorithm iteratively determines which regions in the state space are unreachable and removes those unreachable regions from the over approximated reachable set. We use the State Partitioning Tree (SPT) algorithm to recursively partition the reachable set into convex polytopes. We determine the reachability of adjacent neighbor polytopes by analyzing the direction of state space trajectories at the common faces between two adjacent polytopes. We model the direction of the trajectories as a reachability decision function that we solve using a sound root counting method. We are faithful to the nonlinearities of the system. We demonstrate the memory efficiency of our algorithm through computation of the reachable set of Van der Pol oscillation circuit.

AB - We propose a methodology for reachability analysis of nonlinear analog circuits to verify safety properties. Our iterative reachable set reduction algorithm initially considers the entire state space as reachable. Our algorithm iteratively determines which regions in the state space are unreachable and removes those unreachable regions from the over approximated reachable set. We use the State Partitioning Tree (SPT) algorithm to recursively partition the reachable set into convex polytopes. We determine the reachability of adjacent neighbor polytopes by analyzing the direction of state space trajectories at the common faces between two adjacent polytopes. We model the direction of the trajectories as a reachability decision function that we solve using a sound root counting method. We are faithful to the nonlinearities of the system. We demonstrate the memory efficiency of our algorithm through computation of the reachable set of Van der Pol oscillation circuit.

UR - http://www.scopus.com/inward/record.url?scp=84885626329&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84885626329&partnerID=8YFLogxK

M3 - Conference contribution

SN - 9783981537000

SP - 1436

EP - 1441

BT - Proceedings - Design, Automation and Test in Europe, DATE 2013

ER -