ch13.8.htm

介绍asci设计的一本书

 Gates;</P>
<P CLASS="Body">
<A NAME="pgfId=39620">
 </A>
To compare the reference and the derived models (two representations), formal verification performs the following steps: (1) the HDL is parsed, (2) a <SPAN CLASS="Definition">
finite-state machine compiler</SPAN>
<A NAME="marker=97789">
 </A>
 extracts the states present in any sequential logic, (3) a <SPAN CLASS="Definition">
proof generator</SPAN>
<A NAME="marker=97790">
 </A>
 automatically generates formulas to be proved, (4) the <SPAN CLASS="Definition">
theorem prover</SPAN>
<A NAME="marker=97783">
 </A>
 attempts to prove the formulas. The results from the last step are as follows:</P>
<P CLASS="ComputerFirst">
<A NAME="pgfId=40030">
 </A>
formulas to be proved:    8</P>
<P CLASS="ComputerLast">
<A NAME="pgfId=40031">
 </A>
formulas proved VALID:    8</P>
<P CLASS="Body">
<A NAME="pgfId=69963">
 </A>
By constructing and then proving formulas the software tells us that <SPAN CLASS="BodyComputer">
architecture</SPAN>
 <SPAN CLASS="BodyComputer">
RTL</SPAN>
 <SPAN CLASS="Emphasis">
implies</SPAN>
 <SPAN CLASS="BodyComputer">
architecture Gates</SPAN>
 (implication is the default proof mechanism&#8212;we could also have asked if the architectures are exactly equivalent). Next, we shall explore what this means and how formal verification works.</P>
</DIV>
<DIV>
<H2 CLASS="Heading2">
<A NAME="pgfId=39623">
 </A>
13.8.2&nbsp;Understanding Formal Verification</H2>
<P CLASS="BodyAfterHead">
<A NAME="pgfId=40656">
 </A>
The <SPAN CLASS="Definition">
formulas</SPAN>
<A NAME="marker=40340">
 </A>
 to be proved are generated in a separate file of <SPAN CLASS="Definition">
proof statements</SPAN>
<A NAME="marker=40360">
 </A>
:</P>
<P CLASS="ComputerFirstLabelV">
<A NAME="pgfId=40088">
 </A>
# axioms</P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40090">
 </A>
Let Axiom_ref = Axioms Of alarm-rtl</P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40091">
 </A>
Let Axiom_der = Axioms Of alarm-gates</P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40093">
 </A>
ProveNotAlwaysFalse (Axiom_ref)</P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40096">
 </A>
Prove (Axiom_ref =&gt; Axiom_der)</P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40100">
 </A>
# assertions</P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40102">
 </A>
Let Assert_ref = Asserts Of alarm-rtl</P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40103">
 </A>
Let Assert_der = Asserts Of alarm-gates</P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40105">
 </A>
Prove (Axiom_ref =&gt; (Assert_ref =&gt; Assert_der))</P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40109">
 </A>
# clocks</P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40111">
 </A>
Let ClockEvents_ref = Clocks Of alarm-rtl</P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40112">
 </A>
Let ClockEvents_der = Clocks Of alarm-gates</P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40113">
 </A>
Let Master__clock_event_ref = </P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40323">
 </A>
	Value (master__clock'event Of alarm-rtl)</P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40115">
 </A>
Prove (Axiom_ref =&gt; (ClockEvents_ref &lt;=&gt; ClockEvents_der))</P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40118">
 </A>
# next state of memories </P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40121">
 </A>
Prove ((Axiom_ref And Master__clock_event_ref) =&gt;</P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40122">
 </A>
(Transition (state(1) Of alarm-rtl) &lt;=&gt;</P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40123">
 </A>
Transition (state_ff_b1.t Of alarm-gates)))</P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40126">
 </A>
Prove ((Axiom_ref And Master__clock_event_ref) =&gt;</P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40127">
 </A>
(Transition (state(0) Of alarm-rtl) &lt;=&gt;</P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40128">
 </A>
Transition (state_ff_b0.t Of alarm-gates)))</P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40132">
 </A>
# validity value of outbuses</P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40134">
 </A>
Prove (Axiom_ref =&gt; (Domain (ring Of alarm-rtl) &lt;=&gt;</P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40135">
 </A>
Domain (ring Of alarm-gates)))</P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40136">
 </A>
Prove (Axiom_ref =&gt; (Domain (ring Of alarm-rtl) =&gt;</P>
<P CLASS="ComputerLabelV">
<A NAME="pgfId=40137">
 </A>
(Value (ring Of alarm-rtl) &lt;=&gt;</P>
<P CLASS="ComputerLastLabelV">
<A NAME="pgfId=40138">
 </A>
Value (ring Of alarm-gates))))</P>
<P CLASS="Body">
<A NAME="pgfId=40082">
 </A>
Formal verification makes strict use of the terms <SPAN CLASS="Emphasis">
axiom</SPAN>
 and <SPAN CLASS="Emphasis">
assertion</SPAN>
. An <SPAN CLASS="Definition">
axiom</SPAN>
<A NAME="marker=40331">
 </A>
 is an explicit or implicit fact. For example, if a VHDL signal is declared to be type <SPAN CLASS="BodyComputer">
BIT</SPAN>
, an implicit axiom is that this signal may only take the logic values <SPAN CLASS="BodyComputer">
'0'</SPAN>
 and <SPAN CLASS="BodyComputer">
'1'</SPAN>
. An <SPAN CLASS="Definition">
assertion</SPAN>
<A NAME="marker=40332">
 </A>
<A NAME="marker=40333">
 </A>
 is derived from a statement placed in the HDL code. For example, the following VHDL statement is an assertion:</P>
<P CLASS="ComputerFirst">
<A NAME="pgfId=40341">
 </A>
assert Key /= '1' or Trip /= '1' or NextState = Ringing</P>
<P CLASS="ComputerLast">
<A NAME="pgfId=40342">
 </A>
	report &quot;Alarm on and tripped but not ringing&quot;;</P>
<P CLASS="Body">
<A NAME="pgfId=40083">
 </A>
A VHDL <SPAN CLASS="BodyComputer">
assert </SPAN>
statement prints only if the condition is <SPAN CLASS="BodyComputer">
FALSE</SPAN>
. We know from de&nbsp;Morgan&#8217;s theorem that <SPAN CLASS="BodyComputer">
(A  +  B  +  C)'  =  A'B'C'</SPAN>
. Thus, this statement checks for a burglar alarm that does not ring when it is on and we are burgled.</P>
<P CLASS="Body">
<A NAME="pgfId=40396">
 </A>
In the proof statements the symbol<SPAN CLASS="BodyComputer">
 '=&gt;' </SPAN>
means <SPAN CLASS="Definition">
implies</SPAN>
<A NAME="marker=40329">
 </A>
. In logic calculus we write A <SPAN CLASS="Symbol">
&#8658;</SPAN>
 B to mean <SPAN CLASS="EquationVariables">
A</SPAN>
 implies <SPAN CLASS="EquationVariables">
B</SPAN>
. The symbol <SPAN CLASS="BodyComputer">
'&lt;=&gt;'</SPAN>
 means <SPAN CLASS="Definition">
equivalence</SPAN>
<A NAME="marker=40330">
 </A>
, and this is stricter than implication. We write A <SPAN CLASS="Symbol">
&#164;</SPAN>
 B to mean: <SPAN CLASS="EquationVariables">
A</SPAN>
 is equivalent to <SPAN CLASS="EquationVariables">
B</SPAN>
. <A HREF="CH13.8.htm#32152" CLASS="XRef">
Table&nbsp;13.13</A>
 show the truth tables for these two logic operators.</P>
<TABLE>
<TR>
<TH ROWSPAN="1" COLSPAN="4">
<P CLASS="TableTitle">
<A NAME="pgfId=70068">
 </A>
TABLE&nbsp;13.13&nbsp;<A NAME="32152">
 </A>
Implication and equivalence.</P>
</TH>
</TR>
<TR>
<TD ROWSPAN="1" COLSPAN="1">
<P CLASS="TableFirst">
<A NAME="pgfId=70076">
 </A>
A</P>
</TD>
<TD ROWSPAN="1" COLSPAN="1">
<P CLASS="TableFirst">
<A NAME="pgfId=70078">
 </A>
B</P>
</TD>
<TD ROWSPAN="1" COLSPAN="1">
<P CLASS="TableFirst">
<A NAME="pgfId=70080">
 </A>
A <SPAN CLASS="Symbol">
&#8658;</SPAN>
 B</P>
</TD>
<TD ROWSPAN="1" COLSPAN="1">
<P CLASS="TableFirst">
<A NAME="pgfId=70082">
 </A>
A <SPAN CLASS="Symbol">
&#164;</SPAN>
 B</P>
</TD>
</TR>
<TR>
<TD ROWSPAN="1" COLSPAN="1">
<P CLASS="Table">
<A NAME="pgfId=70084">
 </A>
F</P>
</TD>
<TD ROWSPAN="1" COLSPAN="1">
<P CLASS="Table">
<A NAME="pgfId=70086">
 </A>
F</P>
</TD>
<TD ROWSPAN="1" COLSPAN="1">
<P CLASS="Table">
<A NAME="pgfId=70088">
 </A>
T</P>
</TD>
<TD ROWSPAN="1" COLSPAN="1">
<P CLASS="Table">
<A NAME="pgfId=70090">
 </A>
T</P>
</TD>
</TR>
<TR>
<TD ROWSPAN="1" COLSPAN="1">
<P CLASS="Table">
<A NAME="pgfId=70092">
 </A>
F</P>
</TD>
<TD ROWSPAN="1" COLSPAN="1">
<P CLASS="Table">
<A NAME="pgfId=70094">
 </A>
T</P>
</TD>
<TD ROWSPAN="1" COLSPAN="1">
<P CLASS="Table">
<A NAME="pgfId=70096">
 </A>
T</P>
</TD>
<TD ROWSPAN="1" COLSPAN="1">
<P CLASS="Table">
<A NAME="pgfId=70098">
 </A>
F</P>
</TD>
</TR>
<TR>
<TD ROWSPAN="1" COLSPAN="1">
<P CLASS="Table">
<A NAME="pgfId=70100">
 </A>
T</P>
</TD>
<TD ROWSPAN="1" COLSPAN="1">
<P CLASS="Table">
<A NAME="pgfId=70102">
 </A>
F</P>
</TD>
<TD ROWSPAN="1" COLSPAN="1">
<P CLASS="Table">
<A NAME="pgfId=70104">
 </A>
F</P>
</TD>
<TD ROWSPAN="1" COLSPAN="1">
<P CLASS="Table">
<A NAME="pgfId=70106">
 </A>
F</P>
</TD>
</TR>
<TR>
<TD ROWSPAN="1" COLSPAN="1">
<P CLASS="Table">
<A NAME="pgfId=70108">
 </A>
T</P>
</TD>
<TD ROWSPAN="1" COLSPAN="1">
<P CLASS="Table">
<A NAME="pgfId=70110">
 </A>
T</P>
</TD>
<TD ROWSPAN="1" COLSPAN="1">
<P CLASS="Table">
<A NAME="pgfId=70112">
 </A>
T</P>
</TD>
<TD ROWSPAN="1" COLSPAN="1">
<P CLASS="Table">
<A NAME="pgfId=70114">
 </A>
T</P>
</TD>
</TR>
</TABLE>
</DIV>
<DIV>
<H2 CLASS="Heading2">
<A NAME="pgfId=40462">
 </A>
13.8.3&nbsp;Adding an Assertion</H2>
<P CLASS="BodyAfterHead">
<A NAME="pgfId=40657">
 </A>
If we include the <SPAN CLASS="BodyComputer">
assert</SPAN>
 statement from the previous section in <SPAN CLASS="BodyComputer">
architecture RTL</SPAN>
 and repeat formal verification, we get the following message from the FSM compiler:</P>
<P CLASS="ComputerFirst">
<A NAME="pgfId=40520">
 </A>
&lt;E&gt;  Assertion may be violated</P>
<P CLASS="Computer">
<A NAME="pgfId=40521">
 </A>
SEVERITY: ERROR</P>
<P CLASS="Computer">
<A NAME="pgfId=40522">
 </A>
REPORT: Alarm on and tripped but not ringing</P>