Skip to content

Instantly share code, notes, and snippets.

View buttercutter's full-sized avatar

Phung Cheng Fei buttercutter

61 followers · 29 following
View GitHub Profile
@buttercutter
buttercutter / detect_start_bit.v
Created October 12, 2017 09:27
module detect_start_bit(clk, serial_in, start_detected); // just a falling edge detector
input clk, serial_in;
output reg start_detected = 0;
reg previously_idle = 1;
always @(posedge clk)
begin
if((!serial_in) && (previously_idle) && (!start_detected))
@buttercutter
buttercutter / baud_generator_tb.v
Created October 24, 2017 05:06
Testbench for https://github.com/promach/UART/blob/master/rtl/baud_generator.v
`timescale 1ps/100fs
module baud_generator_tb;
reg clk;
wire baud_out;
baud_generator BG1
(
.clk(clk),
.baud_out(baud_out)
@buttercutter
buttercutter / xillydemo.v
Created December 27, 2017 11:15
module xillydemo
(
input clk_100,
input otg_oc,
inout [55:0] PS_GPIO,
output [3:0] GPIO_LED,
output [3:0] vga4_blue,
output [3:0] vga4_green,
output [3:0] vga4_red,
output vga_hsync,
@buttercutter
buttercutter / base.tcl
Created January 12, 2018 02:20
PYNQ modified TCL setup script for Vivado 2017.2
###############################################################################
# Copyright (c) 2016, Xilinx, Inc.
# All rights reserved.
#
# Redistribution and use in source and binary forms, with or without
# modification, are permitted provided that the following conditions are met:
#
# 1. Redistributions of source code must retain the above copyright notice,
# this list of conditions and the following disclaimer.
@buttercutter
buttercutter / test_lpthread.c
Last active January 17, 2018 12:19
Simple multi-threaded application explains how to create apps with multiple threads and also explains about how to deal with args parameter of pthread_create
#include <stdio.h>
#include <pthread.h>
#include <stdlib.h>
#include <unistd.h>
#include <errno.h>
#include <sys/types.h>
#include <sys/stat.h>
#include <fcntl.h>
#include <string.h>
#include <stdint.h>
@buttercutter
buttercutter / chnl_convolution.v
Created February 5, 2018 04:36
Sobel convolution for Xilinx ML605 (single channel) example in http://riffa.ucsd.edu/node/16
`timescale 1ns/1ns
//----------------------------------------------------------------------------
// This software is Copyright © 2012 The Regents of the University of
// California. All Rights Reserved.
//
// Permission to copy, modify, and distribute this software and its
// documentation for educational, research and non-profit purposes, without
// fee, and without a written agreement is hereby granted, provided that the
// above copyright notice, this paragraph and the following three paragraphs
// appear in all copies.
@buttercutter
buttercutter / chnl_tester_chebyshev.v
Created March 10, 2018 08:43 — forked from anonymous/chnl_tester_chebyshev.v
// ----------------------------------------------------------------------
// 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
buttercutter / chnl_tester_2x_plus_1.v
Created March 10, 2018 08:58 — forked from anonymous/chnl_tester_2x_plus_1.v
// ----------------------------------------------------------------------
// 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
buttercutter / shift_register_compare.v
Last active March 11, 2018 02:14
Induction example for https://imgur.com/a/MMr3c
/*
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
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
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