Skip to content

klsllzx/rtl_z3

Repository files navigation

Example Script

./taint_tracker --toplevel u_xmit --dump-binds --dump-terms --dump-ast --timewindow 5 --solver-signal 'BitVec("u_xmit.state_DataSend#0",3) == 7' --solver-signal 'BitVec("u_xmit.sys_rst_l#5", 1) == 0' --pattern-var u_xmit.xmit_dataH ../experiment/RS232-T700/u_xmit_t700.v

./taint_tracker --toplevel darkriscv --timewindow 4 --solver-signal 'BitVec("darkriscv.unlocked#0", 1) == 1' --solver-signal 'BitVec("darkriscv.RES#4", 1) == 1' --pattern-var darkriscv.IDATA --isa-type riscv ../experiment/ASP_DAC/dark_riscv/modified_preprocess_trojan.v

Dependencies

  • pip3 install timeout-decorator

Bug List

reg [3:0] RESMODE = -1; 

always@(posedge CLK)
RESMODE <= RES ? -1 : RESMODE ? RESMODE-1 : 0;

In this case pyverilog only identify the second one without time delay we use modified_preprocess.v to eliminate this kind of bug compared with original_preprocess.v

wire [3:0] DPTR;
!DPTR is not valid when parsing
  • LLM
  • Mem cache
  • IP

About

No description, website, or topics provided.

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

 
 
 

Contributors