I tested the QED files generated by your workflow using the original ridecore demo. To do this, I replaced the original QED files by the generated ones. The test worked fine except for a spurious counterexample I got, which can be avoided by the following minor fixes.
files qed_i_cache.v and qed_instruction_mux.v: the include statements of the header file "qed.vh" in the first line should be removed. Actually, these changes are not related to the spurious counterexample but fix a parsing error. In the original ridecore demo, the header file "qed.vh" is used only for simulation using module qed_sm.v but not for model checking.
@msrouji Hi Mario,
I tested the QED files generated by your workflow using the original ridecore demo. To do this, I replaced the original QED files by the generated ones. The test worked fine except for a spurious counterexample I got, which can be avoided by the following minor fixes.
the constraint FORMAT_I is defined and should also be added to several lines in file inst_constraints.v.
the constraint FORMAT_R is defined and also should be added to several lines in file inst_constraints.v.
file modify_instruction.v: "NEW_imm12" should be replaced by "imm12" in line 57
files qed_i_cache.v and qed_instruction_mux.v: the include statements of the header file "qed.vh" in the first line should be removed. Actually, these changes are not related to the spurious counterexample but fix a parsing error. In the original ridecore demo, the header file "qed.vh" is used only for simulation using module qed_sm.v but not for model checking.