Registers did, rwd, and inxd of your description for VIS are not
initialized. Is this intentional?
Fabio
>>>>> "vg" == vanessa goyal <vanessa_goyal@rediffmail.com> writes:
vg> Hello Sir
vg> Functional simulation of following code,which is for 4x4 memory is working well over Xilinx fndtn. series but ,VIS is showing error .
vg> For e.g. following property is failing.
vg> AG((rwd=1 * file<*1*>[1:0]=3 * inxd=1)->AX(do[1:0]=3));
vg> which should not fail.
vg> Please tell me the reason of failure.
vg> I observed the counterexample also,I am not getting why
vg> the next state of
vg> rwd=1
vg> file<*1*>[1:0]=3
vg> inxd=1
vg> is,what counterexample is showing.
vg> ********************************************************
vg> CODE USED FOR FUNCTIONAL SIMULATION OVER XILINX
vg> ******************************************************
vg> module memory(clk,rw,inx,di,do);
vg> //parameter n=2,m=2;
vg> input clk,rw;
vg> input inx;
vg> input [1:0] di;
vg> output [1:0] do;
vg> //reg rwd;
vg> //reg inxd;
vg> //reg[1:0] did;
vg> reg [1:0] do;
vg> reg [1:0] file [1:0];
vg> //initial begin
vg> //file[0]=0;
vg> //file[1]=0;
vg> //do=0;
vg> //end
vg> //always @ (negedge clk)
vg> //begin
vg> //rwd=rw;inxd=inx;did=di;
vg> //end
vg> always @ (negedge clk)
vg> if (rw) do=file[inx];
vg> else file[inx]=di;
vg> endmodule
vg> *******************************************************
vg> CODE USED WITH VIS
vg> *******************************************************
vg> module memory(clk,rw,inx,di,do);
vg> //parameter n=2,m=2;
vg> input clk,rw;
vg> input inx;
vg> input [1:0] di;
vg> output [1:0] do;
vg> reg rwd;
vg> reg inxd;
vg> reg[1:0] did;
vg> reg [1:0] do;
vg> reg [1:0] file [1:0];
vg> initial begin
vg> file[0]=0;
vg> file[1]=0;
vg> do=0;
vg> end
vg> always @ (negedge clk)
vg> begin
vg> rwd=rw;inxd=inx;did=di;
vg> end
vg> always @ (negedge clk)
vg> if (rwd) do=file[inxd];
vg> else file[inxd]=did;
vg> endmodule
vg> Thanking you
vg> Vanessa
vg> _________________________________________________________
vg> For Rs. 2,000,000 worth of Aptech scholarships click below
vg> http://clients.rediff.com/clients/aptechsch/index.htm
This archive was generated by hypermail 2b30 : Mon Aug 13 2001 - 09:33:15 MDT