This upload is the research artifact used in the submission of ICCAD'23: Automatic Inductive Invariant Generation for Scalable Dataflow Circuit Verification. In particular: dhls-iccad23.zip is a complete workflow used in the submission (in particular it contains, Dynamatic, verification model generator, inductive invariant generator, and utility scripts for setting up the entire environment). iccad23_experiments_zenodo.zip contains the performed experiments. It includes the complete workflow in dhls-iccad23.zip, and it has detailed instructions for setting up the environments, running the experiments, and extracting the results. It is recommended to use Dynamatic VM -- a pre-installed virtual machine to evaluate the experiments (accessible through https://dynamatic.epfl.ch/, which notably has pre-installed llvm-6.0 and ModelSim). Each zip file has detailed instructions.