Sir
(1)For the FSM code below,taking "ald" as MSB, and bits
for moorestate as LSB's
[0,1,2,3,4,5,6,7] are the 8 states.
please tell me what are the
"reachable states set" and "unreachable states set".
(2)Please tell me the same for the counter code.
How does,skip of reachability analysis for proving the property "AG(clatched=1->AX(q[20:0]=0))" saves time?
Also how does this case differs from the case which
includes reachability analysis?
******************FSM CODE*****************************
module moorefsm(a,clkm);
input a,clkm;
reg ald;
parameter s0=0,s1=1,s2=2,s3=3;
reg [1:0] moorestate;
initial ald=a;
initial moorestate=s0;
always@(posedge clkm)
ald=a;
always@(posedge clkm)
case(moorestate)
s0:moorestate=(!ald)?s0:s2;
s1:moorestate=(!ald)?s0:s2;
s2:moorestate=(!ald)?s2:s3;
s3:moorestate=(!ald)?s1:s3;
endcase
endmodule
*********************************************************
*****************COUNTER CODE***************************
module bc(ck,p,c,u,q);
input ck,p,c,u;
output[20:0]q;
reg clatched,platched,ulatched;
reg[20:0]counter;
assign q = counter;
initial
begin
counter = 0;
clatched=0;platched=0;ulatched=0;
end
always @(posedge ck)
begin
clatched=c;platched=p;ulatched=u;
end
always @ (posedge ck)
if(clatched) counter=0;
else if(platched) counter=255;
else if(ulatched)counter=counter+1;
else counter= counter-1;
endmodule
*********************************************************
THANKING YOU
Vanessa
_____________________________________________________
Chat with your friends as soon as they come online. Get Rediff Bol at
http://bol.rediff.com
This archive was generated by hypermail 2b30 : Sun Jun 03 2001 - 16:14:54 MDT