- This is a formally verified Moore FSM based overlapping sequence detector with registered outputs.
- Tools & Technologies: SystemVerilog, SystemVerilog Assertions, HW-CBMC
- Results: Assertion passing using Bounded Model Checking. Cover statements written and working visualized in the waveform.
- Files & Directories:
- seq_detector.sv: RTL design of "1011" overlapping sequence detector with registered outputs, Moore style. Contains formal properties and witness cover statement.
- seq_detector.vcd: Dump file generated by EBMC for cover statements.
- Run command:
ebmc seq_detector.sv --top seq_detector --bound 500 --reset reset==1 --vcd seq_detector.vcd > ebmc.log
Unbounded model check:
k induction:
ebmc seq_detector.sv --top seq_detector --k-induction --reset reset==1 > ebmc_k_induction.log
BDD:
ebmc seq_detector.sv --top seq_detector --bdd --reset reset==1 > ebmc_bdd.log