GitHub - saranyuc3/Trojan-Counter

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 2 Commits
.visualizer		.visualizer
Output_Results		Output_Results
jgproject		jgproject
qed		qed
vscale_verilog		vscale_verilog
work		work
#README#		#README#
#toppipe.v#		#toppipe.v#
#vscale.flist#		#vscale.flist#
.qverify_ui_local_prefs		.qverify_ui_local_prefs
Makefile		Makefile
OpenSPARCT2.cshrc.linux		OpenSPARCT2.cshrc.linux
README		README
SQED_Trojan_example.pptx		SQED_Trojan_example.pptx
abs_README		abs_README
abs_README~		abs_README~
clean.sh		clean.sh
compile.sh		compile.sh
constants.vh		constants.vh
design.sh		design.sh
directives.tcl		directives.tcl
gui.sh		gui.sh
hnl_const_prop.rpt		hnl_const_prop.rpt
jasper.tcl		jasper.tcl
knockout_trigger.v		knockout_trigger.v
local_old_questa.cshrc		local_old_questa.cshrc
modelsim.ini		modelsim.ini
prove.sh		prove.sh
prove.sh~		prove.sh~
qed.vh		qed.vh
questa.bashrc		questa.bashrc
run.sh		run.sh
rv32_opcodes.vh		rv32_opcodes.vh
setup.cshrc		setup.cshrc
test.init		test.init
toppipe.v		toppipe.v
toppipe.v~		toppipe.v~
visualizer.log		visualizer.log
vscale.flist		vscale.flist
vscale.flist~		vscale.flist~
vscale_alu_ops.vh		vscale_alu_ops.vh
vscale_checker.sv		vscale_checker.sv
vscale_checker.sv~		vscale_checker.sv~
vscale_checker_bind.sv		vscale_checker_bind.sv
vscale_csr_addr_map.vh		vscale_csr_addr_map.vh
vscale_ctrl_constants.vh		vscale_ctrl_constants.vh
vscale_hasti_constants.vh		vscale_hasti_constants.vh
vscale_jg.flist		vscale_jg.flist
vscale_md_constants.vh		vscale_md_constants.vh
vscale_platform_constants.vh		vscale_platform_constants.vh
workspace.sh		workspace.sh

Repository files navigation

1. clean.sh to clean workspace
2. workspace.sh to create a workspace.
3. design.sh to pull in design
4. compile.sh to compile design.
5. prove.sh to run formal.
6. gui.sh to visualize results, need to manually open Output_Results/formal_verify.db in gui due to weird licensing issue