ch13.8.htm
来自「介绍asci设计的一本书」· HTM 代码 · 共 1,232 行 · 第 1/3 页
HTM
1,232 行
<!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 + =
减小字号Ctrl + -
显示快捷键?