Re: Can't run check_invariant -A4 (The puresat algorithm)

From: Andrea Fedeli (andrea.fedeli_at_mclink.it)
Date: Sat Mar 31 2007 - 23:01:39 MDT

Next message: dennyhuang_at_fudan.edu.cn: "Can not download the source code"
Previous message: Sunil Rafeeque K.P.: "Re: Can't run check_invariant -A4 (The puresat algorithm)"
In reply to: Zaher S Andraus: "Re: Can't run check_invariant -A4 (The puresat algorithm)"
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ] [ attachment ]
Mail actions: [ respond to this message ] [ mail a new topic ]

Hi Zaher,

Neither I can reproduce your issue; here is what I get

vis release 2.1 (compiled 17-ott-05 at 6:33 AM)
vis> read_verilog design1.v
design1.v
Warning: Some variables are unused in model design1.
vis> init_verify
vis> build_partition_maigs
WARNING : floating node prop
vis> check_invariant -A4 design1.inv
# INV: formula failed --- prop=1

That is on an Athlon-XP 2800+, OpenSUSE 10.2 (gcc 4.1.2).

Please notice that the VIS version I tried is more recent than the one
you reported in another recent thread.

Cheers,

Andrea.

-- 
Andrea Fedeli
It is better for civilization to be going down the drain than to be
coming up it.
		-- Henry Allen

Next message: dennyhuang_at_fudan.edu.cn: "Can not download the source code"
Previous message: Sunil Rafeeque K.P.: "Re: Can't run check_invariant -A4 (The puresat algorithm)"
In reply to: Zaher S Andraus: "Re: Can't run check_invariant -A4 (The puresat algorithm)"
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ] [ attachment ]
Mail actions: [ respond to this message ] [ mail a new topic ]

This archive was generated by hypermail 2.1.7 : Sat Mar 31 2007 - 23:03:37 MDT