Phung Cheng Fei buttercutter
buttercutter
/ testutil.c
Last active
December 19, 2018 07:37
Modified testutil.c https://github.com/KastnerRG/riffa/blob/master/c_c%2B%2B/linux/x64/test_apps/testutil.c
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| // ---------------------------------------------------------------------- | |
| // Copyright (c) 2016, The Regents of the University of California All | |
| // rights reserved. | |
| // | |
| // Redistribution and use in source and binary forms, with or without | |
| // modification, are permitted provided that the following conditions are | |
| // met: | |
| // | |
| // * Redistributions of source code must retain the above copyright | |
| // notice, this list of conditions and the following disclaimer. |
buttercutter
/ shift_register_compare.v
Last active
March 11, 2018 02:14
Induction example for https://imgur.com/a/MMr3c
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| /* | |
| Assumption #1: assume(i_ce) requires 16 steps, | |
| Assumption #2: always @(posedge i_clk) if (!$past(i_ce)) assume(i_ce); should take 16*2, | |
| Assumption #3: always @(posedge i_clk) if ((!$past(i_ce))&&(!$past(i_ce,2))) assume(i_ce); should require 16 * 3 = 48 steps. | |
| Here's what's going on: there are 16 values in that shift register. It takes i_ce being high to flush one more stage through the assertion. If assume(i_ce), then it will take about 16 clocks to flush the state in the shift register until sa == sb; | |
| if you do an always @(posedge i_ce) if (!$past(i_ce)) assume(i_ce); then there will never be more than one cycle between times when i_ce is high. | |
| The induction engine is going to prove us wrong, so it will stretch out the distance between the i_ce's as far as it can. If we require that it cannot stretch out by more than 2 samples, then it can only stretch out the time to prove all of the shift regi |
buttercutter
/ chnl_tester_chebyshev.v
Created
March 10, 2018 08:43
— forked from anonymous/chnl_tester_chebyshev.v
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| // ---------------------------------------------------------------------- | |
| // Copyright (c) 2016, The Regents of the University of California All | |
| // rights reserved. | |
| // | |
| // Redistribution and use in source and binary forms, with or without | |
| // modification, are permitted provided that the following conditions are | |
| // met: | |
| // | |
| // * Redistributions of source code must retain the above copyright | |
| // notice, this list of conditions and the following disclaimer. |
buttercutter
/ chnl_tester_2x_plus_1.v
Created
March 10, 2018 08:58
— forked from anonymous/chnl_tester_2x_plus_1.v
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| // ---------------------------------------------------------------------- | |
| // Copyright (c) 2016, The Regents of the University of California All | |
| // rights reserved. | |
| // | |
| // Redistribution and use in source and binary forms, with or without | |
| // modification, are permitted provided that the following conditions are | |
| // met: | |
| // | |
| // * Redistributions of source code must retain the above copyright | |
| // notice, this list of conditions and the following disclaimer. |
buttercutter
/ kitest.log
Created
March 15, 2018 13:33
BMC and Induction result log for http://zipcpu.com/blog/2018/03/10/induction-exercise.html
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| phung@UbuntuHW15:~/Documents/phung/verification_example$ sby kitest.sby | |
| SBY 21:29:44 [kitest] Copy 'kitest.v' to 'kitest/src/kitest.v'. | |
| SBY 21:29:44 [kitest] engine_0: smtbmc yices | |
| SBY 21:29:44 [kitest] script: starting process "cd kitest/src; yosys -ql ../model/design.log ../model/design.ys" | |
| SBY 21:29:44 [kitest] script: finished (returncode=0) | |
| SBY 21:29:44 [kitest] smt2: starting process "cd kitest/model; yosys -ql design_smt2.log design_smt2.ys" | |
| SBY 21:29:44 [kitest] smt2: finished (returncode=0) | |
| SBY 21:29:44 [kitest] engine_0.basecase: starting process "cd kitest; yosys-smtbmc -s yices --presat --unroll --noprogress -t 30 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2" | |
| SBY 21:29:44 [kitest] engine_0.induction: starting process "cd kitest; yosys-smtbmc -s yices --presat --unroll -i --noprogress -t 30 --append 0 --dump-vcd engine_0/trace_induct.vcd --dump-vlogtb engine_0/trace_induct_tb.v --dump-smtc engine_0/trace_induct.sm |
buttercutter
/ riffa.c
Created
March 23, 2018 02:35
Modified RIFFA linux driver code for full duplex transactions
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| // ---------------------------------------------------------------------- | |
| // Copyright (c) 2016, The Regents of the University of California All | |
| // rights reserved. | |
| // | |
| // Redistribution and use in source and binary forms, with or without | |
| // modification, are permitted provided that the following conditions are | |
| // met: | |
| // | |
| // * Redistributions of source code must retain the above copyright | |
| // notice, this list of conditions and the following disclaimer. |
buttercutter
/ Gm2_small_signal_model.sch
Last active
March 25, 2018 10:17
Gm2 small signal model for https://github.com/promach/frequency_trap/blob/development/Gm2.sch
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| v 20130925 2 | |
| C 40000 40000 0 0 0 title-B.sym | |
| N 51600 44700 52900 44700 4 | |
| C 52200 44100 1 0 0 gnd-1.sym | |
| C 43900 48300 1 270 1 gnd-1.sym | |
| C 41700 45000 1 0 0 gnd-1.sym | |
| N 52300 44700 52300 44400 4 | |
| T 52200 45500 9 10 1 0 0 0 1 | |
| Vin | |
| T 52300 45000 9 10 1 0 0 0 1 |
buttercutter
/ chnl_tester.v
Created
March 27, 2018 14:42
Modified chnl_tester.v https://github.com/KastnerRG/riffa/blob/master/fpga/riffa_hdl/chnl_tester.v
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| // ---------------------------------------------------------------------- | |
| // Copyright (c) 2016, The Regents of the University of California All | |
| // rights reserved. | |
| // | |
| // Redistribution and use in source and binary forms, with or without | |
| // modification, are permitted provided that the following conditions are | |
| // met: | |
| // | |
| // * Redistributions of source code must retain the above copyright | |
| // notice, this list of conditions and the following disclaimer. |
buttercutter
/ riffa.c
Last active
December 3, 2018 10:03
Modified riffa.c https://github.com/KastnerRG/riffa/blob/master/driver/linux/riffa.c
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| // ---------------------------------------------------------------------- | |
| // Copyright (c) 2016, The Regents of the University of California All | |
| // rights reserved. | |
| // | |
| // Redistribution and use in source and binary forms, with or without | |
| // modification, are permitted provided that the following conditions are | |
| // met: | |
| // | |
| // * Redistributions of source code must retain the above copyright | |
| // notice, this list of conditions and the following disclaimer. |
buttercutter
/ async_fifo.sby
Last active
December 7, 2021 19:54
An asynchronous FIFO implementation from the book "The Art of Hardware Architecture Design Methods and Techniques for Digital Circuits"
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| [tasks] | |
| proof | |
| cover | |
| [options] | |
| proof: mode prove | |
| proof: depth 5 | |
| cover: mode cover | |
| cover: depth 30 |