📄 ch13.8.htm
字号:
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML EXPERIMENTAL 970324//EN">
<HTML>
<HEAD>
<META NAME="GENERATOR" CONTENT="Adobe FrameMaker 5.5/HTML Export Filter">
<TITLE> 13.8 Formal Verification</TITLE></HEAD><!--#include file="top.html"--><!--#include file="header.html"-->
<DIV>
<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><!--#include file="AmazonAsic.html"--><HR></DIV>
<H1 CLASS="Heading1">
<A NAME="pgfId=38974">
</A>
13.8 <A NAME="10040">
</A>
Formal Verification</H1>
<P CLASS="BodyAfterHead">
<A NAME="pgfId=69935">
</A>
Using logic synthesis we move from a behavioral model to a structural model. How are we to know (other than by trusting the logic synthesizer) that the two representations are the same? We have already seen that we may have to alter the original reference model because the HDL acceptable to a synthesis tool is a subset of HDL acceptable to simulators. <SPAN CLASS="Definition">
Formal verification</SPAN>
<A NAME="marker=69945">
</A>
can prove, in the mathematical sense, that two representations are equivalent. If they are not, the software can tell us why and how two representations differ.</P>
<DIV>
<H2 CLASS="Heading2">
<A NAME="pgfId=39033">
</A>
13.8.1 <A NAME="19438">
</A>
An Example</H2>
<P CLASS="BodyAfterHead">
<A NAME="pgfId=39358">
</A>
We shall use the following VHDL entity with two architectures as an example:<A HREF="#pgfId=119243" CLASS="footnote">
1</A>
</P>
<P CLASS="ComputerFirstLabel">
<A NAME="pgfId=39361">
</A>
<B CLASS="Keyword">
entity</B>
Alarm <B CLASS="Keyword">
is</B>
</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39377">
</A>
<B CLASS="Keyword">
port</B>
(Clock, Key, Trip : <B CLASS="Keyword">
in</B>
bit; Ring : <B CLASS="Keyword">
out</B>
bit); </P>
<P CLASS="ComputerLastLabel">
<A NAME="pgfId=39378">
</A>
<B CLASS="Keyword">
end</B>
Alarm;</P>
<P CLASS="Body">
<A NAME="pgfId=39359">
</A>
The following behavioral architecture is the <SPAN CLASS="Definition">
reference model</SPAN>
<A NAME="marker=40315">
</A>
:</P>
<P CLASS="ComputerFirstLabel">
<A NAME="pgfId=39385">
</A>
<B CLASS="Keyword">
architecture</B>
RTL <B CLASS="Keyword">
of</B>
Alarm <B CLASS="Keyword">
is</B>
</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39387">
</A>
<B CLASS="Keyword">
type</B>
States <B CLASS="Keyword">
is</B>
(Armed, Off, Ringing); <B CLASS="Keyword">
signal</B>
State : States;</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39390">
</A>
<B CLASS="Keyword">
begin</B>
</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39392">
</A>
<B CLASS="Keyword">
process </B>
(Clock) <B CLASS="Keyword">
begin</B>
</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39394">
</A>
<B CLASS="Keyword">
if</B>
Clock = '1' <B CLASS="Keyword">
and</B>
Clock'EVENT <B CLASS="Keyword">
then</B>
</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39395">
</A>
<B CLASS="Keyword">
case</B>
State <B CLASS="Keyword">
is</B>
</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39396">
</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=39400">
</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=39403">
</A>
<B CLASS="Keyword">
elsif</B>
Trip = '1' <B CLASS="Keyword">
then</B>
State <= Ringing;</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39405">
</A>
<B CLASS="Keyword">
end</B>
<B CLASS="Keyword">
if</B>
;</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39406">
</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="ComputerLabel">
<A NAME="pgfId=39410">
</A>
<B CLASS="Keyword">
end</B>
<B CLASS="Keyword">
case</B>
;</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39411">
</A>
<B CLASS="Keyword">
end</B>
<B CLASS="Keyword">
if</B>
;</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39412">
</A>
<B CLASS="Keyword">
end</B>
<B CLASS="Keyword">
process</B>
;</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39414">
</A>
Ring <= '1' <B CLASS="Keyword">
when</B>
State = Ringing <B CLASS="Keyword">
else</B>
'0';</P>
<P CLASS="ComputerLastLabel">
<A NAME="pgfId=39416">
</A>
<B CLASS="Keyword">
end</B>
RTL;</P>
<P CLASS="Body">
<A NAME="pgfId=39379">
</A>
The following synthesized structural architecture is the <SPAN CLASS="Definition">
derived model</SPAN>
<A NAME="marker=40316">
</A>
:</P>
<P CLASS="ComputerFirstLabel">
<A NAME="pgfId=39625">
</A>
<B CLASS="Keyword">
library</B>
cells; <B CLASS="Keyword">
use</B>
cells.<B CLASS="Keyword">
all</B>
; // ...contains logic cell models</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39628">
</A>
<B CLASS="Keyword">
architecture</B>
Gates <B CLASS="Keyword">
of</B>
Alarm <B CLASS="Keyword">
is</B>
</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39630">
</A>
<B CLASS="Keyword">
component</B>
Inverter <B CLASS="Keyword">
port</B>
(i : <B CLASS="Keyword">
in</B>
BIT;z : <B CLASS="Keyword">
out</B>
BIT) ; <B CLASS="Keyword">
end</B>
<B CLASS="Keyword">
component</B>
;</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39634">
</A>
<B CLASS="Keyword">
component</B>
NAnd2 <B CLASS="Keyword">
port</B>
(a,b : <B CLASS="Keyword">
in</B>
BIT;z : <B CLASS="Keyword">
out</B>
BIT) ; <B CLASS="Keyword">
end</B>
<B CLASS="Keyword">
component</B>
;</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39638">
</A>
<B CLASS="Keyword">
component</B>
NAnd3 <B CLASS="Keyword">
port</B>
(a,b,c : <B CLASS="Keyword">
in</B>
BIT;z : <B CLASS="Keyword">
out</B>
BIT) ; <B CLASS="Keyword">
end</B>
<B CLASS="Keyword">
component</B>
;</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39642">
</A>
<B CLASS="Keyword">
component</B>
DFF port(d,c : <B CLASS="Keyword">
in</B>
BIT; q,qn : <B CLASS="Keyword">
out</B>
BIT) ; <B CLASS="Keyword">
end</B>
<B CLASS="Keyword">
component</B>
;</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39646">
</A>
<B CLASS="Keyword">
signal</B>
State, NextState : BIT_VECTOR(1 <B CLASS="Keyword">
downto</B>
0);</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39647">
</A>
<B CLASS="Keyword">
signal</B>
s0, s1, s2, s3 : BIT;</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39649">
</A>
<B CLASS="Keyword">
begin</B>
</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39651">
</A>
g2: Inverter <B CLASS="Keyword">
port</B>
<B CLASS="Keyword">
map</B>
( i => State(0), z => s1 );</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39652">
</A>
g3: NAnd2 <B CLASS="Keyword">
port</B>
<B CLASS="Keyword">
map</B>
( a => s1, b => State(1), z => s2 );</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39653">
</A>
g4: Inverter <B CLASS="Keyword">
port</B>
<B CLASS="Keyword">
map</B>
( i => s2, z => Ring );</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39654">
</A>
g5: NAnd2 <B CLASS="Keyword">
port</B>
<B CLASS="Keyword">
map</B>
( a => State(1), b => Key, z => s0 );</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39655">
</A>
g6: NAnd3 <B CLASS="Keyword">
port</B>
<B CLASS="Keyword">
map</B>
( a => Trip, b => s1, c => Key, z => s3 );</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39656">
</A>
g7: NAnd2 <B CLASS="Keyword">
port</B>
<B CLASS="Keyword">
map</B>
( a => s0, b => s3, z => NextState(1) );</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39657">
</A>
g8: Inverter <B CLASS="Keyword">
port</B>
<B CLASS="Keyword">
map</B>
( i => Key, z => NextState(0) );</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39658">
</A>
state_ff_b0: DFF <B CLASS="Keyword">
port</B>
<B CLASS="Keyword">
map</B>
</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39753">
</A>
( d => NextState(0), c => Clock, q => State(0), qn => <B CLASS="Keyword">
open</B>
);</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39660">
</A>
state_ff_b1: DFF <B CLASS="Keyword">
port</B>
<B CLASS="Keyword">
map</B>
</P>
<P CLASS="ComputerLabel">
<A NAME="pgfId=39763">
</A>
( d => NextState(1), c => Clock, q => State(1), qn => <B CLASS="Keyword">
open</B>
);</P>
<P CLASS="ComputerLastLabel">
<A NAME="pgfId=39663">
</A>
<B CLASS="Keyword">
end</B>
⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -