Prahallad,
I think I have identofied where the problem comes from. I don't have a
solution, maybe someone else knows one?
Your system has multiple drivers for the same signal. In particular,
the cache module has two always@(posedge clock) blocks, both of which
drive transReqPending. Although this may be legal Verilog (I cannot
judge that), vl2mv does not allow it.
I can se two solutions:
* Rewrite the model to conform to vl2mv specifics.
* Use a synthesis tool to obtain the blif. (See the FAQ.)
Maybe someone else knows whether there is an option to vl2mv to do
this? Has ST been seen recently?
Below is a small model that exhibits the same problem.
Roderick.
prahallad wrote:
>
> Dear sir,
> I am M.Tech student in IITKanpur doing Microelectronics.As part of our m.Tech
> Thesis,I am working on the formal verification.
> I have installed VIS(ver 1.3) in Linux mandrake.I have got the vl2mv(linux
> version)executable from the VIS website.
> Vl2mv is converting the verilog file into corresponding .mv file.After that VIS
> is reading the .mv file by read-blif_mv command.But when i am doing init_verify
> it is giving the following errors.
> Is there problem in the verilog code?or vl2mv is creating problems?
> I am attaching the verilog file and BLIF-MV file(created through vl2mv).
>
> The error is as follows:
>
> vis> read_blif_mv ls_ls_v01.mv
> Warning: Some variables are unused in model PENTIUM_PRO_SYSTEM.
> Warning: Model P6 may have a cyclic connection which involves variable
> EXT_DATA_O<0>
> Warning: Some variables are unused in model MEMORY.
> Warning: Some variables are unused in model EU.
> Warning: Some variables are unused in model REQUEST_AGENT.
> vis> init_verify
> Table processor0.CACHE1._n181e is not deterministic
> Table processor0.CACHE1._n1841<0> is not deterministic
etc etc
module main(clk);
input clk;
reg ister;
always @(posedge clk) begin
ister = 0;
end
always @(posedge clk) begin
ister = 0;
end
endmodule
_________________________________________________________
Do You Yahoo!?
Get your free @yahoo.com address at http://mail.yahoo.com
This archive was generated by hypermail 2b29 : Thu Nov 09 2000 - 11:08:40 MST