iaik / coco-alma Goto Github PK

Hi! Thank you for sharing this great work! I have been trying to run through the examples but I am getting an error when I try to run examples/prince_ti. The error occurs during the verify step.

python3 /home/karthik/projects/coco-alma/verify.py 
    --top-module top_module_d11
    --json /home/karthik/projects/coco-alma/tmp/circuit.json 
    --vcd /home/karthik/projects/coco-alma/tmp/tmp.vcd
    --label /home/karthik/projects/coco-alma/examples/prince_ti/labels.txt 
    --rst-name i_reset 
    --cycles 3 
    --mode transient 
    --probing-model time-constrained 
    --num-leaks 1

| CircuitGraph | Total: 6915 | Linear: 3146 | Non-linear: 1065 | Registers:  905 | Mux: 1211 | 
/home/karthik/projects/coco-alma/tmp/tmp.vcd:10574: [WARNING] Entry for name i_clk already exists in namemap (i_clk -> dW)
/home/karthik/projects/coco-alma/tmp/tmp.vcd:10575: [WARNING] Entry for name i_enc_dec already exists in namemap (i_enc_dec -> eW)
/home/karthik/projects/coco-alma/tmp/tmp.vcd:10576: [WARNING] Entry for name i_key1 already exists in namemap (i_key1 -> fW)
/home/karthik/projects/coco-alma/tmp/tmp.vcd:10577: [WARNING] Entry for name i_key2 already exists in namemap (i_key2 -> jW)
/home/karthik/projects/coco-alma/tmp/tmp.vcd:10578: [WARNING] Entry for name i_load already exists in namemap (i_load -> nW)
/home/karthik/projects/coco-alma/tmp/tmp.vcd:10579: [WARNING] Entry for name i_pt1 already exists in namemap (i_pt1 -> oW)
/home/karthik/projects/coco-alma/tmp/tmp.vcd:10580: [WARNING] Entry for name i_pt2 already exists in namemap (i_pt2 -> qW)
/home/karthik/projects/coco-alma/tmp/tmp.vcd:10581: [WARNING] Entry for name i_r already exists in namemap (i_r -> sW)
/home/karthik/projects/coco-alma/tmp/tmp.vcd:10582: [WARNING] Entry for name i_reset already exists in namemap (i_reset -> uW)
/home/karthik/projects/coco-alma/tmp/tmp.vcd:10583: [WARNING] Entry for name i_start already exists in namemap (i_start -> vW)
Traceback (most recent call last):
  File "/home/karthik/projects/coco-alma/verify.py", line 223, in <module>
    main()
  File "/home/karthik/projects/coco-alma/verify.py", line 195, in main
    trace = VCDStorage(args.vcd_file_path)
  File "/home/karthik/projects/coco-alma/VCDStorage.py", line 28, in __init__
    self.parse_header()
  File "/home/karthik/projects/coco-alma/VCDStorage.py", line 75, in parse_header
    assert (up - down + 1 == signal_width), "%s:%d Signal width does not match" % (self.vcd_file_path, self.line_nr)
AssertionError: /home/karthik/projects/coco-alma/tmp/tmp.vcd:10611 Signal width does not match

Line 10611 in tmp.vcd is $var wire 4 $' inaff.SHARE1[0].sh1.i_in1 [0:3] $end. Its hard to tell from this what the signals are.

I tried running the various steps manually as well as with run_pipeline.py but I see the same issue.

Coco has been in development for a long time now. Over the years, we have changed many things and Python was good for prototyping. However, it is now at a point where not even I can properly distinguish internal data structures, modes and what code is not in use. This needs to change. Python extremely exacerbates the problems of documentation and things are always in flux and prone to change. It promotes worse data structure organization among other things. Typing issues, runtime exceptions, most of which would be preventable. On top of everything, it is also super slow.

The long term plan is switching to C++. To make sure we do not repeat the same mistakes, we will require everything to be documented on commit, and tested with the CI workflow. This issue is supposed to track all of the steps that take us to a full implementation.

• Protect the master branch.
• Create a cpp-dev branch for development.
• Create a cmake project and include solver, json, options and other libraries.
• Create better sat solver interface based on IPASIR
• Migrate PropVarSets from other project.
• Add optimizations and alternatives for non-linear operations
• Enable unit testing of components with CTest
• Write tests for the SatSolver interface
• Rework concept and interactions within the verification process
• Decide on best structure -> reduce outer dependencies
• Finish migrating CircuitGraphCircuit class from other project.
• Create new structure for Cells, based on unions
• Implement execution semantics for all non-async Yosys cells
• [important] Make tests for execution semantics of all yosys cells
• [optional] Make it possible to create a Circuit without Yosys
• Create a unified structure for symbolic (PropVarSet) and concrete execution values
• Create Verification managerSimulator class based on the Circuit class
• Enable Simulator to maintain symbolic values on demand
• Implement debugging features for the Simulation (custom vcd generation)
• Implement proper Value caching utilities, that are respected by the operators
• Implement the verification routines
• [Milestone] Get first working Coco version.
• Implement optimizations:
• ...
• [Milestone] Release Coco 1.0

Hello,

I am trying to run the example provided in your github (using the stable_ok_10.S program). When running the trace.py script, the execution stops due to errors (in the "3: Compiling provided verilator testbench" stage):

clang-12: warning: treating 'c' input as 'c++' when in C++ mode, this behavior is deprecated [-Wdeprecated]
In file included from tmp/verilator_tb.c:3:

tmp/ram_init.h:2:15: error: no member named 'ibex_top__DOT__instr_rom__02emem__05b0__05d' in 'Vcircuit'; did you mean 'ibex_top__DOT__instr_rom__02Emem__05B0__05D'?
tb->m_core->ibex_top__DOT__instr_rom__02emem__05b0__05d = 0x00000000;
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
ibex_top__DOT__instr_rom__02Emem__05B0__05D
coco-alma/tmp/obj_dir/Vcircuit.h:22137:27: note: 'ibex_top__DOT__instr_rom__02Emem__05B0__05D' declared here
IData/31:0/ ibex_top__DOT__instr_rom__02Emem__05B0__05D;
^
In file included from tmp/verilator_tb.c:3:
tmp/ram_init.h:3:15: error: no member named 'ibex_top__DOT__instr_rom__02emem__05b1__05d' in 'Vcircuit'; did you mean 'ibex_top__DOT__instr_rom__02Emem__05B1__05D'?
tb->m_core->ibex_top__DOT__instr_rom__02emem__05b1__05d = 0x00000000;
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
ibex_top__DOT__instr_rom__02Emem__05B1__05D
coco-alma/tmp/obj_dir/Vcircuit.h:22252:27: note: 'ibex_top__DOT__instr_rom__02Emem__05B1__05D' declared here
IData/31:0/ ibex_top__DOT__instr_rom__02Emem__05B1__05D;
^
In file included from tmp/verilator_tb.c:3:
tmp/ram_init.h:4:15: error: no member named 'ibex_top__DOT__instr_rom__02emem__05b2__05d' in 'Vcircuit'; did you mean 'ibex_top__DOT__instr_rom__02Emem__05B2__05D'?
tb->m_core->ibex_top__DOT__instr_rom__02emem__05b2__05d = 0x00000000;
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
ibex_top__DOT__instr_rom__02Emem__05B2__05D
coco-alma/tmp/obj_dir/Vcircuit.h:22321:27: note: 'ibex_top__DOT__instr_rom__02Emem__05B2__05D' declared here
IData/31:0/ ibex_top__DOT__instr_rom__02Emem__05B2__05D;
^
...

fatal error: too many errors emitted, stopping now [-ferror-limit=]
20 errors generated.

Do you have an idea why I obtain such errors ?
Thank you for your help.

Best

In the default case, the --from-cycle command line parameter is essentially ignored, which is wrong. This requires careful adjustments of a re-integrated portion of old code.

verify.py supports a row of arguments. The documentation of the following could be improved:

• --glitch-behavior
• --trace-stable
• --minimize-leaks

Hello,

I'm trying to run the examples/ibex and using my own program which is:

.org 0x80
nop
xor x1,  x1, x9
and x0,  x0, x0
xor x17, x1, x9
nop
nop
nop
...

and the label file is:

# registers: x1, x9, x17
u_core.register_file_i.rf_reg_reg[32]  = secret 0
u_core.register_file_i.rf_reg_reg[288] = static_random
u_core.register_file_i.rf_reg_reg[544] = secret 0

I execute the verification script using the --mode stable and the --include-hamming options (plus --cycles -1, --rst-name rst_sys_n, --rst-cycles 2, --rst-phase 0), and I expect it should report a transition leakage (because I overwrite the register x17 which contains a share by another share). But the verification script doesn't report any leakages, therefore I'd like to ask: is there somewhere I made a mistake (about the usage of this tool) or somewhere I just didn't understand correctly?

Many thanks for your help!

Hi,

I am trying to experiment with your verification tool as I find it very interesting.
I work on "Rocky Linux "8.4 (Green Obsidian). I had issues with the pip install python-sat==0.1.7.dev10
so I installed python-sat using pip install python-sat[pblib,aiger] (maybe this might create error later on ?).

I am following the steps mentioned in https://github.com/IAIK/coco-alma/tree/master/examples/ibex.
Unfortunately, I am stuck at the section "Compile RISC-V Program and create the header for the testbench".
When I run:
assemble.py --program programs/aes_sbox.S --netlist ../../tmp/circuit.v

I obtain:

Using program file:  programs/aes_sbox.S
Using initialization file:  None
Using build directory: /volume1/scratch/jgaspoz/cocoAlma/coco-alma/tmp
Using netlist path: ../../tmp/circuit.v

.text section is too large (> 1024 bytes)

Do you know how to fix this error ?

Thanks a lot for you help.