From: Waseem Muhammad (Waseem.Muhammad_at_eurecom.fr)
Date: Wed Jun 11 2008 - 02:17:10 MDT
You can refer only those variables of your module in CTL formula which
constitute some state (register). Your input 'a' (and 'b' too!) in
module "fulladder128" is not a register but wire, therefore VIS is
unable to find any state for these variables and this gives error.
A solution is to create a top level module where you instantiate your
"fulladder128" instance and supply it with registered
inputs 'a' and 'b'. This top level module should be given to VIS which
then builds states for your inputs 'a' and 'b' and you can verify the
given property.
Regards
Waseem
Aritra Hazra wrote:
> Sir,
>
> I am encountering an error while attempting to use VIS to
> verify a simple "128-bit fulladder" file in verilog with a CTL file
> having one CTL formula.
>
> The error message looks like:
> ** mc error: error in parsing Atomic Formula:
> Could not find node corresponding to the name
> - fulladder128.a<127>
> (Wire for this name may have been removed by synthesis)
>
> I have seen few solutions to this error in:
> (i) VIS FAQ page (point-8)
> (http://vlsi.colorado.edu/~vis/doc/html/vis-faq.html
> <http://vlsi.colorado.edu/%7Evis/doc/html/vis-faq.html>) and
> (ii) The mails regarding such problem in
> http://vlsi.colorado.edu/~vis/vis-users2/0104.html
> <http://vlsi.colorado.edu/%7Evis/vis-users2/0104.html>.
> But, approaching according to the previous two
> suggestions do not help me either.
>
> I am attaching my verilog test file and the CTL formula file.
>
> Kindly help me regarding this and suggest how I can get rid
> of this error.
>
> Thanking you for your time,
> -----
> Aritra Hazra.
> MS Student & Research Consultant,
> Department of Computer Science & Engineering,
> Indian Institute of Technology, Kharagpur.
> INDIA - 721302
-- Waseem MUHAMMAD PhD Research Student Office 231, System-on-Chip Laboratory ENST Institut Eurecom BP 193, 2229 route des Cretes 06904 Sophia-Antipolis Cedex France Tel: +33 (0) 4 93 00 84 05 Fax: +33 (0) 4 93 00 82 00
This archive was generated by hypermail 2.1.7 : Wed Jun 11 2008 - 02:20:26 MDT