当前位置：文档之家 › Generating and Model Checking a Hierarchy of Abstract Models

Generating and Model Checking a Hierarchy of Abstract Models

  • 格式：pdf
  • 大小：293.47 KB
  • 文档页数：34

GeneratingandModelCheckingaHierarchyofAbstractModels

ScottHazelhurst

ProgrammeforHighlyDependableSystems

DepartmentofComputerScience

UniversityoftheWitwatersrand,Johannesburg

2050Wits,SouthAfrica

scott@cs.wits.ac.za

2March1999

Abstract

Theuseofautomaticmodelcheckingalgorithmstoverifydetailedgateorswitchleveldesignsofcircuitsisveryattractivebecausethemethodisautomaticandsuchmodelscanaccuratelycapturede-tailedfunctional,timing,andevensubtleelectricalbehaviourofcircuits.Theuseofbinarydecisiondiagramshasextendedbyordersofmagnitudethesizeofcircuitsthatcanbesoverified,buttherearestillverysignificantlimitationsduetothecomputationalcomplexityoftheproblem.Verifyingabstractversionsofthemodelisattractivetoreducecomputationalcostsbutthisposestheproblemofhowtobuildabstractionseasilywithoutlosingtheaccuracyofthelow-levelmodel.Thispaperproposesamethodofbridgingthegapbetweendetaileddesignsandabstractmod-els,andpresentspreliminarytheoreticalandexperimentalresults.Startingwithadetailed,low-levelmodelofacircuit(whichusesBDDsforrepresentingdata),thehumanverifierpicksasetofprop-ertiesthats/hebelievescharacterisesthecircuit.Thesepropertiesareautomaticallyverifiedbyamodelcheckingalgorithm.Onceproved,thesepropertiesareusedtosynthesiseautomaticallyanabstractmodelofthecircuit,whichcanusesymbolicrepresentationofdata.Anautomaticmodelcheckingalgorithmcanthenbeappliedtotheabstractmodeltoverifymorepropertiesofthecircuit.Thepreliminaryresults,althoughlimited,werepromising:theabstractioncouldbeconstructedandverifiedwithrelativelymodestcost,therebyreducingthehumancostofverificationsignificantly.

1Introduction

1.1Motivation

Thedevelopmentofefficientmodelcheckingalgorithms(suchas[6,25])basedonbinarydecision

diagrams(BDDs)hasmeantthatautomaticverificationmethodsarenowapplicabletoawiderange

ofcircuits.However,althoughtheuseofBDDshasextendedthesizeofcircuitsthatcanbeverified

byordersofmagnitude,theydonotchangetheunderlyingcomputationalcomplexitycostsofmodel

checking,andatthesametimehavetheirownlimitations.

Thelastfewyearshaveseenconsiderableworkbeingputintoextendingmodelcheckingalgorithms

todealwiththeselimitations.Onetackhasbeentousemethodssuchasabstractionandcompositionality,

oftencombinedwiththeuseoftheoremproving[8,13,17,20,21,23].Thishasbeenveryeffective,but

hasthedrawbackthatsignificanthumaninterventionisoftenneeded,ordatapathortiminginformation

isabstractedaway(whichisnotalwaysappropriate).

Anothertackhasbeenextendingtherangeofdatastructuresusedinthemodelcheckingprocess,

andtheuseofmoreadvanceddecisiondiagramshasbeenveryeffective(forexamples,see[5,7]).The

difficultywiththisisthatoftenthestartingpointforverificationisadesigngivenatthegateorswitch

level,forwhichthenaturaldatarepresentationtouseisBDDs.Althoughworkisbeingdoneatbeing

abletogeneratemoreabstractmodelsdirectlyfromcircuitdescriptions,thisisnotalwayspossible,

particularlywhenitisimportanttocaptureelectricalordetailedtimingpropertiesofthecircuit.Thus

1astartingpointofthispaperisthatverifyingcircuitswhichhavemodelsthatarenaturallyrepresented

usingBDDs(orequivalentdatastructures)willremainanimportantproblemtobesolved.

1.2ResearchProblem

Thispaperproposesamethodofabstraction,therebybridgingthegapbetweenthelow-levelmodel

extractedautomaticallyfromacircuitdescriptionandhigherlevelmethodsofdatarepresentation.The

focusoftheabstractionmechanismistoidentifystructureinthecircuit,whichallowsmorepowerful

datarepresentationmethodstobeused.

Thebasicapproachisasfollows.Supposethatwehavesomemodelwhichwewishtoverify,

andthatisnaturallyrepresentedataverydetailedlevelusingdatastructuressuchasBDDs.

Thehumanverifierselectsasetofpropertieswhichs/hebelievesaretheimportant

propertiesthatcharacterisethecircuit.

Eachpropertyisverifiedautomaticallyusingamodelcheckingalgorithm.

Amodelisgeneratedautomaticallyfromtheproperties.isanabstraction

ofinthefollowingsense:everypropertythatistrueofistrueof,andeveryproperty

thatisfalseofisfalseof.(Therewillbesomepropertiesofthatareneithertruenor

falseof.)Eachandanypropertiesinferablefromthewillbetrueof.

Thekeyhereisthathasahigher-levelrepresentation.WhileBDDsmaystillbeusedto

representbooleandata,otherdatastructureswillbeusedfordatasuchasintegersandvectors.

Thehumanverifierusesanautomaticmodelcheckingalgorithmontoverifymoreproperties.

Inprinciple,theprocessofabstractingcouldbecarriedoutatanumberofdifferentlevels.

Theideaofconstructingamodelfromasetofpropertiesisacommononeinthestudyoflogic(es-

pecially,thestudyoflogicincomputerscience).Thecontributionofthispaperistoshowhowsuch

constructioncanbedoneforcircuitmodels.Thesignificanceofthisisthatitprovidesapracticalwayof

creatingabstractionwithrelativelyminimalhumanintervention.Thisabstractioninturncanbeusedfor

合集下载

Keynote

Keynote

Benoit Baudry, Alain Faivre, Sudipto Ghosh, Alexander Pretschner (Eds.)

Proceedings

of the

4th MoDeVVa workshop

Model-Driven Engineering, Verification and

Validation

October 2nd, 2007

In conjunction with MoDELS’07, Nashville, TN, USA

ISBN 2-7261-1294 3 Preface

Development processes that rely on Model-Driven Engineering (MDE) make extensive use of

models and automatic model transformations to handle complex software developments. A

plethora of software artifacts, tools, environments and modeling languages have to be developed

to make MDE a reality. Consequently, there is a pressing need for effective verification and

validation (V&V) techniques in this new context. The novelty of this development paradigm

gives rise to questions concerning its impact on traditional V&V techniques, and how they can

leverage this new approach.

心理学专业词汇G

心理学专业词汇G

G factor G 因素

G factor 一般因素

G period

G period G 期

G score 年级分数

G tolerance G 耐力

G 期 G 期

GA 总平均数

gab 空谈

GABA γ氨基丁酸

gabble 急促不清的说话

gabby 健谈的

gaby 傻子

GAD 泛焦虑症

gad 游荡

gaffe 失礼

gag reflex 咽反射

gage 量规

Gagnes accumulative learning theory 加涅的累积学习论

Gagnes hierarchy of learning 加涅的学习层次

Gagnes hierarchy system of learning 加涅的学习层次系统

Gagnes learning model 加涅的学习模型

Gagnes learning outcome variety 加涅的学习结果种类

Gagnes stages of learning 加涅的学习阶段

Gagnes theory of instruction 加涅的教学论

gaiety 快乐

gain 增益

gain experience 获得经验

gain from illness 因病得益

gaining new insights through restudying the old material 温故知新

gainsharing 收入分成

gainloss hypothesis 得失说

gainloss model 得失模型

gainloss theory 得失论

gait 步态

galactochloral 半乳糖氯醛

galactosemia 半乳糖血

galeanthropia 变猫妄想

TMAX精简教程

TMAX精简教程

一、TMAX的使用

1. 工具接口

Basic input of TetraMAX to perform ATPG are the vendor gate-level simulation

libraries, design netlist, command script and test procedure file. Main output data are

the test patterns and reports on results. In order to read in netlist and library files, use

the “read netlist” command or the Netlist button of the GUI. The netlist format

(Verilog, EDIF, VHDL) is automatically detected. It is recommended you use Verilog

as the netlist input format. TetraMAX also automatically detects netlist compression

(none, GZIP, proprietary binary). A single file may contain one or more modules. By

using multiple files, mixed language netlists are supported. A single read command

may use wildcards to match multiple files using the „?‟ and „*‟ characters.

Example:

read netlist /proj/mars/lander/shared/*/??DFF*.v

帕金森定律

帕金森定律

Chapter1 Study skills for business learning

帕金森定律（Parkinson's Law） s

What is the implication of Parkinson's Law?

The demand upon a resource tends to expand to match the supply of the resource.

This generalization has become very similar to the economic law of demand; that the lower the price of a service or commodity, the greater the quantity demanded

Time management models

Method 1: Task list: a list of tasks to be completed, Model 2: The Eisenhower Method

Method3: POSEC method

Prioritize, organizing, streamlining, economizing, contributing,

Method4： Pareto analysis :80-20 rule (80% of tasks can be completed in 20% of the disposable

time. The remaining 20% of tasks will take up 80% of the time. )

Prioritize, organizing, Streamlining,(使流线型，使简单化） Economizing and Contributing

Chapter2 Management and Managers