Hello,
I would like to check the following design (W10.trivial.blif):
.model w10l.s.pre_blif
.outputs xx35_out
.latch xx35 xx35_out 1;
.names xx35
1
.end
with the following invariant (W10.B.invar):
xx35_out = 1 ;
and the following script :
set vis_stdout ci_trivial_1.vis.output
set vis_stderr ci_trivial_1.vis.error
read_blif W10.trivial.blif
flatten_hierarchy
static_order
build_partition_mdds
check_invariant -d 1 -i -v 2 -F ci_trivial_1.vis.debug W10.B.invar
time
I've obtained the following output :
********************************
Reachability analysis results:
FSM depth = 1
reachable states = 2
BDD size = 1
analysis time = 0
reachability analysis = complete
# INV: Summary of invariant pass/fail
# INV: formula failed --- xx35_out=1
elapse: 0.0 seconds, total: 0.0 seconds
and the following debug trace :
# INV: formula 1 failed --- xx35_out=1
# INV: calling debugger
# INV: invariant fails at the following initial state
--State 0:
xx35_out:0
The built FSM accept value 0 for variable xx35_out even with the
.latch xx35 xx35_out 1;
initialising xx35_out with value 1.
How can I force the initial state of the FSM with chosen values ?
Could this be a bug ?
Thanks in advance for your response.
Jean-Luc Mercadier
This archive was generated by hypermail 2b30 : Mon Jul 08 2002 - 08:10:26 MDT