Jaen-Luc,
If your .mv file does not specify the intial state(s), then all
possible states are assumed initial.
You want to add the following lines:
.r xx35_out
1
to your model. This will force the initial state to 1.
Fabio
>>>>> "JM" == Jean-Luc Mercadier <jean-luc.mercadier@tni-valiosys.com> writes:
JM> Hello,
JM> I would like to check the following design (W10.trivial.blif):
JM> .model w10l.s.pre_blif
JM> .outputs xx35_out
JM> .latch xx35 xx35_out 1;
JM> .names xx35
JM> 1
JM> .end
JM> with the following invariant (W10.B.invar):
JM> xx35_out = 1 ;
JM> and the following script :
JM> set vis_stdout ci_trivial_1.vis.output
JM> set vis_stderr ci_trivial_1.vis.error
JM> read_blif W10.trivial.blif
JM> flatten_hierarchy
JM> static_order
JM> build_partition_mdds
JM> check_invariant -d 1 -i -v 2 -F ci_trivial_1.vis.debug W10.B.invar
JM> time
JM> I've obtained the following output :
JM> ********************************
JM> Reachability analysis results:
JM> FSM depth = 1
JM> reachable states = 2
JM> BDD size = 1
JM> analysis time = 0
JM> reachability analysis = complete
JM> # INV: Summary of invariant pass/fail
JM> # INV: formula failed --- xx35_out=1
JM> elapse: 0.0 seconds, total: 0.0 seconds
JM> and the following debug trace :
JM> # INV: formula 1 failed --- xx35_out=1
JM> # INV: calling debugger
JM> # INV: invariant fails at the following initial state
JM> --State 0:
JM> xx35_out:0
JM> The built FSM accept value 0 for variable xx35_out even with the
JM> .latch xx35 xx35_out 1;
JM> initialising xx35_out with value 1.
JM> How can I force the initial state of the FSM with chosen values ?
JM> Could this be a bug ?
JM> Thanks in advance for your response.
JM> Jean-Luc Mercadier
This archive was generated by hypermail 2b30 : Mon Jul 08 2002 - 15:07:11 MDT