📄 ch13.8.htm
字号:
<P CLASS="Computer">
<A NAME="pgfId=40523">
</A>
FILE: .../alarm-rtl3.vhdl</P>
<P CLASS="Computer">
<A NAME="pgfId=40524">
</A>
FSM: alarm-rtl3</P>
<P CLASS="Computer">
<A NAME="pgfId=40525">
</A>
STATEMENT or DECLARATION: line8</P>
<P CLASS="Computer">
<A NAME="pgfId=40526">
</A>
.../alarm-rtl3.vhdl (line 8)</P>
<P CLASS="Computer">
<A NAME="pgfId=40527">
</A>
Context of the message is:</P>
<P CLASS="ComputerLast">
<A NAME="pgfId=40515">
</A>
(key And trip And memoryofdriver__state(0))</P>
<P CLASS="BodyAfterHead">
<A NAME="pgfId=40517">
</A>
This message tells us that the <SPAN CLASS="BodyComputer">
assert</SPAN>
statement that we included may be triggered under a certain condition: <SPAN CLASS="BodyComputer">
(key And trip And state(0))</SPAN>
. The prefix <SPAN CLASS="BodyComputer">
'memoryofdriver__'</SPAN>
is used by the theorem prover to refer to the memory element used for <SPAN CLASS="BodyComputer">
state(0)</SPAN>
. The state <SPAN CLASS="BodyComputer">
'off'</SPAN>
in the reference model corresponds to <SPAN CLASS="BodyComputer">
state(0)</SPAN>
in the encoding that the finite-state machine compiler has used (and also to <SPAN CLASS="BodyComputer">
state(0)</SPAN>
in the derived model). From this message we can isolate the problem to the following <SPAN CLASS="BodyComputer">
case</SPAN>
statement (the line numbers follow the original code in <SPAN CLASS="BodyComputer">
architecture RTL</SPAN>
):</P>
<P CLASS="ComputerFirstLabel">
<A NAME="pgfId=40681">
</A>
<B CLASS="Keyword">
case</B>
State <B CLASS="Keyword">
is</B>
</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=40682">
</A>
<B CLASS="Keyword">
when</B>
Off => <B CLASS="Keyword">
if</B>
Key = '1' <B CLASS="Keyword">
then</B>
State <= Armed; <B CLASS="Keyword">
end</B>
<B CLASS="Keyword">
if</B>
;</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=40683">
</A>
<B CLASS="Keyword">
when</B>
Armed => <B CLASS="Keyword">
if</B>
Key = '0' <B CLASS="Keyword">
then</B>
State <= Off;</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=40664">
</A>
<B CLASS="Keyword">
elsif</B>
Trip = '1' <B CLASS="Keyword">
then</B>
State <= Ringing;</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=40665">
</A>
<B CLASS="Keyword">
end</B>
<B CLASS="Keyword">
if</B>
;</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=40666">
</A>
<B CLASS="Keyword">
when</B>
Ringing => <B CLASS="Keyword">
if</B>
Key = '0' <B CLASS="Keyword">
then</B>
State <= Off; <B CLASS="Keyword">
end</B>
<B CLASS="Keyword">
if</B>
;</P>
<P CLASS="ComputerLastLabel">
<A NAME="pgfId=40667">
</A>
<B CLASS="Keyword">
end</B>
<B CLASS="Keyword">
case</B>
;</P>
<P CLASS="Body">
<A NAME="pgfId=119843">
</A>
When we start in state <SPAN CLASS="BodyComputer">
Off</SPAN>
and the two inputs are <SPAN CLASS="BodyComputer">
Trip = '1'</SPAN>
and <SPAN CLASS="BodyComputer">
Key = '1'</SPAN>
, we go to state<SPAN CLASS="BodyComputer">
Armed</SPAN>
, and not to state <SPAN CLASS="BodyComputer">
Ringing</SPAN>
. On the subsequent clock cycle we will go state <SPAN CLASS="BodyComputer">
Ringing</SPAN>
, but only if <SPAN CLASS="BodyComputer">
Trip</SPAN>
does not change. Since we have all seen “Mission Impossible” and the burglar who exits the top-secret computer room at the Pentagon at the exact moment the alarm is set, we know this is perfectly possible and the software is warning us of this fact. Continuing on, we get the following results from the theorem prover:</P>
<P CLASS="ComputerFirst">
<A NAME="pgfId=40475">
</A>
Prove (Axiom_ref => (Assert_ref => Assert_der))</P>
<P CLASS="Computer">
<A NAME="pgfId=40476">
</A>
Formula is NOT VALID</P>
<P CLASS="ComputerLast">
<A NAME="pgfId=40477">
</A>
But is VALID under Assert Context of alarm-rtl3</P>
<P CLASS="Body">
<A NAME="pgfId=40468">
</A>
We included the <SPAN CLASS="BodyComputer">
assert</SPAN>
statement in the reference model (<SPAN CLASS="BodyComputer">
architecture RTL</SPAN>
) but not in the derived model (<SPAN CLASS="BodyComputer">
architecture Gates</SPAN>
). Now we are really mixed up: The <SPAN CLASS="BodyComputer">
assertion</SPAN>
statement in the reference model says one thing, but the <SPAN CLASS="BodyComputer">
case</SPAN>
statement in the reference model describes another. The theorem prover retorts: “The axioms of the reference model do not imply that the assertions of the reference model imply the assertions of the derived model.” Translation: “These two architectures differ in some way.” However, if we assume that the assertion is true (despite what the <SPAN CLASS="BodyComputer">
case</SPAN>
statement says) then the formula is true. The prover is also saying: “Make up your mind, you cannot have it both ways.” The prover goes on to explain the differences between the two representations:</P>
<P CLASS="ComputerFirst">
<A NAME="pgfId=70212">
</A>
***Difference is:</P>
<P CLASS="Computer">
<A NAME="pgfId=70213">
</A>
(Not state(1) And key And state(0) And trip)</P>
<P CLASS="Computer">
<A NAME="pgfId=70214">
</A>
There are 1 cubes and 4 literals in the complete equation</P>
<P CLASS="Computer">
<A NAME="pgfId=70215">
</A>
</P>
<P CLASS="Computer">
<A NAME="pgfId=70216">
</A>
***Local Variable Assert_der is:</P>
<P CLASS="Computer">
<A NAME="pgfId=70217">
</A>
Not key Or Not state(0) Or Not trip</P>
<P CLASS="Computer">
<A NAME="pgfId=70218">
</A>
There are 3 cubes and 3 literals in the complete equation</P>
<P CLASS="Computer">
<A NAME="pgfId=70219">
</A>
</P>
<P CLASS="Computer">
<A NAME="pgfId=70220">
</A>
***Local Variable Assert_ref is: 1</P>
<P CLASS="Computer">
<A NAME="pgfId=70221">
</A>
</P>
<P CLASS="Computer">
<A NAME="pgfId=70222">
</A>
***Local Variable Axiom_ref is:</P>
<P CLASS="Computer">
<A NAME="pgfId=70223">
</A>
Not state(1) Or Not state(0)</P>
<P CLASS="Computer">
<A NAME="pgfId=70224">
</A>
There are 2 cubes and 2 literals in the complete equation</P>
<P CLASS="Computer">
<A NAME="pgfId=70225">
</A>
</P>
<P CLASS="Computer">
<A NAME="pgfId=70226">
</A>
formulas to be proved: 8</P>
<P CLASS="Computer">
<A NAME="pgfId=70227">
</A>
formulas proved VALID: 7</P>
<P CLASS="ComputerLast">
<A NAME="pgfId=70228">
</A>
formulas VALID under assert context of der.model: 1</P>
<P CLASS="BodyAfterHead">
<A NAME="pgfId=70209">
</A>
Study these messages hard and you will see that the differences between the two models are consistent with our explanation.</P>
</DIV>
<DIV>
<H2 CLASS="Heading2">
<A NAME="pgfId=40469">
</A>
13.8.4 Completing a Proof</H2>
<P CLASS="BodyAfterHead">
<A NAME="pgfId=40915">
</A>
To fix the problem we change the code as follows:</P>
<P CLASS="ComputerFirst">
<A NAME="pgfId=40916">
</A>
...<B CLASS="Keyword">
</B>
</P>
<P CLASS="Computer">
<A NAME="pgfId=70249">
</A>
<B CLASS="Keyword">
case</B>
State <B CLASS="Keyword">
is</B>
</P>
<P CLASS="Computer">
<A NAME="pgfId=40917">
</A>
<B CLASS="Keyword">
when</B>
Off => <B CLASS="Keyword">
if</B>
Key = '1' <B CLASS="Keyword">
then</B>
</P>
<P CLASS="Computer">
<A NAME="pgfId=40918">
</A>
<B CLASS="Keyword">
if</B>
Trip = '1' <B CLASS="Keyword">
then</B>
NextState <= Ringing;</P>
<P CLASS="Computer">
<A NAME="pgfId=40919">
</A>
<B CLASS="Keyword">
else</B>
NextState <= Armed;</P>
<P CLASS="Computer">
<A NAME="pgfId=40920">
</A>
<B CLASS="Keyword">
end</B>
<B CLASS="Keyword">
if</B>
;</P>
<P CLASS="Computer">
<A NAME="pgfId=40921">
</A>
<B CLASS="Keyword">
end</B>
<B CLASS="Keyword">
if</B>
;</P>
<P CLASS="Computer">
<A NAME="pgfId=40922">
</A>
<B CLASS="Keyword">
when</B>
Armed => <B CLASS="Keyword">
if</B>
Key = '0' <B CLASS="Keyword">
then</B>
NextState <= Off;</P>
<P CLASS="Computer">
<A NAME="pgfId=40923">
</A>
<B CLASS="Keyword">
elsif</B>
Trip = '1' <B CLASS="Keyword">
then</B>
NextState <= Ringing;</P>
<P CLASS="Computer">
<A NAME="pgfId=40924">
</A>
<B CLASS="Keyword">
end</B>
<B CLASS="Keyword">
if</B>
;</P>
<P CLASS="Computer">
<A NAME="pgfId=40925">
</A>
<B CLASS="Keyword">
when</B>
Ringing => <B CLASS="Keyword">
if</B>
Key = '0' <B CLASS="Keyword">
then</B>
NextState <= Off; <B CLASS="Keyword">
end</B>
<B CLASS="Keyword">
if</B>
;</P>
<P CLASS="Computer">
<A NAME="pgfId=40926">
</A>
<B CLASS="Keyword">
end</B>
<B CLASS="Keyword">
case</B>
; </P>
<P CLASS="ComputerLast">
<A NAME="pgfId=70250">
</A>
...</P>
<P CLASS="Body">
<A NAME="pgfId=40658">
</A>
This results in a minor change in the synthesized netlist, </P>
<P CLASS="ComputerFirst">
<A NAME="pgfId=70252">
</A>
g2: Inverter port map ( i => State(0), z => s1 );</P>
<P CLASS="Computer">
<A NAME="pgfId=70253">
</A>
g3: NAnd2 port map ( a => s1, b => State(1), z => s2 );</P>
<P CLASS="Computer">
<A NAME="pgfId=70254">
</A>
g4: Inverter port map ( i => s2, z => Ring );</P>
<P CLASS="Computer">
<A NAME="pgfId=70255">
</A>
g5: NAnd2 port map ( a => State(1), b => Key, z => s0 );</P>
<P CLASS="Computer">
<A NAME="pgfId=70256">
</A>
g6: NAnd3 port map ( a => Trip, b => s1, c => Key, z => s3 );</P>
<P CLASS="Computer">
<A NAME="pgfId=70257">
</A>
g7: NAnd2 port map ( a => s0, b => s3, z => NextState(1) );</P>
<P CLASS="Computer">
<A NAME="pgfId=70258">
</A>
g8: Inverter port map ( i => Key, z => NextState(0) );</P>
<P CLASS="Computer">
<A NAME="pgfId=70259">
</A>
state_ff_b0: DFF port map ( d => NextState(0), c => Clock, q => State(0), qn => open );</P>
<P CLASS="ComputerLast">
<A NAME="pgfId=70261">
</A>
state_ff_b1: DFF port map ( d => NextState(1), c => Clock, q => State(1), qn => open );</P>
<P CLASS="Body">
<A NAME="pgfId=70271">
</A>
Repeating the formal verification confirms and formally proves that the derived model will operate correctly. Strictly, we say that the operation of the derived model is implied by the reference model.</P>
</DIV>
<HR>
<DIV CLASS="footnotes">
<DIV CLASS="footnote">
<P CLASS="FootnoteRegular">
<SPAN CLASS="footnoteNumber">
1.</SPAN>
<A NAME="pgfId=119243">
</A>
By one of the architects of the Compass VFormal software, Erich Marschner.</P>
</DIV>
</DIV>
<HR><P>[ <A HREF="CH13.htm">Chapter start</A> ] [ <A HREF="CH13.7.htm">Previous page</A> ] [ <A HREF="CH13.9.htm">Next page</A> ]</P></BODY>
<!--#include file="Copyright.html"--><!--#include file="footer.html"-->
⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -