Jin,
My guess is that one of the signals you use in your formula is an
input. That is not allowed.
To bypass this restriction, make an extra latch that latches your input,
and use the latch in your formula. This changes your input-output
language by shifting the input by one timestep, but typically that is
easily taken into account. There is an example below.
If I am wrong, please send us the verilog.
Roderick.
Example:
----------------------
module simple(clk, in);
input clk;
input in;
reg latch;
initial latch = 0;
always @(posedge clk)
latch = in;
endmodule
----------------------
AG(in = 1 -> AX latch = 1);
-----------------
If we have the verilog file above, and you try to model check the given
CTL formula, you will get this error:
** mc error: error in parsing Atomic Formula:
Node in found in the support of node in.
Node in is not driven only by latches and constants.
Now if we latch our input as below and use the formula below, things
will work.
-------------------------------------
module simple2(clk, in);
input clk;
input in;
reg latch;
reg inlatched;
initial begin
latch = 0;
inlatched = 0;
end
always @(posedge clk)
inlatched = in;
always @(posedge clk)
latch = inlatched;
endmodule
------------------------------------
AG(inlatched = 1 -> AX latch = 1);
Jin Hou wrote:
>
> Hi,
> When I used VIS to verify a property on my design, the system gave me
> the following message:
> ** mc error: error in parsing Atomic Formula:
> Node S found in the support of node S.
> Node S is not driven only by latches and constants.
>
> I checked my property shown in the following and cannot find any error.
> Could you please tell me why the property cannot be passed?
>
> AG( ( S=0 * RD = 0 * R0[27:0]=0) -> AX(R0[27:0]=1) );
>
> Thanks!
>
> Jin
This archive was generated by hypermail 2b29 : Thu Apr 06 2000 - 10:31:19 MDT