Bug #7753
closed
example.vhd: cannot generate SMV-based test
Added by Sergey Smolov over 7 years ago.
Updated over 6 years ago.
Category:
Engine (Transformer)
Published in build:
1.0.1-beta-170912
Description
Command line:
<path-to-example.vhd> --target vhdl-testbench;efsm;cgaa --toplevel example --assert-smv-file example.smv --check-method bmc --engine smv-test-parser --overwrite-existing
- Subject changed from example.vhd: EFSM extraction failure to example.vhd: cannot generate SMV-based test
- Detected in build changed from flatten.modules to master
The erroneous SMV file fragment:
next(W) :=
case
esac;
next(Z_SUBSTITUTED) :=
case
esac;
next(CLK) :=
case
esac;
next(RESET) :=
case
esac;
- Status changed from New to Open
- Status changed from Open to Resolved
- % Done changed from 0 to 100
- Status changed from Resolved to Verified
- Status changed from Verified to Closed
- Published in build set to 1.0.1-beta-170912
Also available in: Atom
PDF